From 73bc5df9fc5c58c192d4e6def9cc2c257383479a Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 4 Jan 2017 14:58:02 +0000 Subject: [PATCH] Added introduction. --- document/introduction.tex | 164 +++++++++++++++++++++++++++++++++++--- document/root.bib | 146 +++++++++++++++++++++++++++++++++ document/root.tex | 39 ++++++++- 3 files changed, 335 insertions(+), 14 deletions(-) diff --git a/document/introduction.tex b/document/introduction.tex index 2af25f0..820a34e 100644 --- a/document/introduction.tex +++ b/document/introduction.tex @@ -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. diff --git a/document/root.bib b/document/root.bib index 2e5bc1d..ea316ba 100644 --- a/document/root.bib +++ b/document/root.bib @@ -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}, +} + diff --git a/document/root.tex b/document/root.tex index 7e19ba1..66c21df 100644 --- a/document/root.tex +++ b/document/root.tex @@ -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. } }