Formal Network Models and Their Application to Firewall Policies

Achim D. Brucker 🌐, Lukas Brügger and Burkhart Wolff 🌐

January 8, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

We present a formal model of network protocols and their application to modeling firewall policies. The formalization is based on the Unified Policy Framework (UPF). The formalization was originally developed with for generating test cases for testing the security configuration actual firewall and router (middle-boxes) using HOL-TestGen. Our work focuses on modeling application level protocols on top of tcp/ip.

License

BSD License

Topics

Related publications

  • Brucker, A. D., Brügger, L., & Wolff, B. (2014). Formal firewall conformance testing: an application of test and proof techniques. Software Testing, Verification and Reliability, 25(1), 34–71. https://doi.org/10.1002/stvr.1544

Session UPF_Firewall

Depends on

Cite

× 
@article{UPF_Firewall-AFP,
  author  = {Achim D. Brucker and Lukas Brügger and Burkhart Wolff},
  title   = {Formal Network Models and Their Application to Firewall Policies},
  journal = {Archive of Formal Proofs},
  month   = {January},
  year    = {2017},
  note    = {\url{https://isa-afp.org/entries/UPF_Firewall.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: