87 lines
4.6 KiB
Plaintext
87 lines
4.6 KiB
Plaintext
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},
|
|
}
|