afp-mirror
/
UPF_Firewall
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Added introduction.

This commit is contained in:
Achim D. Brucker 2017-01-04 14:58:02 +00:00
parent 722ca30ad4
commit 73bc5df9fc
3 changed files with 335 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

164
document/introduction.tex
View File

@ -1,12 +1,154 @@
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)~\cite{brucker.ea:upf:2014}. The
formalization was originally developed with for generating test cases
(see~\cite{brucker.ea:formal-fw-testing:2014} for details) for testing the
security configuration actual firewall and router (middle-boxes) using
HOL-TestGen~\cite{brucker.ea:formal-fw-testing:2014}. Our work focuses
on modeling application level protocols on top of tcp/ip. Thus, its
abstraction level differs from Diekmann's Network Security Policy
Verification
formalization~\cite{Network_Security_Policy_Verification-AFP}.
\section{Motivation}
Because of its connected life, the modern world is increasingly
depending on secure implementations and configurations of network
infrastructures. As building blocks of the latter, firewalls are
playing a central role in ensuring the overall \emph{security} of
networked applications.
Firewalls, routers applying network-address-translation (NAT) and
similar networking systems suffer from the same quality problems as
other complex software. Jennifer Rexford mentioned in her keynote at
POPL 2012 that high-end firewalls consist of more than 20
million lines of code comprising components written in Ada as well as
LISP. However, the testing techniques discussed here are of
wider interest to all network infrastructure operators that need to
ensure the security and reliability of their infrastructures across
system changes such as system upgrades or hardware replacements. This
is because firewalls and routers are active network elements that can
filter and rewrite network traffic based on configurable rules. The
\emph{configuration} by appropriate rule sets implements a security
policy or links networks together.
Thus, it is, firstly, important to test both the implementation of a
firewall and, secondly, the correct configuration for each use. To
address this problem, we model firewall policies formally in
Isabelle/HOL. This formalization is based on the Unified Policy
Framework (UPF)~\cite{brucker.ea:upf:2014}. This formalization allows
to express access control policies on the network level using a
combinator-based language that is close to textbook-style
specifications of firewall rules. To actually test the implementation
as well as the configuration of a firewall, we use
HOL-TestGen~\cite{brucker.ea:hol-testgen-fw:2013,brucker.ea:theorem-prover:2012}
to generate test cases that can be used to validate the compliance of
real network middleboxes (e.g., firewalls, routers). In this document,
we focus on the Isabelle formalization of network access control
policies. For details of the overall approach, we refer the reader
elsewhere~\cite{brucker.ea:formal-fw-testing:2014}
\section{The Unified Policy Framework (UPF)}
Our formalization of firewall policies is based on the Unified Policy
Framework (UPF. In this section, we briefly introduce UPF, for all
details we refer the reader to)~\cite{brucker.ea:upf:2014}.
UPF is a generic framework for policy modeling with the primary goal
of being used for test case generation. The interested reader is
referred to~\cite{brucker.ea:model-based:2011} for an application of
UPF to large scale access control policies in the health care domain;
a comprehensive treatment is also contained in the reference manual
coming with the distribution on the \testgen website
(\url{http://www.brucker.ch/projects/hol-testgen/}). UPF is based on
the following four principles:
\begin{enumerate}
\item policies are represented as \emph{functions} (rather than relations),
\item policy combination avoids conflicts by construction,
\item the decision type is three-valued (allow, deny, undefined),
\item the output type does not only contain the decision but also a
`slot' for arbitrary result data.
\end{enumerate}
Formally, the concept of a policy is specified as a partial function
from some input to a decision value and additional some
output. \emph{Partial} functions are used because elementary policies
are described by partial system behavior, which are glued together by
operators such as function override and functional composition.
\begin{gather*}
\types\enspace \alpha \mapsto \beta =
\alpha \rightharpoonup \beta \operatorname{decision}
\end{gather*}
where the enumeration type $\operatorname{decision}$ is
\begin{gather*}
\datatype \qquad \alpha\ap \operatorname{decision}
= \operatorname{allow}\ap \alpha \mid
\operatorname{deny}\ap \alpha
\end{gather*}
As policies are partial functions or `maps', the notions of a
\emph{domain} $\dom \ap p \ofType \alpha \rightharpoonup \beta
\Rightarrow \HolSet{\alpha}$ and a \emph{range} $\ran\ap p \ofType
[\alpha \rightharpoonup \beta] \Rightarrow \HolSet{\beta}$ can be
inherited from the Isabelle library.
Inspired by the Z notation~\cite{spivey:z-notation:1992}, there is the
concept of \emph{domain restriction} $\_ \triangleleft \_$ and
\emph{range restriction} $\_ \triangleright \_$, defined as:
\begin{gather*}
\begin{array}{lrl}
\isadefinition &\_ \triangleleft \_&\ofType \HolSet{\alpha}
\Rightarrow \alpha \mapsto \beta \Rightarrow \alpha \mapsto \beta\\
\where & S \triangleleft p &= \lambda x\spot \HolIf x \in S \HolThen p\ap x
\HolElse \bottom \\[.5ex]
\isadefinition & \_ \triangleright \_ &\ofType \alpha \mapsto
\beta \Rightarrow \HolSet{\beta\ap\operatorname{decision}}
\Rightarrow \alpha \mapsto \beta \\
\where & p \triangleright S &= \lambda x\spot \HolIf
\bigl(\operatorname{the}\ap
(p\ap x)\bigr) \in S \HolThen p\ap x \HolElse \bottom \\
\end{array}
\end{gather*}
The operator `$\operatorname{the}$' strips off the $\HolSome$, if it
exists. Otherwise the range restriction is underspecified.
There are many operators that change the result of applying the
policy to a particular element. The essential one is the
\emph{update}:
\begin{gather*}
p(x \mapsto t) = \lambda y\spot \HolIf y = x \HolThen \lfloor
t\rfloor \HolElse p\ap y
\end{gather*}
Next, there are three categories of elementary policies in UPF,
relating to the three possible decision values:
\begin{itemize}
\item The empty policy; undefined for all elements: $\emptyset =
\lambda x\spot \bottom$
\item A policy allowing everything, written as $A_f\ap f$, or $A_U$ if
the additional output is unit (defined as $\lambda x\spot \lfloor
\operatorname{allow} ()\rfloor$).
\item A policy denying everything, written as $D_f\ap f$, or $D_U$ if
the additional output is unit.
\end{itemize}
The most often used approach to define individual rules is to define a
rule as a refinement of one of the elementary policies, by using a
domain restriction. As an example,
\begin{gather*}
\bigl\{(\operatorname{Alice}, \operatorname{obj1},
\operatorname{read})\bigr\} \triangleleft A_U
\end{gather*}
Finally, rules can be combined to policies in three different ways:
\begin{itemize}
\item Override operators: used for policies of the same type, written
as $\_ \oplus_i \_$.
\item Parallel combination operators: used for the parallel
composition of policies of potentially different type, written as
$\_ \otimes_i \_$.
\item Sequential combination operators: used for the sequential
composition of policies of potentially different type, written as
$\_ \circ_i \_$.
\end{itemize}
All three combinators exist in four variants, depending on how the
decisions of the constituent policies are to be combined. For example,
the $\_ \prodTwo \_$ operator is the parallel combination operator where the
decision of the second policy is used.
Several interesting algebraic properties are proved for UPF
operators. For example, distributivity
\begin{gather*}
( P_1 \oplus P_2) \otimes P_3 = ( P_1 \otimes P_3) \oplus ( P_2 \otimes P_3)
\end{gather*}
Other UPF concepts are introduced in this paper on-the-fly when
needed.

146
document/root.bib
View File

@ -251,4 +251,150 @@
year = {2015},
}
@Book{ spivey:z-notation:1992,
bibkey = {spivey:z-notation:1992},
author = {J. M. Spivey},
title = {The {Z} Notation: A Reference Manual},
publisher = pub-prentice,
address = pub-prentice:adr,
edition = {2nd},
length = 150,
year = 1992,
isbn = {0-139-78529-9},
acknowledgement={brucker, 2007-04-23},
abstract = {This is a revised edition of the first widely available
reference manual on Z originally published in 1989. The
book provides a complete and definitive guide to the use of
Z in specifying information systems, writing specifications
and designing implementations. \par Contents: Tutorial
introduction; Background; The Z language; The mathematical
tool-kit; Sequential systems; Syntax summary; Changes from
the first edition; Glossary.}
}
@InCollection{ brucker.ea:hol-testgen-fw:2013,
abstract = { The \testgen environment is conceived as a system for
modeling and semi-automated test generation with an
emphasis on expressive power and generality. However, its
underlying technical framework Isabelle/\acs{hol} supports the
customization as well as the development of highly
automated add-ons working in specific application domains.
In this paper, we present \testgen/fw, an add-on for the
test framework \testgen, that allows for testing the
conformance of firewall implementations to high-level
security policies. Based on generic theories specifying a
security-policy language, we developed specific theories
for network data and firewall policies. On top of these
firewall specific theories, we provide mechanisms for
policy transformations based on derived rules and adapted
code-generators producing test drivers. Our empirical
evaluations shows that \testgen/fw is a competitive
environment for testing firewalls or high-level policies of
local networks. },
keywords = {symbolic test case generations, black box testing, theorem
proving, network security, firewall testing, conformance
testing},
location = {Shanghai},
author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
booktitle = {International Colloquium on Theoretical Aspects of
Computing (\acs{ictac})},
language = {USenglish},
publisher = pub-springer,
series = s-lncs,
number = 8049,
doi = {10.1007/978-3-642-39718-9_7},
editor = {Zhiming Liu and Jim Woodcock and Huibiao Zhu},
title = {HOl-TestGen/FW: An Environment for Specification-based
Firewall Conformance Testing},
categories = {holtestgen},
classification= {conference},
areas = {security, formal methods},
public = {yes},
year = 2013,
pages = {112--121},
isbn = {978-3-642-39717-2},
}
@Article{ brucker.ea:theorem-prover:2012,
author = {Achim D. Brucker and Burkhart Wolff},
journal = j-fac,
publisher = pub-springer,
language = {USenglish},
categories = {holtestgen},
title = {On Theorem Prover-based Testing},
year = 2013,
issn = {0934-5043},
pages = {683--721},
volume = 25,
number = 5,
classification= {journal},
areas = {formal methods, software},
public = {yes},
doi = {10.1007/s00165-012-0222-y},
keywords = {test case generation, domain partitioning, test sequence,
theorem proving, \testgen},
abstract = {\testgen is a specification and test case generation
environment extending the interactive theorem prover
Isabelle/\acs{hol}. As such, \testgen allows for an integrated
workflow supporting interactive theorem proving, test case
generation, and test data generation.
The \testgen method is two-staged: first, the original
formula is partitioned into test cases by transformation
into a normal form called test theorem. Second, the test
cases are analyzed for ground instances (the test data)
satisfying the constraints of the test cases. Particular
emphasis is put on the control of explicit test-hypotheses
which can be proven over concrete programs.
Due to the generality of the underlying framework, our
system can be used for black-box unit, sequence, reactive
sequence and white-box test scenarios. Although based on
particularly clean theoretical foundations, the system can
be applied for substantial case-studies. },
}
@InProceedings{ brucker.ea:model-based:2011,
title = {An Approach to Modular and Testable Security Models of
Real-world Health-care Applications},
author = {Achim D. Brucker and Lukas Br{\"u}gger and Paul Kearney
and Burkhart Wolff},
booktitle = conf-sacmat,
language = {USenglish},
publisher = pub-acm,
location = {Innsbruck, Austria},
categories = {holtestgen},
classification= {conference},
areas = {security, formal methods},
year = 2011,
copyright = {\acs{acm}},
copyrighturl = {http://dl.acm.org/authorize?431936},
public = {yes},
pages = {133--142},
abstract = {We present a generic modular policy modelling framework
and instantiate it with a substantial case study for
model-based testing of some key security mechanisms of
applications and services of the NPfIT. NPfIT, the National
Programme for \acs{it}, is a very large-scale development project
aiming to modernise the \acs{it} infrastructure of the \acs{nhs} in
England. Consisting of heterogeneous and distributed
applications, it is an ideal target for model-based testing
techniques of a large system exhibiting critical security
features.
We model the four information governance principles,
comprising a role-based access control model, as well as
policy rules governing the concepts of patient consent,
sealed envelopes and legitimate relationship. The model is
given in \acs{hol} and processed together with suitable test
specifications in the \testgen system, that generates
test sequences according to them. Particular emphasis is
put on the modular description of security policies and
their generic combination and its consequences for
model-based testing.},
doi = {10.1145/1998441.1998461},
isbn = {978-1-4503-0688-1},
}

39
document/root.tex
View File

@ -15,6 +15,7 @@
\usepackage{stmaryrd}
\usepackage{paralist}
\usepackage{xspace}
\usepackage{amsmath}
\usepackage[USenglish]{babel}
\newcommand{\testgen}{HOL-TestGen\xspace}
\newcommand{\testgenFW}{HOL-TestGen/FW\xspace}
@ -24,8 +25,42 @@
\sloppy
\usepackage{amssymb}
\newcommand{\isadefinition} {{\operatorname{definition}}}
\newcommand{\types} {{\operatorname{type\_synonym}}}
\newcommand{\datatype} {{\operatorname{datatype}}}
\newcommand{\ap}{\,}
\newcommand{\dom}{\mathrm{dom}}
\newcommand{\ran}{\mathrm{ran}}
\newcommand{\ofType}{\!::\!}
\newcommand{\HolBin}[0]{\ensuremath{\mathrm{bin}}}
\newcommand{\HolNum}[0]{\ensuremath{\mathrm{num}}}
\newcommand{\HolBoolean}[0]{\ensuremath{\mathrm{bool}}}
\newcommand{\HolString}[0]{\ensuremath{\mathrm{string}}}
\newcommand{\HolInteger}[0]{\ensuremath{\mathrm{int}}}
\newcommand{\HolNat}[0]{\ensuremath{\mathrm{nat}}}
\newcommand{\HolReal}[0]{\ensuremath{\mathrm{real}}}
\newcommand{\HolSet}[1]{#1\ap\ensuremath{\mathrm{set}}}
\newcommand{\HolList}[1]{#1\ap\ensuremath{\mathrm{list}}}
%\newcommand{\HolOrderedSet}[1]{#1~\ensuremath{\mathrm{orderedset}}}
\newcommand{\HolMultiset}[1]{#1\ap\ensuremath{\mathrm{multiset}}}
\newcommand{\classType}[2]{#1\ap\ensuremath{\mathrm{#2}}}
\newcommand{\bottom}{\bot}
\DeclareMathOperator{\HolSome}{Some}
\DeclareMathOperator{\HolNone}{None}
\DeclareMathOperator{\Poverride}{\oplus}
\DeclareMathOperator{\prodTwo}{\otimes_2}
\newcommand{\HolMkSet}[1]{\operatorname{set} #1}
\newcommand{\spot}{.\;}
\newcommand{\where} {{\operatorname{where}}}
\DeclareMathOperator{\HolIf}{if}
\DeclareMathOperator{\HolLet}{let}
\DeclareMathOperator{\HolIn}{in}
\DeclareMathOperator{\HolThen}{then}
\DeclareMathOperator{\HolElse}{else}
\newcommand{\isasymmodels}{\isamath{\models}}
\newcommand{\HOL}{HOL}
@ -81,9 +116,7 @@
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. Thus, its
abstraction level differs from Diekmann's Network Security
Policy Verification formalization
modeling application level protocols on top of tcp/ip.
}
}