J Autom Reasoning
https://doi.org/10.1007/s10817-017-9445-1
Verified iptables Firewall Analysis and Verification
Cornelius Diekmann
1
· Lars Hupel
1
· Julius Michaelis
1
·
Maximilian Haslbeck
1
· Georg Carle
1
Received: 31 March 2017 / Accepted: 14 December 2017
© The Author(s) 2018. This article is an open access publication
Abstract This article summarizes our efforts around the formally verified static analysis of
iptables rulesets using Isabelle/HOL. We build our work around a formal semantics of the
behavior of iptables firewalls. This semantics is tailored to the specifics of the filter table and
supports arbitrary match expressions, even new ones that may be added in the future. Around
that, we organize a set of simplification procedures and their correctness proofs: we include
procedures that can unfold calls to user-defined chains, simplify match expressions, and
construct approximations removing unknown or unwanted match expressions. For analysis
purposes, we describe a simplified model of firewalls that only supports a single list of rules
with limited expressiveness. We provide and verify procedures that translate from the complex
iptables language into this simple model. Based on that, we implement the verified generation
of IP space partitions and minimal service matrices. An evaluation of our work on a large
set of real-world firewall rulesets shows that our framework provides interesting results in
many situations, and can both help and out-compete other static analysis frameworks found
in related work.
This work has been supported by the European Commission, project SafeCloud, Grant 653884; German
Federal Ministry of Education and Research (BMBF), EUREKA project SASER, Grant 16BP12304, and
SENDATE, Grant 16KIS0472.
B
Lars Hupel
lars.hupel@tum.de
Cornelius Diekmann
diekmann@net.in.tum.de
Julius Michaelis
michaeli@in.tum.de
Maximilian Haslbeck
haslbecm@in.tum.de
Georg Carle
carle@net.in.tum.de
1
Department of Informatics, Technical University of Munich, Boltzmannstr. 3, Garching bei München,
Germany
123
C. Diekmann et al.
Keywords Computer networks · Firewalls · Isabelle · Netfilter · Iptables · Semantics ·
Formal verification
1 Introduction
Firewalls are a fundamental security mechanism for computer networks. Several firewall
solutions, ranging from open source [66,78,79] to commercial [14,37], exist. Operating and
managing firewalls is challenging as rulesets are usually written manually. While vulnera-
bilities in firewall software itself are comparatively rare, it has been known for over a decade
[82] that many firewalls enforce poorly written rulesets. However, the prevalent methodology
for configuring firewalls has not changed. Consequently, studies regularly report insufficient
quality of firewall rulesets [25,36,47,54,74,81,8486].
The predominant firewall of Linux is iptables [78]. In general, an iptables ruleset is pro-
cessed by the Linux kernel for each packet comparably to a batch program: rules are evaluated
sequentially, but the action (sometimes called target) is only applied if the packet matches
the criteria of the rule. A list of rules is called a chain. Ultimately, the Linux kernel needs to
determine whether to ACCEPT or DROP the packet, hence, those are the common actions.
Further possible actions include jumping to other chains and continue processing from there.
As an example, we use the firewall rules in Fig. 1, taken from an NAS (network-attached
storage) device. The ruleset reads as follows: processing starts at the INPUT chain. In the
first rule, all incoming packets are sent directly to the user-defined DOS_PROTECT chain,
where some rate limiting is applied. A packet which does not exceed certain limits can make
it through this chain without getting DROPped by RETURNing back to the second rule of the
INPUT chain. In this second rule, the firewall allows all packets which belong to already
ESTABLISHED (or RELATED) connections. This is generally considered good practice.
Often, the ESTABLISHED rule accepts most packets and is placed at the b eginning of a
ruleset for performance reasons. However, it is barely interesting for the actual policy (“who
may connect to whom”) enforced by the firewall. The interesting aspect is when a firewall
accepts a packet which does not yet belong to an established connection. Once a packet is
accepted, further packets for this connection are treated as ESTABLISHED. In the example,
Chain INPUT (policy ACCEPT)
target prot source destination
DOS_PROTECT all 0.0.0.0/0 0.0.0.0/0
ACCEPT all 0.0.0.0/0 0.0.0.0/0 state RELATED,ESTABLISHED
DROP tcp 0.0.0.0/0 0.0.0.0/0 tcp dpt:22
DROP tcp 0.0.0.0/0 0.0.0.0/0 multiport dports 21,873,5005,5006,80,
548,111,2049,892
DROP udp 0.0.0.0/0 0.0.0.0/0 multiport dports 123,111,2049,892,5353
ACCEPT all 192.168.0.0/16 0.0.0.0/0
DROP all 0.0.0.0/0 0.0.0.0/0
Chain DOS_PROTECT (1 references)
target prot source destination
RETURN icmp 0.0.0.0/0 0.0.0.0/0 icmptype 8 limit: avg 1/sec burst 5
DROP icmp 0.0.0.0/0 0.0.0.0/0 icmptype 8
RETURN tcp 0.0.0.0/0 0.0.0.0/0 tcp flags:0x17/0x04 limit: avg 1/sec burst 5
DROP tcp 0.0.0.0/0 0.0.0.0/0 tcp flags:0x17/0x04
RETURN tcp 0.0.0.0/0 0.0.0.0/0 tcp flags:0x17/0x02 limit: avg 10000/sec
burst 100
DROP tcp 0.0.0.0/0 0.0.0.0/0 tcp flags:0x17/0x02
Fig. 1 Linux iptables ruleset of a Synology NAS (network attached storage) device
123
Verified iptables Firewall Analysis and Verification
the subsequent rules are the interesting ones which shape the firewall’s connectivity policy.
There, some services, identified by their ports, are blocked (and any packets with those
destination ports will never create an established connection). Finally, the firewall allows all
packets from the local network 192.168.0.0/16 and discards all other packets.
Several tools [4749,54,59,69,80,85] have been developed to ease firewall management
and reveal configuration errors. Many tools are not designed for iptables directly, but are
based on a generic firewall model. When we tried to analyze real-world iptables firewalls
with the publicly available static analysis tools, none of them could handle the rulesets. Even
after we simplified the firewall rulesets, we found that tools still fail to analyze our rulesets
for the following reasons:
They do not support the vast amount of firewall features,
Their firewall model is too simplistic,
They require the administrator to learn a complex query language which might be more
complex than the firewall language itself,
The analysis algorithms do not scale to large firewalls, or
The output of the (unverified) verification tools itself cannot be trusted.
To illustrate the problem, we decided to use ITVal [48] because it natively supports iptables,
is open source, and supports calls to user-defined chains. However, ITVal’s firewall model is
representative of the model used by the majority of tools; therefore, the problems described
here also apply to a large class of other tools. Firewall models used in related work are
surveyed in Sect. 3.1.
We used ITVal to partition the IP space of Fig. 1 into equivalence classes (i.e., ranges with
the same access rights) [49]. The expected result is a set of two IP ranges: the local network
192.168.0.0/16 and the “rest”. However, ITVal erroneously only reports one IP range: the
universe. Removing the first two rules (in particular the call in the DOS_PROTECT chain)
lets ITVal compute the expected result.
We identified two concrete issues which prevent tools from “understanding” real-world
firewalls. First, calling and returning from custom chains, due to the possibility of complex
nested chain calls. Second, more seriously, most tools do not understand the firewall’s match
conditions. In the above example, the rate limiting is not understood. An ad-hoc implemen-
tation of rate limiting for the respective tool might not be possible, because the underlying
algorithm might not be capable of dealing with this special case. Even so, this would not
solve the general problem of unknown match conditions. Firewalls, such as iptables, support
numerous match conditions and several new ones are added in every release. As of version
1.6.0 (Linux kernel 4.10, early 2017), iptables supports more than 60 match conditions with
over 200 individual options. We expect even more match conditions for nftables [79]inthe
future since they can be written as simple userspace programs [45]. Therefore, it is virtu-
ally impossible to write a tool which understands all possible match conditions. Combined
with the fact that in production networks, huge, complex, and legacy firewall rulesets have
evolved over time, this poses a particular challenge. Our methodology to tackle this can also
be applied to firewalls with simpler semantics, or younger technology with fewer features,
e.g., Cisco IOS Access Lists or filtering OpenFlow flow tables (Sect. 15).
In this article, we first build a fundamental prerequisite to enable tool-supported analysis
of real-world firewalls: we present several steps of semantics-preserving ruleset simplifica-
tion, which lead to a ruleset that is “understandable” to subsequent analysis tools: first, we
unfold all calls to and returns from user-defined chains. This process is exact and valid for
arbitrary match conditions. Afterwards, we process unknown match conditions. For that, we
embed a ternary-logic semantics into the firewall’s semantics. Due to ternary logic, all match
123
C. Diekmann et al.
conditions not understood by subsequent analysis tools can be treated as always yielding
an unknown result. In a next step, all unknown conditions can be removed. This introduces
an over- and underapproximation ruleset, called upper/lower closure. Guarantees about the
original ruleset dropping/allowing a packet can be given by using the respective closure
ruleset.
To summarize, we provide the following contributions for simplifying iptables rulesets:
1. A formal semantics of iptables packet filtering (Sect. 4)
2. Chain unfolding: transforming a ruleset in the complex chain model to a ruleset in the
simple list model (Sect. 5)
3. An embedded semantics with ternary logic, supporting arbitrary match conditions,
introducing a lower/upper closure of accepted packets (Sect. 6)
4. Normalization and translation of complex logical expressions to an iptables-compatible
format, discovering a meta-logical firewall algebra (Sect. 7)
We give a small intermediate evaluation to demonstrate these generic ruleset preprocessing
steps (Sect. 8). Afterwards, we use these preprocessing steps to build a fully-verified iptables
analysis and verification tool on top. In detail, our further contributions are:
5. A simple firewall model, designed for mathematical beauty and ease of static analysis
(Sect. 9)
6. A method to translate real-world firewall rulesets into this simple model (Sect. 10),
featuring a series of translation steps to transform, rewrite, and normalize primitive
match conditions (Sect. 11)
7. Static and automatic firewall analysis methods, based on the simple model (Sect. 12),
featuring
IP address space partitioning
Minimal service matrices
8. Our stand-alone, administrator-friendly tool fffuu (Sect. 13)
9. Evaluation on large real-world data set (Sect. 14)
10. Full formal and machine-verifiable proof of correctness with Isabelle/HOL (Sect. 17)
2 Background: Formal Verification with Isabelle
We verified all proofs with Isabelle [63], using its standard Higher-Order Logic (HOL).
Isabelle is a proof assistant in the LCF tradition: the system is based on a small and
well-established kernel. All higher-level specification and proof tools, e.g., for inductive
predicates, functional programs, or proof search, have to go through this kernel. Therefore,
the correctness of all obtained results only depends on the correctness of this kernel and the
iptables semantics (Fig. 2).
The full formalization containing a set of Isabelle theory files is publicly available. An
interested reader may consult the detailed (100+ pages) proof document. For brevity, we
usually omit proofs in this article, but point the reader with a footnote to the corresponding
part of the formalization. Section 17 points the reader to our Isabelle formalization and further
accompanying material.
Notation. We use pseudo code close to SML and Isabelle. Function application is written
without parentheses, e.g., fadenotes function f applied to parameter a.Wewrite:: for
prepending a single element to a list, e. g., a :: b :: [c, d]=[a, b, c, d],and::: for appending
lists, e. g., [a, b] ::: [c, d]=[a, b, c, d]. The empty list is written as []. [ fa. a l] denotes
123
Verified iptables Firewall Analysis and Verification
a list comprehension, i.e., applying f to every element a of list l. [ fxy. x l
1
, y l
2
]
denotes the list comprehension where f is applied to each combination of elements of the
lists l
1
and l
2
.For fxy= (x, y), this yields the Cartesian product of l
1
and l
2
.
Whenever we refer to specific iptables options or modules, we set them in typewriter
font. The iptables options can be looked up in the respective man pages iptables(8) and
iptables-extensions(8).
3 Related Work
We first survey the common understanding of firewalls in the literature and present specific
static firewall analysis tools afterwards.
3.1 Firewall Models
Packets are routed through the firewall and the firewall needs to decide whether to a llow or
deny a packet. The firewall’s ruleset determines its filtering behavior. The firewall inspects
its ruleset for each single packet to determine the action to apply to the packet. The ruleset
can be viewed as a list of rules; usually it is processed sequentially and the first matching
rule is applied.
The literature agrees on the definition of a single firewall rule. It consists of a predicate
(the match expression) and an action. If the match expression applies to a packet, the action is
performed. Usually, a packet is scrutinized by several rules. Zhang et al. [86] specify a com-
mon format for packet filtering rules. The action is either “allow” or “deny”, which directly
corresponds to the firewall’s filtering decision. The ruleset is processed strictly sequentially,
no jumping between chains is possible. Yuan et al. [85] call this the simple list model.ITVal
also supports calls to user-defined chains as an action. This allows “jumping” within the
ruleset without having a final filtering decision yet. This is called the complex chain model
[85].
In general, a packet header is a bitstring which can be matched against [87]. Zhang et al.
[86] support matching on the following packet header fields: IP source and destination
address, protocol, and port on layer 4. This model is commonly found in the literature
[6,9,10,69,85,86]. ITVal extends these match conditions with flags (e. g., TCP SYN)and
connection states (INVALID, NEW, ESTABLISHED, RELATED). The state matching is
treated as just another match condition.
1
This model is similar to Margrave’s model for IOS
[54]. When comparing these features to the simple firewall in Fig. 1, it becomes obvious that
none of these tools supports that firewall directly.
We are not the first to propose simplifying firewall rulesets to enable subsequent analysis.
Brucker et al. [8,10,11] provide algorithms to generate test cases from a firewall policy. A
firewall policy in their model is a list of rules on disjoint networks. A rule is a partial function
from packets to decisions, e.g., allow or deny. To keep the number of test cases manageable,
the firewall ruleset is first simplified while preserving the original behavior. The correctness of
1
Firewalls can be stateful or stateless. Most current firewalls are stateful, which means the firewall remembers
and tracks information of previously seen packets, e. g., the TCP connection a packet belongs to and the state
of that connection (“conntrack” in iptables parlance). ITVal does not track the state of connections. Match
conditions on connection states are treated exactly the same as matches on a packet header. In general, by
focusing on rulesets and not firewall implementation, matching on conntrack states is exactly like matching
on any other (stateless) condition. However, internally in the firewall, not only the packet header is consulted
but also the current connection tables. Note that existing firewall analysis tools also largely ignore state [54].
In our semantics, we also model stateless matching.
123
C. Diekmann et al.
these transformations is proved with Isabelle/HOL. With regard to low-level firewall features,
the instantiation used by Brucker et al. in their evaluation is more limited than the model used
by the tools presented above. This is not a limitation since their framework is designed to
support different firewall technologies by having a more abstract and generic policy model.
Yet, it demonstrates that our tool as a preprocessor to transform low-level iptables rules to a
generic firewall model is a useful building block. In general, using our tool as preprocessor
can make firewall analysis tools from related work available for iptables.
We are not aware of any tool which uses a model fundamentally different than those
described here. Our model enhances existing work in that we use ternary logic to support
arbitrary match conditions. To analyze a large iptables firewall, the authors of Margrave [54]
translated it to basic Cisco IOS access lists [14] by hand. With our simplification, we can
automatically remove all features not understood by basic Cisco IOS. This enables translation
of any iptables firewall to basic Cisco access lists which is guaranteed to drop no more packets
than the original iptables firewall. This opens up all tools available only for Cisco IOS access
lists, e.g., Margrave [54] and Header Space Analysis [41].
2
3.2 Static Firewall Analysis Tools
Popular tools for static firewall analysis include FIREMAN [85], Capretta et al. [13], and
the Firewall Policy Advisor [2]. They can use the following features to match on packets: IP
addresses, ports, and protocol. However, most real-world firewall rulesets we found in our
evaluation use many more features. As can be seen in Fig. 1, among others, iptables supports
matching on source IP address, layer 4 port, inbound interface, conntrack state, entries and
limits in the recent list. Hence, these tools would not be applicable (without our generic
preprocessing) to most firewalls from our evaluation.
Most aforementioned tools allow detecting conflicts between rules to uncover configura-
tion mistakes. Since our approach rewrites rules to a simpler form and the provenance and
relation of the simplified rules to the original ruleset is lost, our approach does not support
this. However, we offer service matrices (Sect. 12.2) to provide a general overview of the
firewall’s filtering behavior.
The work most similar to our static analysis tool, in particular to our IP address space
partitioning, is ITVal [48]: it supports a large set of iptables features and can compute an
IP address space partition [49]. ITVal, as an academic prototype, only supports IPv4, is not
formally verified, and its implementation contains several errors. For example, ITVal produces
spurious results if the number of significant bits in IP addresses in CIDR notation [31] is not
a multiple of 8. It does not consider logical negations which may occur when RETURNing
prematurely from user-defined chains, which leads to wrong interpretation of complement
sets. It does not support abstracting over unknown match conditions but simply ignores them,
which also leads to spurious results. Anecdotally, we uncovered these corner cases when we
tried to prove the correctness of our algorithms and Isabelle was presenting unexpected
proof obligations. Without the formal verification, our tool would likely contain similar
errors. For rulesets with more than 1000 rules, ITVal requires tens of GBs of memory. We are
uncertain whether this is a limitation of its internal data structure or just a simple memory leak.
ITVal neither proves the soundness nor the minimality of its IP address range partitioning.
Nevertheless, ITVal shows the need for and the use of IP address range partitioning and
has demonstrated that its implementation works well on rulesets which do not trigger the
2
Note that the other direction is considered easy [71], because basic Cisco IOS access lists have “no nice
features” [32]. Also note that there also are Advanced Access Lists.
123
Verified iptables Firewall Analysis and Verification
aforementioned errors. Our tool strongly builds on the ideas of ITVal, but with a different
algorithm.
Exodus [57] translates existing device configurations to a simpler model, similar to our
translation step. It translates router configurations to a high-level SDN controller program,
which is implemented on top of OpenFlow. Exodus supports many Cisco IOS features. The
translation problem solved by Exodus is comparable to this article’s problem of translating to
a simple firewall model: OpenFlow 1.0 only supports a limited set of features (comparable to
our simple firewall) whereas IOS supports a wide range of features (comparable to iptables). A
complex language is ultimately translated to a simple language, which is the ‘hard’ direction.
Since our approach loses the relation of the simplified rules to the original ruleset, our
approach cannot point to individual flawed firewall rules, but only provides a complete
overview. For example, our tool reduces thousands of firewall rules to the easy-to-understand
graphinFig.8, but the information which initial firewall rules and match conditions are
responsible for each edge of the graph is lost. Complementary to our verification tool, and
well-suited for debugging and uncovering responsible misbehaving rules, is Margrave [54].
Margrave can be used to query firewalls and to troubleshoot configurations or to show the
impact of ruleset edits. Margrave can find scenarios, i. e., it can show concrete packets which
violate a security policy. Our framework does not show such information. Margrave’s query
language, which a potential user has to learn, is based on first-order logic.
All these tools have one limitation in common: they do not understand all iptables match
conditions. Our generic ruleset preprocessing algorithms help to make a ruleset accessible for
the respective tool. However, our generic algorithms still lose too much information. This is
because iptables conditions are also related to each other. For example, the iprange mod-
ule allows to write down IP address ranges using a notation more expressive than most tools
support. Just removing iprange matches would lose too much information, since tools
understand matches on IP address ranges in a simpler format. We need to rewrite iprange
expressions to a simpler, semantics-preserving notation of IP addresses, commonly under-
stood by tools. This may be non-trivial since one rule with one iprange expression may
correspond to several rules with only simple matches on IP addresses. As a more involved
example, we saw that most firewall analysis tools do not support matching on interfaces. But
given that a firewall implements spoofing protection and the routing tables are known, con-
ditions matching on network interfaces can be rewritten to those matching on IP addresses.
After an intermediate evaluation (Sect. 8), we present in Sect. 11 algorithms to overcome
these issues for the most common match conditions.
4 Semantics of iptables
We formalized the semantics of a subset of iptables. The semantics focuses on access control,
which is done in the INPUT, OUTUT,andFORWARD chain of the filter table. Thus packet
modification (e.g., NAT) is not considered (and also not allowed in these chains).
Match conditions, e. g., source 192.168.0.0/24 and protocol TCP, are called
primitives. A primitive matcher γ decides whether a packet matches a primitive. Formally,
basedonasetX of primitives and a set of packets P, a primitive matcher γ is a binary relation
over X and P. The semantics supports arbitrary packet models and match conditions, hence
both remain abstract in our definition.
In one firewall rule, several primitives can be specified. Their logical connective is con-
junction, for example src 192.168.0.0/24 and tcp. Disjunction is omitted because
123
C. Diekmann et al.
it is neither needed for the formalization nor supported by the iptables user interface; this
is consistent with the model by Jeffrey and Samak [39]. Primitives can be combined in an
algebra of match expressions M
X
:
mexpr = x for x X mexpr | mexpr mexpr | Any
The match expression Any matches any packet. For a primitive matcher γ and a match
expression m M
X
,wewritematch γ mpif a packet p P matches m, essentially lifting
γ to a relation over M
X
and P, with the connectives defined as usual. With completely generic
P, X ,andγ , the semantics can be considered to have access to an oracle which understands
all possible match conditions.
Furthermore, we support the following actions, modeled closely after iptables: Accept,
Reject, Drop, Log, Empty, Call c for a chain c ,andReturn.Arule can be defined
as a tuple (m, a) for a match expression m and an action a. A list (or sequence) of rules
is called a chain. For example, the beginning of the DOS_PROTECT chain in Fig. 1 is
[(icmp icmptype 8 limit: ..., Return), ...].
A set of named chains is called a ruleset.LetΓ denote the mapping from chain names to
chains. For example, Γ DOS_PROTECT returns the contents of the DOS_PROTECT chain.
We assume that Γ is well-formed, that is, if a Call c action occurs in a ruleset, then the
chain named c is defined in Γ . This assumption is justified, because the Linux kernel only
accepts well-formed rulesets.
4.1 Inductive Definition
The semantics of a firewall wrt a given packet p, a background ruleset Γ ,andaprimitive
matcher γ can be defined as a relation over the currently active chain and the state before
and the state after processing this chain. The semantics is specified in Fig. 2.
3
The judge-
ment Γ,γ, p
rs, t
t
states that starting with state t, after processing the chain rs,
the resulting state is t
. For a packet p, our semantics focuses on firewall filtering decisions.
Therefore, only the following three states are necessary: the firewall may allow (
)ordeny
(
) the packet, or it may not have come to a decision yet (
?
).
We will now discuss the most important rules.
Accept If the packet p matches the match expression m, then the firewall with
no filtering decision (
?
) processes the singleton chain [(m, Accept)] by
switching to the allow state.
Drop/Reject Both actions deny a packet. The difference lies in whether the firewall
generates some informational message, which does not influence filtering.
NoMatch If the firewall has not come to a filtering decision yet it can process any
non-matching rule without changing its state.
Decision As soon as the firewall made a filtering decision, all remaining rules can
be skipped. Given determinism (Theorem 2), this means that once decided,
the firewall does not change its filtering decision of
or
.
Seq If the firewall has not come to a filtering decision and it processes the chain
rs
1
, which results in state t and starting from t processes the chain rs
2
,
which results in state t
, then both chains can be processed sequentially,
ending in state t
.
CallResult If a matching Call to a chain named c occurs, the resulting state t is the
result of processing the chain Γ c.
3
Formalization: inductive iptables_bigstep [19].
123
Verified iptables Firewall Analysis and Verification
Γ, γ, p
[],t
t
Skip
match γmp
Γ, γ, p
[(m, Accept)],
?
Accept
match γmp
Γ, γ, p
[(m, Drop)],
?
Drop
match γmp
Γ, γ, p
[(m, Reject)],
?
Reject
¬ match γmp
Γ, γ, p
[(m, a)],
?
?
NoMatch
t =
?
Γ, γ, p
rs,t
t
Decision
Γ, γ, p
rs
1
,
?
,γ,p
rs
2
,t
t
Γ, γ, p
rs
1
::: rs
2
,
?
t
Seq
match γ m p Γ,p
Γc,
?
t
Γ, γ, p
[(m, Call c)],
?
t
CallResult
match γm
c= rs
1
::: (m
, Return)::rs
2
match γmp Γ,γ,p
rs
1
,
?
?
Γ, γ, p
[(m, Call c)],
?
?
CallReturn
match γmp
Γ, γ, p
[(m, Log)],
?
?
Log
match γmp
Γ, γ, p
[(m, Empty)],
?
?
Empty
(for any primitive matcher γ and any well-formed ruleset Γ )
Fig. 2 Big-step semantics for iptables
CallReturn Likewise, if processing a prefix rs
1
of the called chain does not lead to a
filtering decision and directly afterwards, a matching Return rule occurs,
the called chain is processed without result.
Log/Empty Neither rule influences the filtering behavior. An Empty rule,i.e.,arule
without an action, is sometimes used by administrators to have iptables
only update its internal state, e.g., updating packet counters.
The semantics is carefully designed to not require a call stack. The format of the Call-
Return rule is part of this design: if we tried to introduce a rule that allows to process
a Return without either processing its matching Call or manipulating some call stack,
we would necessarily cause problems with the Seq rule. This is because a separated rule for
Return would need to remain in the
?
state, and a later rule from the same chain (where we
should already have returned from) could then switch to a decision state. One way of avoiding
this problem is to merge the functionality of the Seq and Decision rules into all other rules.
After doing so, one can introduce a separate Return rule and additionally remove the initial
state, since it would always be
?
. An example set of productions for such an a lternate formu-
lation is shown in Fig. 3. For the practical implementation of our proofs, this alternative lacks
flexibility: since the Seq rule is no longer applicable, we cannot easily separate arguments
about lists of rules from arguments about the different action types of rules. We provide this
as an equivalent
4
alternative because we hope that can provide additional confidence in the
correctness of our semantics:
Theorem 1 (Equivalence of the two Semantics) If no call to c occurs in any of the chains
of Γ and default-policy is either Accept or Drop,then
4
Formalization: theorem iptables_bigstep_r_eq.
123
C. Diekmann et al.
match γmp
Γ, γ, p (m, Accept)::rs
Accept
match γmp
Γ, γ, p (m, Return)::rs
?
Return
match γmp
Γ, γ, p (m, Drop)::rs
Drop
match γmp
Γ, γ, p (m, Reject)::rs
Reject
¬ match γmp Γ,γ,prs t
Γ, γ, p (m, a)::rs t
NoMatch
Γ, γ, p []
?
Skip
match γmp Γ,γ,pΓc tt
,
Γ, γ, p (m, Call c)::rs t
CallResult
Γ, γ, p Γc
?
Γ, γ, p rs t
Γ, γ, p (m, Call c)::rs t
CallNoResult
Γ, γ, p rs t
Γ, γ, p (m, Log)::rs t
Log
Γ, γ, p rs t
Γ, γ, p (m, Empty)::rs t
Empty
(for any primitive matcher γ and any well-formed ruleset Γ )
Fig. 3 Alternative big-step semantics for iptables
Γ,γ, p [
(
m, Call c
)
,(Tr u e , default-policy)]⇒t
←→
Γ,γ, p
[
(
m, Call c
)
,(Tr u e , default-policy)],
?
t
Note that for finite rulesets (i. e., the image/range of Γ is finite), we can always find a c such
that no call occurs to it. In practice, we will chose c to be INPUT, FORWARD,orOUTPUT.
The Linux kernel rejects rulesets where a user calls these chains directly.
4.2 Model Limitations and Stateful Matchers
Our primitive matcher is completely stateless: γ ::
(
X P B
)
. However, iptables also
allows stateful operations, such as marking a packet, and, later on, matching on the marking.
The documentation of iptables distinguishes between match extensions and target exten-
sions. Ideally, almost all match extensions can be used as if they were stateless. Anything
which performs an action should be implemented as target extension, i. e., action. For exam-
ple, marking a packet with CONNMARK is an action. Matching on a CONNMARK marking
is a match condition. Our semantics does not support the CONNMARK action. This is not a
problem since usually, new CONNMARK markings are not set in the filter table. However,
it is possible to match on existing markings. Since our primitive matchers and packets are
completely generic, this case can be represented within our semantics: instead of keeping
an internal CONNMARK state, an additional “ghost field” must be introduced in the packet
model. Since packets are immutable, this field cannot be set by a rule, but the packet must
be given to the firewall with the final value of the ghost field already set. Hence, an analysis
must be carried out with the correct value in the ghost fields when the packet is given to the
filter table. We admit that this model is very unwieldy in general. However, for one of the
most used stateful modules of iptables, namely connection state tracking with conntrack
123
Verified iptables Firewall Analysis and Verification
and state, this model has been proven to be very convenient.
5
We will elaborate on stateful
connection tracking (which can be fully supported by our semantics) in Sect. 11.2. For future
work, if we want to consider e. g., the raw or mangle table with its extended set of actions
or OpenFlow with its full set of actions, a semantics needs to be designed with a mutable
packet model.
What if a match extension maintains an internal state and changes its behavior on every
invocation? Ideally, due to usability, iptables match extensions should be “purely functional”;
however, the recent and connbytes modules exhibit side effects on their internal state.
As a consequence, the tautology in Boolean logic a ∧¬a = False does not hold if a is
a module which updates an internal state and its matching behavior after every invocation.
Therefore, one might argue that our iptables model can only be applied to stateless match
conditions. If we add some state σ and updated state σ
to the match condition, the formula
a
σ
∧¬a
σ
now correctly represents stateful match conditions. Therefore, it would only
be wrong to perform equality operations on stateful match conditions, but not to model
stateful match conditions with a specific fixed state. To additionally convince the reader of
the soundness of our approach, it would be possible to adapt the parser to give a unique
identifier to every primitive which is not known to be stateless. This identifier represents
the internal state of that particular match condition at that particular position in a ruleset. It
prevents equality operations between multiple invocations of a stateful match condition. This
does not change any of our algorithms.
4.3 Analysis and Use of the Semantics
The subsequent sections of this article are all based on these semantics. Whenever we provide
a procedure P to operate on chains, we proved that the firewall’s filtering behavior is preserved,
formally:
Γ,γ, p
P rs, t
t
iff Γ,γ, p
rs, t
t
All our proofs are machine-verified with Isabelle. Therefore, once the reader is convinced
of the semantics as specified in Fig. 2, the correctness of all subsequent theorems follows
automatically, without any hidden assumptions or limitations.
The rules in Fig. 2 are designed such that every rule can be inspected individually. However,
considering all of them together, it is not immediately clear whether the result depends on the
order of their application to a concrete ruleset and packet. Theorem 2 states that the semantics
is deterministic, i.e., only one uniquely defined outcome is possible.
6
Theorem 2 (Determinism)
If Γ,γ, p
rs, t
t
and Γ,γ, p
rs, t
t

