Local mirror of The Unified Policy Framework (UPF) entry of the Archive of Formal Proofs (AFP). https://www.isa-afp.org/entries/UPF_Firewall.shtml
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

87 lines 4.6 KiB Raw Permalink Normal View History

 5 years ago To cite the use of this formal theory, please use   3 years ago  Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Formal Network   Models and Their Application to Firewall Policies. In Archive of Formal   Proofs, 2017. http://www.isa-afp.org/entries/UPF_Firewall.shtml,   Formal proof development. 5 years ago   A BibTeX entry for LaTeX users is   3 years ago @Article{ brucker.ea:upf-firewall:2017,  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.},  author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},  date = {2017-01-08},  file = {https://www.brucker.ch/bibliography/download/2017/brucker.ea-upf-firewall-outline-2017.pdf},  filelabel = {Outline},  issn = {2150-914x},  journal = {Archive of Formal Proofs},  month = {jan},  note = {\url{http://www.isa-afp.org/entries/UPF_Firewall.shtml}, Formal proof development},  pdf = {https://www.brucker.ch/bibliography/download/2017/brucker.ea-upf-firewall-2017.pdf},  title = {Formal Network Models and Their Application to Firewall Policies},  url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-upf-firewall-2017},  year = {2017}, }  5 years ago   An overview of the formalization is given in:    Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Formal Firewall  Conformance Testing: An Application of Test and Proof Techniques. In  Software Testing, Verification & Reliability (STVR), 25 (1), pages  34-71, 2015.  https://www.brucker.ch/bibliography/abstract/brucker.ea-formal-fw-testing-2014   A BibTeX entry for LaTeX users is @Article{ brucker.ea:formal-fw-testing:2014,  abstract = {Firewalls are an important means to secure  critical ICT infrastructures. As configurable  off-the-shelf prod\-ucts, the effectiveness of a  firewall crucially depends on both the correctness  of the implementation itself as well as the  correct configuration. While testing the  implementation can be done once by the  manufacturer, the configuration needs to be tested  for each application individually. This is  particularly challenging as the configuration,  implementing a firewall policy, is inherently  complex, hard to understand, administrated by  different stakeholders and thus difficult to  validate. This paper presents a formal model of  both stateless and stateful firewalls (packet  filters), including NAT, to which a  specification-based conformance test case  gen\-eration approach is applied. Furthermore, a  verified optimisation technique for this approach  is presented: starting from a formal model for  stateless firewalls, a collection of  semantics-preserving policy transformation rules  and an algorithm that optimizes the specification  with respect of the number of test cases required  for path coverage of the model are derived. We  extend an existing approach that integrates  verification and testing, that is, tests and  proofs to support conformance testing of network  policies. The presented approach is supported by a  test framework that allows to test actual  firewalls using the test cases generated on the  basis of the formal model. Finally, a report on  several larger case studies is presented.},  author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},  doi = {10.1002/stvr.1544},  journal = {Software Testing, Verification & Reliability (STVR)},  keywords= {model-based testing; conformance testing; security  testing; firewall; specification-based testing;  testing cloud infrastructure, transformation for  testability; HOL-TestGen; test and proof; security  configuration testing},  language= {USenglish},  number = {1},  pages = {34--71},  pdf = {https://www.brucker.ch/bibliography/download/2014/brucker.ea-formal-fw-testing-2014.pdf},  publisher= {John Wiley & Sons},  title = {Formal Firewall Conformance Testing: An Application of Test and Proof Techniques},  url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-formal-fw-testing-2014},  volume = {25},  year = {2015}, 3 years ago }