Formal Network Models and Their Application to Firewall Policies

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

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.

Please cite this work as follows:
A. D. Brucker, L. Brügger, and B. Wolff, “Formal network models and their application to firewall policies,” Archive of Formal Proofs, Jan. 2017. https://www.isa-afp.org/entries/UPF_Firewall.shtml, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-upf-firewall-2017/

BibTeX
@Article{ brucker.ea:upf-firewall:2017,
  author    = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
  title     = {Formal Network Models and Their Application to Firewall
               Policies},
  journal   = {Archive of Formal Proofs},
  month     = {jan},
  year      = {2017},
  date      = {2017-01-08},
  note      = {\url{https://www.isa-afp.org/entries/UPF_Firewall.shtml},
               Formal proof development. 
               Author copy: \url{https://logicalhacking.com/publications/brucker.ea-upf-firewall-2017/}},
  issn      = {2150-914x},
  abstract  = {We present a formal model of network protocols and their
               application to modeling firewall policies. The formalization
               is based on the \emph{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.},
  filelabel = {Outline},
  file      = {download/2017/brucker.ea-upf-firewall-outline-2017.pdf},
  areas     = {formal methods, security},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-upf-firewall-2017/brucker.ea-upf-firewall-2017.pdf},
}