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

To cite the use of this formal theory, please use
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.
A BibTeX entry for LaTeX users is
@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},
}
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},
}