then t
= t

Next, we show that the semantics are actually total, i. e., there is always a decision for any
packet and ruleset.
7
We assume that the ruleset does not have an infinite loop and that all
chains which are called exist in the background ruleset. These conditions are checked by the
Linux kernel and can thus safely be assumed. In addition, we assume that only the actions
defined in Fig. 2 occur in the ruleset; our parser rejects everything else.
5
Formalization: file Semantics_Stateful.thy [19].
6
Formalization: theorem iptables_bigstep_deterministic [19].
7
Formalization: theorem semantics_bigstep_defined [19].
123
C. Diekmann et al.
We start any analysis with [(Any, Call start-chain), (Any, default-policy)],wherethe
default policy is either Accept or Drop. This means that existing top-level Return actions
fall back to the default policy. This is consistent with iptables behavior.
Theorem 3 (Totality) If the caller–callee relation is well-founded (i. e., there are no infinite
calling loops), Γ is well-formed (i. e., all chain names that are called are defined), there is
no Return on top-level, and all actions are supported by the semantics, then
t
,γ,p
rs, t
t
To also assert empirically that we only allow analysis of iptables rulesets which are total
according to our semantics, we always check the preconditions of Theorem 3 at runtime when
our tool loads a ruleset: first, we can statically verify that Γ is well-formed by verifying that
all chain names which are referenced in an action are defined and that no unsupported actions
occur. Next, our tool verifies that there are no infinite loops by unfolding the ruleset (Sect. 5)
only a finite but sufficiently large number of times and aborts if the ruleset is not in the
proper form afterwards. These conditions have only been violated for a negligible fraction
of all real-world firewalls we have analyzed. Those used very special iptables actions
8
not
supported by our semantics or special hand-crafted firewalls which deliberately violate a
property and which are also rejected by the Linux kernel.
5 Custom Chain Unfolding
In this section, we present algorithms to convert a ruleset from the complex chain model to
the simple list model.
The function pr (“process return”) iterates over a chain. If a Return rule is encountered,
all subsequent rules are amended by adding the Return rule’s negated match expression as
a conjunct. Intuitively, if a Return rule occurs in a chain, all following rules of this chain
can only be reached if the Return rule does not match.
add-match m
rs =[(m m
, a). (m, a) rs]
pr [] = []
pr ((m, Return) :: rs) = add-match (¬m)(pr rs)
pr ((m, a) :: rs) = (m, a) :: pr rs
The function pc (“process call”) iterates over a chain, unfolding one level of Call rules.
If a Call to the chain c occurs, the chain itself (i.e., Γ c) is inserted instead of the Call.
However, Returns in the chain need to be processed and the match expression for the
original Call needs to be added to the inserted chain.
pc [] = []
pc ((m, Call c) :: rs) = add-match m
(
pr
(
Γ c
))
::: pc rs
pc ((m,
a) :: rs) = (m, a) :: pc rs
8
For example, setting CONNMARK in the filter table where it was not necessary, redirecting packets to
userspace with NFQUEUE where we do not know how the userspace application handles them, or specialized
loggings such as NFLOG which is technically equivalent to the LOG action and could directly be supported.
123
Verified iptables Firewall Analysis and Verification
[(¬ (icmp icmptype 8 limit: ...) icmp icmptype 8, Drop) ,
(¬ (icmp icmptype 8 limit: ...) ∧¬(tcp tcp flags:0x17/0x04 limit: ...)
tcp tcp flags:0x17/0x04, Drop) ,..., (src 192.168.0.0/16, Accept) , ...]
Fig. 4 Unfolded Synology firewall
The procedure pc can be applied arbitrarily many times and preserves the semantics.
9
Theorem 4 (pc sound and complete)
Γ,γ, p
pc
n
rs, t
t
iff Γ,γ, p
rs, t
t
In each iteration, the algorithm unfolds one level of Calls. The algorithm needs to be
applied until the result no longer changes. Note that the syntax and semantics allow non-
terminating rulesets. However, the only rulesets that are interesting for analysis are the ones
actually accepted by the Linux kernel. Since it rejects rulesets with loops,
10
both our algorithm
and the resulting ruleset are guaranteed to terminate.
Corollary 1 Every ruleset (with only Accept, Drop, Reject, Log, Empty, Call,
Return actions) accepted by the Linux kernel can be unfolded completely while preserving
its filtering behavior.
Since we have not formally verified the Linux kernel sources, Corollary 1 is not formally
proven. It follows from our previous theorems and we have extensively checked it empirically.
In addition to unfolding calls, the following transformations applied to any ruleset preserve
the semantics:
replacing Reject actions with Drop actions,
11
–removingEmpty and Log rules,
12
simplifying match expressions which c ontain Any or ¬ Any,
13
for some given primitive matcher, specific optimizations,
14
e.g., rewriting src
0.0.0.0/0 to Any.
Therefore, after unfolding and optimizing, a chain which only contains Accept or Drop
actions is left. In the subsequent sections, we require this as a precondition. As an example,
recall the firewall in Fig. 1.Its INPUT chain after unfolding and optimizing is listed in
Fig. 4. Observe that some of the computed match expressions are beyond the expressiveness
of what the iptables command line user interface supports. We will elaborate on this in Sect. 7.
6 Unknown Primitives
As we argued earlier, it is infeasible to support all possible primitives of a firewall. Sup-
pose a new firewall module is created which provides the ssh_blacklisted and
9
Formalization: theorem unfolding_n_sound_complete [19].
10
The relevant check is in mark_source_chains,filesource/net/ipv4/netfilter/ip_table
s.c of the Linux kernel version 4.10.
11
Formalization: theorem iptables_bigstep_rw_Reject [19].
12
Formalization: theorem iptables_bigstep_rm_LogEmpty [19].
13
Formalization: theorem unfold_optimize_ruleset_CHAIN [19].
14
Formalization: theorem unfold_optimize_common_matcher_univ_ruleset_CHAIN [19].
123
C. Diekmann et al.
ssh_innocent primitives. The former applies if an IP address has had too many invalid
SSH login attempts in the past; the latter is the opposite of the former. Since we invented
these primitives, no existing tool will support them. However, a new version of iptables could
implement them or they may be provided as third-party kernel modules. Therefore, our rule-
set transformations must take unknown primitives into account. To achieve this, we lift the
primitive matcher γ to ternary logic, adding Unknown as matching outcome. We embed this
new “approximate” semantics into the semantics described in the previous sections. Thus,
it becomes easier to construct matchers tailored to the primitives supported by a particular
tool.
6.1 Ternary Matching
Logical conjunction and negation on ternary values are as in Boolean logic, with these
additional rules for Unknown operands (commutative cases omitted):
Tr u e Unknown = Unknown False Unknown = False ¬ Unknown = Unknown
These rules correspond to Kleene’s 3-valued logic [42] and are well-suited for firewall
semantics. For firewall rules, the first equation states that, if one condition matches, the final
result only depends on the other condition. The next equation states that a rule cannot match
if one of its conditions does not match. Finally, by negating an unknown value, no additional
information can be inferred. The match expression Any always evaluates to Tr u e and ¬ Any
always evaluates to False for any γ . A match expression may evaluate to Unknown if it
contains unknown primitives x X.
We demonstrate the ¬ Unknown = Unknown case by example: the two rulesets
[
(ssh_blacklisted, Drop)
]
and
(Any, Call c)
where Γ c =[(ssh_innocent,
Return), (Any, Drop)] have exactly the same filtering behavior. After unfolding, the sec-
ond ruleset collapses to
[
(¬ ssh_innocent, Drop)
]
. Both the ssh_blacklisted and
the ssh_innocent primitives are Unknown to our matcher. Thus, since both rulesets have
the same filtering behavior, a packet matching Unknown in the first ruleset should also match
¬ Unknown in the second ruleset.
Stateful Matchers in Ternary Logic.
In Sect. 4.2, we discussed the problem that some match
conditions may maintain an internal state. For a match condition a which updates an internal
state, a ∧¬a = False may not hold. We argued that for some state σ and σ
, stateful
match conditions need to be augmented with their internal state. For example a
σ
∧¬a
σ
”,
which is not a tautology. In our implementation, we immediately embed everything in ternary
logic and treat all primitives which are not definitely stateless as “unknown”. This avoids
the problem with internal state and yields a ∧¬a = Unknown”, which correctly describes
the behavior since we do not know about a potential internal state of some arbitrary match
condition a.
6.2 Closures
In the ternary semantics, it may be unknown whether a rule applies to a packet. Therefore, the
matching semantics are extended with the notion of “in-doubt”-tactics. A tactic is consulted
if the result of a match expression is Unknown. It decides whether a rule should apply or
not.
We introduce the in-doubt-allow and in-doubt-deny tactics. The first tactic forces a match
if the rule’s action is Accept and a mismatch if it is Drop. The second tactic behaves in
123
Verified iptables Firewall Analysis and Verification
the opposite manner. Note that an unfolded ruleset is necessary, since no behavior can be
specified for Call and Return actions.
15
We denote the exact Boolean semantics with and embedded ternary semantics with
an arbitrary tactic α with
α
”. In particular, α = allow for in-doubt-allow and α =deny
analogously.
”and“
α
are related to the tactics as follows: considering the set of all accepted
packets, in-doubt-allow is an overapproximation, whereas in-doubt-deny is an underapprox-
imation. In other words, if accepts a packet, then
allow
also accepts the packet.
Thus, from the opposite perspective, the in-doubt-allow tactic can be used to guarantee that
a packet is certainly dropped. Likewise, if denies a packet, then
deny
also denies
this packet. Thus, the in-doubt-deny tactic can be used to guarantee that a packet is certainly
accepted.
For example, the unfolded firewall of Fig. 1 contains rules which drop a packet if a limit
is exceeded. If this rate limiting is not understood by γ ,thein-doubt-allow tactic will never
apply this rule, while with the in-doubt-deny tactic, it is applied universally.
We say that the Boolean and the ternary matchers agree if they return the same result or
the ternary matcher returns Unknown. Interpreting this definition, the ternary matcher may
always return Unknown and the Boolean matcher serves as an oracle knowing the correct
result. Note that we never explicitly specify anything about the Boolean matcher; therefore
the model is universally valid, i.e., the proof holds for an arbitrary oracle.
If the exact and ternary matcher agree, then the set of all packets allowed by the in-doubt-
deny tactic is a subset of the packets allowed by the exact semantics, which in turn is a subset
of the packets allowed by the in-doubt-allow tactic.
16
Therefore, we call all packets accepted
by
deny
the lower closure, i.e., the semantics which accepts at most the packets that the
exact semantics accepts. Likewise, we call all packets accepted by
allow
the upper closure,
i.e., the semantics which accepts at least the packets that the exact semantics accepts. Every
packet which is not in the upper closure is guaranteed to be dropped by the firewall.
Theorem 5 (Lower and upper closure of allowed packets)
p,γ,p
rs,
?
deny
p,γ,p
rs,
?
p,γ,p
rs,
?
allow
The opposite holds for the set of denied packets.
17
For the example in Fig. 1 , we computed the closures (without the RELATED,ESTABLISH
ED rule, see Sect. 6.4) and a ternary matcher which only understands IP addresses and layer
4 protocols. The lower closure is the empty set since rate limiting could apply to any packet.
The upper closure is the set of packets originating from 192.168.0.0/16.
15
The final decision for Call (resp. Return) rules depends on the called (resp. calling) chain.
16
Formalization: theorem FinalAllowClosure [19].
17
Formalization: theorem FinalDenyClosure [19].
123
C. Diekmann et al.
6.3 Removing Unknown Matches
In this section, as a final optimization, we remove all unknown primitives. We call this
algorithm pu (“process unknowns”). For this step, the specific ternary matcher and the choice
of tactic must be known.
In every rule, top-level unknown primitives can be rewritten to Any or ¬ Any. For example,
let m
u
be a primitive which is unknown to γ . Then, for in-doubt-allow, (m
u
, Accept) is
equal to (Any, Accept) and (m
u
, Drop) is equal to (¬ Any, Drop). Similarly, negated
unknown primitives and conjunctions of (negated) unknown primitives can be rewritten.
Hence, the base cases of pu are straightforward. However, the case of a negated conjunction
of match expressions requires some care. The following equation represents the De Morgan
rule, specialized to the in-doubt-allow tactic.
pu (¬ (m
1
m
2
), a) =
Any if pu (¬ m
1
, a) = Any
Any if pu (¬ m
2
, a) = Any
pu (¬ m
2
, a) if pu (¬ m
1
, a) Any
pu (¬ m
1
, a) if pu (¬ m
2
, a) Any
¬
(
¬ pu
(
¬ m
1
, a
)
∧¬pu
(
¬ m
2
, a
))
otherwise
The algorithm explicitly works on Any instead of Tr u e ’, since in this context, Any
is the syntactic base case of a match expression M
X
and not a Boolean or ternary value.
The ¬ Unknown = Unknown equation is responsible for the complicated nature of the
De Morgan rule. Fortunately, we machine-verified all our algorithms.
18
Anecdotally, we
initially wrote a seemingly simple (but incorrect) version of pu and everybody agreed that
the algorithm looks correct. In the early empirical evaluation, with yet unfinished proofs, we
did not observe our bug. Only because of the failed correctness proof did we realize that we
introduced an equation that only holds in Boolean logic.
Theorem 6 (pu sound and complete)
Γ,γ, p
[pu r. r rs], t
allow
t
iff Γ,γ, p
rs, t
allow
t
Theorem 7 Algorithm pu removes all unknown primitive match expressions.
An algorithm for the in-doubt-deny tactic (with the same equation for the De Morgan
case) can be specified in a similar way. Thus,
α
can be treated as if it were defined only on
Boolean logic with only known match expressions.
As an example, we examine the ruleset of the upper closure of Fig. 1 (without the
RELATED, ESTABLISHED rule, see Sect. 6.4) for a ternary matcher which only under-
stands IP addresses and layer 4 protocols. The ruleset is simplified to
[(src 192.168.0.0/16, Accept), (Any, Drop)]. ITVal can now directly compute
the correct results on this ruleset.
6.4 The RELATED, ESTABLISHED Rule
Since firewalls process rules sequentially, the first rule has no dependency on any previous
rules. Similarly, rules at the beginning have few dependencies on other rules. Therefore,
18
Formalization: theorems transform_remove_unknowns_upper, transform_remove_unkno
wns_lower [19].
123
Verified iptables Firewall Analysis and Verification
firewall rules in the beginning can be inspected manually, whereas the complexity of manual
inspection increases with every additional preceding rule.
It is good practice to start a firewall with an ESTABLISHED (and sometimes RELATED)
rule [29]. This also happens in Fig. 1 after the rate limiting. The ESTABLISHED rule usually
matches most of the packets [29],
19
which is important for performance; however, when
analyzing the filtering behavior of a firewall, it is important to consider how a connection
can be brought to this state. Therefore, we remove this rule and only focus on the connection
setup.
The ESTABLISHED rule essentially allows packet flows in the opposite direction of all
subsequent rules [20]. Unless there are special security requirements (which is not the case
in any of our analyzed scenarios), the ESTABLISHED rule can be excluded when analyzing
the connection setup [20, Corollary 1].
20
If the ESTABLISHED rule is removed and in the
subsequent rules, for example, a primitive state NEW occurs, our ternary matcher returns
Unknown. The closure procedures handle these cases automatically, without the need for
any additional knowledge.
Our generic ruleset rewriting algorithms are not aware of connection state. Therefore,
for our intermediate evaluation (Sect. 8), we removed ESTABLISHED rules by hand. In
Sect. 11.2, we will describe our improvements which will enable support for conntrack state.
There will no longer be any need to manually exclude rules. In short, we will fully support
matches on conntrack state such as ESTABLISHED or NEW. The observation and argument
of this section remains: for access control analysis, we focus on NEW packets.
7 Normalization
Ruleset unfolding may result in non-atomic match expressions like ¬ (a b). The iptables
user interface only supports match expressions in Negation Normal Form (NNF).
21
There, a
negation may only occur before a primitive, not before compound expressions. For example,
¬ ( src ip) tcp is a valid NNF formula, whereas ¬
((
src ip
)
tcp
)
is not. The
reason is that iptables rules are usually specified on the command line and each primitive is an
argument to the iptables command, for example ! –src ip -p tcp .Wenormalize
match expressions to NNF, using the following observations:
De Morgan’s rule can be applied to match expressions, splitting one rule into
two. For example,
(
¬ ( src ip tcp ), Accept
)
and [(¬ src ip, Accept),
(¬ tcp , Accept)] are equivalent. This introduces a “meta-logical” disjunction consist-
ing of a sequence of consecutive rules with a shared action. For example, [(m
1
, a), (m
2
, a)]
is equivalent to [(m
1
m
2
, a)].
For sequences of rules with the same action, a distributive law akin to common Boolean
logic holds. For example, the conjunction of the two rulesets
[(m
1
, a), (m
2
, a)] and [(m
3
, a), (m
4
, a)]
19
We revalidated this observation in September 2014 and found that in our firewall, which has seen more
than 15 billion packets (>19TB data) since the last reboot, more than 95% of all packets matched the first
RELATED,ESTABLISHED rule.
20
The same can be concluded for reflexive ACLs in Cisco’s IOS Firewall [14].
21
Since match expressions do not contain disjunctions, any match expression in NNF is trivially also in
Disjunctive Normal Form (DNF).
123
C. Diekmann et al.
is equivalent to the ruleset
[(m
1
m
3
, a), (m
1
m
4
, a), (m
2
m
3
, a), (m
2
m
4
, a)].
This can be illustrated with a situation where a = Accept and a packet needs to pass two
firewalls in a row.
We can now construct a procedure which converts a rule with a complex match expression
to a sequence of rules with match expressions in NNF. It is independent of the particular
primitive matcher and the in-doubt tactic used. The algorithm n (“normalize”) of type M
X
M
X
list is defined as follows:
nAny =[Any]
n (m
1
m
2
) =[x y. x n m
1
, y n m
2
]
n (¬ (m
1
m
2
)) = n (¬m
1
) ::: n (¬m
2
)
n (¬¬m) = n m
n (¬ Any) =[]
n x =[x ]
for x X
n (¬x ) =[¬x]
The second equation corresponds to the distributive law, the third to the De Morgan rule.
For example, n
(
¬ ( src ip tcp )
)
=
¬ src ip, ¬ tcp
. The fifth rule states
that non-matching rules can be removed completely.
The unfolded ruleset of Fig. 4, which consists of nine rules, can be normalized to a
ruleset of 20 rules (due to distributivity). In the worst case, normalization can cause an
exponential blowup. Our evaluation shows that this is not a problem in practice, even for
large rulesets. This is because rulesets are usually managed manually, which naturally limits
their complexity to a level processible by state-of-the-art hardware.
Theorem 8 n always terminates, all match expressions in the returned list are in NNF, and
their conjunction is equivalent to the original expression.
22
We show soundness and completeness wrt arbitrary γ , α, and primitives.
23
Hence, it also
holds for the Boolean semantics. In general, proofs about the ternary semantics are stronger,
because the ternary primitive matcher can simulate the Boolean matcher.
24
Theorem 9 (n sound and complete)
Γ,γ, p
[(m
, a). m
n m], t
α
t
iff Γ,γ, p
[(m, a)], t
α
t
After having been normalized by n, the rules can mostly be fed back to iptables. For some
specific primitives, iptables imposes additional restrictions, e.g., that at most one primitive of
a type may be present in a single rule. For our intermediate evaluation, we only need to solve
this issue for IP address ranges in CIDR notation [31]. We introduced and verified another
transformation which computes intersection of IP address ranges, which returns at most one
range. This is sufficient to process all rulesets we encountered during our intermediate eval-
uation. In the following sections, we show how to support more primitives; the intermediate
evaluation only focuses on IP addresses; the final evaluation (Sect. 14) incorporates many
more primitives.
22
Formalization: theorem normalized_nnf_match_normalize_match [19].
23
Formalization: theorem normalize_match_correct [19].
24
Formalization: theorems β
magic
_approximating_bigstep_fun_iff_iptables_bigstep,
LukassLemma [19].
123
Verified iptables Firewall Analysis and Verification
8 Intermediate Evaluation
In this section, we demonstrate the applicability of our ruleset preprocessing described thus
far. Usually, network administrators are not inclined towards publishing their firewall ruleset
because of potential negative security implications. For this intermediate evaluation, we have
obtained approximately 20k real-world rules and the permission to publish them (Sect. 17).
An even larger evaluation follows in Sect. 14. In addition to the running example in Fig. 1
(a small real-world firewall), we tested our algorithms on four other real-world firewalls. We
put focus on the third ruleset, because it is one of the largest and the most interesting one.
For our analysis, we wanted to know how the firewall partitions the IPv4 space. Therefore,
we used a matcher γ which only understands source/destination IP addresses and the layer 4
protocols TCP and UDP. Our algorithms do not require special processing capabilities, they
can be executed within seconds on a common off-the-shelf laptop with 4GB of memory.
Ruleset 1 is taken from a Shorewall [28] firewall, running on a home router, with around
500 rules. We verified that our algorithms correctly unfolds, preprocesses, and simplifies
this ruleset. We expected to see, in both the upper and lower closure, that the firewall d rops
packets from private IP ranges. However, we could not see this in the upper closure and
verified that the firewall does indeed not block such packets if their connection is in a certain
state. The administrator of the firewall confirmed this issue and, upon further investigation,
rewrote the whole firewall.
Ruleset 2 is taken from a small firewall script found online [38]. Although it only contains
about 50 rules, we found that it contains a serious mistake. We assume the author accidentally
confused iptables’ -I (insert at top) and -A (append at tail) options. We saw this after unfold-
ing, as the firewall allows nearly all packets at the beginning. Subsequent rules are shadowed
and cannot apply. However, these rules come with a documentation of their intended pur-
pose, such as “drop reserved addresses”, which highlights the error. We verified the erroneous
behavior by installing the firewall on our systems. Thus, our unfolding algorithm alone can
provide valuable insights.
Ruleset 3 and 4 are taken from the main firewall of our lab (Chair of Network Architectures
and Services). One snapshot was taken 2013 with 2800 rules and one snapshot was taken
2014, containing around 4000 rules. It is obvious that these rulesets have grown historically.
About 10 years ago, these two rulesets would h ave been the largest real-world rulesets ever
analyzed in academia [82].
We present the analysis results of the 2013 version of the firewall. Details can be found in
the additional material, the beginning of the ruleset is shown in Fig. 5.Weremovedthefirst
three rules. The first rule was the ESTABLISHED rule, as discussed in Sect. 6.4.Ourfocus
was put on the second rule when we calculated the lower closure: this rule was responsible
for the lower closure being the empty set. Upon closer inspection of this rule, we realized that
it was ‘dead’, i.e., it can never apply. We confirmed this observation by changing the target
to a Log action on the real firewall and could never see a hit of this rule for months. Due
to our analysis, this rule could be removed. The third rule performed SSH rate limiting (a
Drop rule). We removed this rule because we had a very good understanding of it. Keeping
it would not influence correctness of the upper closure, but lead to a smaller lower closure
than necessary.
123
C. Diekmann et al.
-A FORWARD -m state --state RELATED,ESTABLISHED,UNTRACKED -j ACCEPT
-A FORWARD -m recent --update --seconds 60 --name DEFAULT --rsource -j LOG_RECENT_DROP
-A FORWARD -p tcp -m state --state NEW -m tcp --dport 22 --tcp-flags FIN,SYN,RST,ACK SYN
-m recent --update --seconds 360 --hitcount 41 --name ratessh --rsource
-j LOG_RECENT_DROP
-A FORWARD -s 127.0.0.0/8 -j LOG_DROP
-A FORWARD -s 131.159.14.206/32 -i vlan1011 -p tcp -m multiport --sports 389,636 -j ACCEPT
-A FORWARD -s 131.159.14.208/32 -i vlan1011 -p tcp -m multiport --sports 389,636 -j ACCEPT
...
-A LOG_DROP -m limit --limit 100/min -j LOG --log-prefix "[IPT_DROP]:"
-A LOG_DROP -j DROP
-A LOG_RECENT_DROP -m limit --limit 100/min -j LOG --log-prefix "[IPT_RECENT_DROP]:"
-A LOG_RECENT_DROP -j DROP
Fig. 5 Excerpt (first rules) of the 2013 iptables ruleset of our lab
First, we tested the ruleset with the well-maintained Firewall Builder [59]. The original
ruleset could not be imported by Firewall Builder due to 22 errors, caused by unknown match
expressions. Using the calculated upper closure, Firewall Builder could import this ruleset
without any problems.
Next, we tested ITVal’s IP space partitioning query [49]. On our original ruleset with
2800 rules, ITVal completed the query with around 3GB of RAM in around 1min. Analyzing
ITVal’s debug output, we found that most of the rules were not understood correctly due to
unknown primitives. Thus, the results were not reliable. We could verify this as 127.0.0.0/8,
obviously dropped by our firewall, was grouped into the same class as the rest of the Internet.
In contrast, using the upper and lower closure ruleset, ITVal correctly identifies 127.0.0.0/8
as its own class.
We found another interesting result about ITVal: the (optimized) upper closure ruleset only
contains around 1000 rules and the lower closure only around 500 rules. Thus, we expected
that ITVal could process these rulesets significantly faster. However, the opposite is the case:
ITVal requires more than 10 times the resources (both CPU and RAM; we had to move the
analysis to a big machine with > 40GB of memory) to finish the analysis of the closures.
We assume that this is due to the fact that ITVal now understands all rules. Yet, Sect. 14 will
reveal that ITVal still computes wrong results.
Limitations of the Translation. We inspected the simplified rulesets and observed a few
limitations of the translation. Those limitations mainly occur because our algorithms work
on arbitrary γ . While this an important feature, it also means that we did not consider the
peculiarities of specific primitives so far.
We said that iptables only accepts match expressions in NNF, but this condition alone is
insufficient. In addition to NNF, each primitive must occur at most once in a match expression.
For example, iptables does not allow to have two -s primitives which match on source
IP addresses in an expression. However, such expressions may occur after unfolding and
NNF normalization. For this intermediate evaluation, we solved this problem since we can
compress the conjunction of an arbitrary number of matches on IP addresses to a single match
on IP addresses: the intersection of IP address ranges in CIDR notation is either the smallest
of all ranges, or the empty set (details follow in Sect. 11.1). Similarly, the conjunction of all
the same matches on protocols is either the protocol itself, otherwise the match expression
cannot apply to any packet and the complete rule can be removed. For example, a rule which
matches on both tcp and icmp can be removed as a packet cannot be both. In addition, we
see rules with ‘unknown’-parts (before the removal of unknown primitives) which can never
match and should be removed. For example, it is impossible for a packet the have only the SYN
and only the ACK flags set at the same time. However, without providing knowledge about
tcp flags, our generic treatment of unknown match conditions may assume that this match
123
Verified iptables Firewall Analysis and Verification
condition may apply and such rules remain after the simplification. Hence, our simplification
is still too coarse g rained and loses too much information. In addition, as we indicated in
Sect. 3.2, primitives may also be related and can be transformed into simpler primitives. We
elaborate on the treatment of primitives in the following sections.
9 Simple Firewall Model
Now, we present a very simple firewall model. This model was designed to feature nice
mathematical properties, but it is too simplistic to mirror the real world. Afterwards, we
will compare it to our model for real-world firewalls of Sect. 4. Section 10 will show how
rulesets can be translated between these two models. This preprocessing step converts firewall
rulesets from the real-world model to the simple model, which greatly simplifies all future
static firewall analysis.
We will write simple firewall rules as tuple (m, a),wherem is a match expression and a
is the action the firewall performs if m matches for a packet. The firewall has two possibilities
for the filtering decision: it may accept (
) the packet or deny (
) the packet. We will also
use the intermediate state (
?
) in which the firewall did not come to a filtering decision yet.
Note that iptables firewalls always have a default policy and the
?
case cannot occur as final
decision for the simple firewalls we will construct.
The semantics of the simple model is given by a recursive function. The first parameter is
the ruleset the firewall iterates over, the second parameter is the packet.
simple-fw [] p =
?
simple-fw ((m, Accept) :: rs) p = if smatch mpthen
else simple-fw rs p
simple-fw ((m, Drop) :: rs) p = if smatch mpthen
else simple-fw rs p
A function smatch tests whether a packet p matches the match condition m.
25
The match
condition is an 7-tuple, consisting of the following primitives:
(
in, out, src, dst, protocol, src ports, dst ports
)
In contrast to iptables, negating matches is not supported. In detail, the following primitives
are supported:
In/out interface, including support for the + wildcard
Source/destination IP address range in CIDR notation, e.g., 192.168.0.0/24
–Protocol(any, tcp, udp, icmp, or any numeric protocol identifier)
Source/destination interval of ports, e. g., 0:65535
For example, we obtain an empty match (a match that does not apply to any packet) if and
only if an end port is greater than the start port.
26
The match which matches any packet is
constructed by setting the interfaces to +’, the IP to 0.0.0.0/0, the ports to 0:65535 and the
protocol to any.
27
We require that all match conditions are well-formed, i.e., it is only allowed to match on
ports (other than the universe 0:65535) if the protocol is tcp, udp, or sctp.
25
Note that this is not the same function as in Sect. 4, because this simple smatch function does not require
parameter γ . Roughly speaking, it already has the primitive matcher hard-coded into it.
26
Formalization: theorem empty_match [22].
27
Formalization: theorem simple_match_any [22].
123
C. Diekmann et al.
With this type of match expression, it is possible to implement a function conj which
takes two match expressions m
1
and m
2
and returns exactly one match expression being the
conjunction of both.
28
Theorem 10 (Conjunction of two simple match expressions)
smatch m
1
p smatch m
2
p ←→ smatch (conj m
1
m
2
) p
Computing the conjunction of the individual match expressions for port intervals and single
protocols is straightforward. The conjunction of two intervals in CIDR notation is either
empty or the smaller of both intervals. The conjunction of two interfaces is either empty if
they do not share a common prefix, otherwise it is the longest of both interfaces (non-wildcard
interfaces dominate wildcard interfaces).
The conj of two well-formed matches is again well-formed.
29
The type of match expressions was carefully designed such that the conjunction of two
match expressions is only one match expression. If features were added to the match expres-
sion, for example negated interfaces, this property would no longer be guaranteed. Of the
features most commonly found in our iptables firewall rulesets [3], we only found that it
would further be possible to add TCP flags to the match expression without violating the
aforementioned conjunction property. Considering common features of firewalls in general
[70], it would probably be possible to enhance the ICMP support of our model.
One advantage of simple-fw over the semantics of Fig. 2 is that it is a simple recursive
function. In addition, simple-fw is total, i. e., it is guaranteed to terminate. This is not the
case for the semantics of Fig. 2, as the assumptions of Theorem 3 show. Hence, the simple
firewall makes proofs about the filtering behavior much easier as they can often be done by a
list induction over the ruleset. Another advantage is that the smatch function of simple-fw is
completely defined and it is no longer required to reason about an arbitrary but fixed function
γ .
10 Translation to the Simple Firewall Model
The semantics given in Sect. 4 includes a primitive matcher γ that decides whether a certain
primitive matches a packet. The model and all algorithms on top of it are proven correct for
an arbitrary γ , hence, this model supports all iptables matching features. Obviously, there
is no executable code for an arbitrary γ . However, the algorithms to transform rulesets we
present are executable. To have a clear semantics of the primitives, we have defined a subset
of γ , namely for all primitives supported by the simple firewall and some further primitives,
detailed in Sect. 11. We assume that γ behaves as expected on our subset, but it may show
arbitrary behavior for all other primitives. We say we agree on γ . For example, γ behaves
as expected on IP addresses, but it may show arbitrary behavior for a bfp match.
Using our previously described algorithms, we assume that the ruleset is already unfolded
and the match expressions are normalized. This leaves a ruleset where only the following
actions occur: Accept and Drop.
30
Thus, a large step for translating the real-world model
to the simple firewall model is already accomplished. Translating the match expressions for
the simple firewall remains. Of course, it is not possible to translate all primitives to the very
28
Formalization: theorem simple_match_and_correct [22].
29
Formalization: theorem simple_match_and_valid [22].
30
Formalization: theorems rewrite_Goto_chain_safe, unfold_optimize_common_matcher
_univ_ruleset_CHAIN [19].
123
Verified iptables Firewall Analysis and Verification
limited simple-fw model, so we will make use of the pu algorithm when necessary. For the
sake of example, we will only consider the overapproximation in the following parts of this
article; the underapproximation is analogous and can be found in our formalization.
Since firewalls usually accept all packets which belong to an ESTABLISHED connection,
the interesting access control rules in a ruleset only apply to NEW packets. We only consider
NEW packets, i.e., −−ctstate NEW and −−syn for TCP packets. Our first goal is to
translate a ruleset from the real-world model to the simple model. We have proven that the
set of new packets accepted by the simple firewall is a superset (overapproximation) of the
packets accepted by the real-world model.
31
This is a core contribution and we expand on
the translation in the following section.
Theorem 11 (Translation to simple firewall model)