J Autom Reasoning

https://doi.org/10.1007/s10817-017-9445-1

Veriﬁed iptables Firewall Analysis and Veriﬁcation

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 veriﬁed static analysis of

iptables rulesets using Isabelle/HOL. We build our work around a formal semantics of the

behavior of iptables ﬁrewalls. This semantics is tailored to the speciﬁcs of the ﬁlter table and

supports arbitrary match expressions, even new ones that may be added in the future. Around

that, we organize a set of simpliﬁcation procedures and their correctness proofs: we include

procedures that can unfold calls to user-deﬁned chains, simplify match expressions, and

construct approximations removing unknown or unwanted match expressions. For analysis

purposes, we describe a simpliﬁed model of ﬁrewalls 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 veriﬁed generation

of IP space partitions and minimal service matrices. An evaluation of our work on a large

set of real-world ﬁrewall 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 · Netﬁlter · Iptables · Semantics ·

Formal veriﬁcation

1 Introduction

Firewalls are a fundamental security mechanism for computer networks. Several ﬁrewall

solutions, ranging from open source [66,78,79] to commercial [14,37], exist. Operating and

managing ﬁrewalls is challenging as rulesets are usually written manually. While vulnera-

bilities in ﬁrewall software itself are comparatively rare, it has been known for over a decade

[82] that many ﬁrewalls enforce poorly written rulesets. However, the prevalent methodology

for conﬁguring ﬁrewalls has not changed. Consequently, studies regularly report insufﬁcient

quality of ﬁrewall rulesets [25,36,47,54,74,81,84–86].

The predominant ﬁrewall 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 ﬁrewall 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

ﬁrst rule, all incoming packets are sent directly to the user-deﬁned 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 ﬁrewall 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 ﬁrewall. The interesting aspect is when a ﬁrewall

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

Veriﬁed iptables Firewall Analysis and Veriﬁcation

the subsequent rules are the interesting ones which shape the ﬁrewall’s connectivity policy.

There, some services, identiﬁed by their ports, are blocked (and any packets with those

destination ports will never create an established connection). Finally, the ﬁrewall allows all

packets from the local network 192.168.0.0/16 and discards all other packets.

Several tools [47–49,54,59,69,80,85] have been developed to ease ﬁrewall management

and reveal conﬁguration errors. Many tools are not designed for iptables directly, but are

based on a generic ﬁrewall model. When we tried to analyze real-world iptables ﬁrewalls

with the publicly available static analysis tools, none of them could handle the rulesets. Even

after we simpliﬁed the ﬁrewall rulesets, we found that tools still fail to analyze our rulesets

for the following reasons:

– They do not support the vast amount of ﬁrewall features,

– Their ﬁrewall model is too simplistic,

– They require the administrator to learn a complex query language which might be more

complex than the ﬁrewall language itself,

– The analysis algorithms do not scale to large ﬁrewalls, or

– The output of the (unveriﬁed) veriﬁcation 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-deﬁned chains. However, ITVal’s ﬁrewall 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 ﬁrst two rules (in particular the call in the DOS_PROTECT chain)

lets ITVal compute the expected result.

We identiﬁed two concrete issues which prevent tools from “understanding” real-world

ﬁrewalls. 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 ﬁrewall’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 ﬁrewall rulesets have

evolved over time, this poses a particular challenge. Our methodology to tackle this can also

be applied to ﬁrewalls with simpler semantics, or younger technology with fewer features,

e.g., Cisco IOS Access Lists or ﬁltering OpenFlow ﬂow tables (Sect. 15).

In this article, we ﬁrst build a fundamental prerequisite to enable tool-supported analysis

of real-world ﬁrewalls: we present several steps of semantics-preserving ruleset simpliﬁca-

tion, which lead to a ruleset that is “understandable” to subsequent analysis tools: ﬁrst, we

unfold all calls to and returns from user-deﬁned 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 ﬁrewall’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 ﬁltering (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 ﬁrewall 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-veriﬁed iptables

analysis and veriﬁcation tool on top. In detail, our further contributions are:

5. A simple ﬁrewall model, designed for mathematical beauty and ease of static analysis

(Sect. 9)

6. A method to translate real-world ﬁrewall 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 ﬁrewall 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-veriﬁable proof of correctness with Isabelle/HOL (Sect. 17)

2 Background: Formal Veriﬁcation with Isabelle

We veriﬁed 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 speciﬁcation 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 ﬁles 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

Veriﬁed iptables Firewall Analysis and Veriﬁcation

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 speciﬁc 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 ﬁrst survey the common understanding of ﬁrewalls in the literature and present speciﬁc

static ﬁrewall analysis tools afterwards.

3.1 Firewall Models

Packets are routed through the ﬁrewall and the ﬁrewall needs to decide whether to a llow or

deny a packet. The ﬁrewall’s ruleset determines its ﬁltering behavior. The ﬁrewall 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 ﬁrst matching

rule is applied.

The literature agrees on the deﬁnition of a single ﬁrewall 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 ﬁltering rules. The action is either “allow” or “deny”, which directly

corresponds to the ﬁrewall’s ﬁltering 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-deﬁned chains as an action. This allows “jumping” within the

ruleset without having a ﬁnal ﬁltering 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 ﬁelds: 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 ﬂags (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 ﬁrewall in Fig. 1, it becomes obvious that

none of these tools supports that ﬁrewall directly.

We are not the ﬁrst to propose simplifying ﬁrewall rulesets to enable subsequent analysis.

Brucker et al. [8,10,11] provide algorithms to generate test cases from a ﬁrewall policy. A

ﬁrewall 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 ﬁrewall ruleset is ﬁrst simpliﬁed while preserving the original behavior. The correctness of

1

Firewalls can be stateful or stateless. Most current ﬁrewalls are stateful, which means the ﬁrewall 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 ﬁrewall implementation, matching on conntrack states is exactly like matching

on any other (stateless) condition. However, internally in the ﬁrewall, not only the packet header is consulted

but also the current connection tables. Note that existing ﬁrewall 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 ﬁrewall 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 ﬁrewall 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 ﬁrewall model is a useful building block. In general, using our tool as preprocessor

can make ﬁrewall 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 ﬁrewall, the authors of Margrave [54]

translated it to basic Cisco IOS access lists [14] by hand. With our simpliﬁcation, we can

automatically remove all features not understood by basic Cisco IOS. This enables translation

of any iptables ﬁrewall to basic Cisco access lists which is guaranteed to drop no more packets

than the original iptables ﬁrewall. 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 ﬁrewall 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 ﬁrewall 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 ﬁrewalls from our evaluation.

Most aforementioned tools allow detecting conﬂicts between rules to uncover conﬁgura-

tion mistakes. Since our approach rewrites rules to a simpler form and the provenance and

relation of the simpliﬁed 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

ﬁrewall’s ﬁltering 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 veriﬁed, and its implementation contains several errors. For example, ITVal produces

spurious results if the number of signiﬁcant 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-deﬁned 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 veriﬁcation, 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

Veriﬁed iptables Firewall Analysis and Veriﬁcation

aforementioned errors. Our tool strongly builds on the ideas of ITVal, but with a different

algorithm.

Exodus [57] translates existing device conﬁgurations to a simpler model, similar to our

translation step. It translates router conﬁgurations 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 ﬁrewall model: OpenFlow 1.0 only supports a limited set of features (comparable to

our simple ﬁrewall) 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 simpliﬁed rules to the original ruleset, our

approach cannot point to individual ﬂawed ﬁrewall rules, but only provides a complete

overview. For example, our tool reduces thousands of ﬁrewall rules to the easy-to-understand

graphinFig.8, but the information which initial ﬁrewall rules and match conditions are

responsible for each edge of the graph is lost. Complementary to our veriﬁcation tool, and

well-suited for debugging and uncovering responsible misbehaving rules, is Margrave [54].

Margrave can be used to query ﬁrewalls and to troubleshoot conﬁgurations or to show the

impact of ruleset edits. Margrave can ﬁnd 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 ﬁrst-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 ﬁrewall analysis tools do not support matching on interfaces. But

given that a ﬁrewall implements spooﬁng 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

modiﬁcation (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 deﬁnition.

In one ﬁrewall rule, several primitives can be speciﬁed. 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 deﬁned 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 deﬁned

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 deﬁned in Γ . This assumption is justiﬁed, because the Linux kernel only

accepts well-formed rulesets.

4.1 Inductive Deﬁnition

The semantics of a ﬁrewall wrt a given packet p, a background ruleset Γ ,andaprimitive

matcher γ can be deﬁned as a relation over the currently active chain and the state before

and the state after processing this chain. The semantics is speciﬁed 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 ﬁrewall ﬁltering decisions.

Therefore, only the following three states are necessary: the ﬁrewall 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 ﬁrewall with

no ﬁltering 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 ﬁrewall

generates some informational message, which does not inﬂuence ﬁltering.

NoMatch If the ﬁrewall has not come to a ﬁltering decision yet it can process any

non-matching rule without changing its state.

Decision As soon as the ﬁrewall made a ﬁltering decision, all remaining rules can

be skipped. Given determinism (Theorem 2), this means that once decided,

the ﬁrewall does not change its ﬁltering decision of

or

.

Seq If the ﬁrewall has not come to a ﬁltering 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

Veriﬁed iptables Firewall Analysis and Veriﬁcation

Γ, γ, 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

,

?

⇒ tΓ,γ,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

pΓ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 preﬁx rs

1

of the called chain does not lead to a

ﬁltering decision and directly afterwards, a matching Return rule occurs,

the called chain is processed without result.

Log/Empty Neither rule inﬂuences the ﬁltering 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

ﬂexibility: 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 conﬁdence 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 Γ,γ,p rs ⇒ 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 ﬁnite rulesets (i. e., the image/range of Γ is ﬁnite), we can always ﬁnd 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 ﬁeld” must be introduced in the packet

model. Since packets are immutable, this ﬁeld cannot be set by a rule, but the packet must

be given to the ﬁrewall with the ﬁnal value of the ghost ﬁeld already set. Hence, an analysis

must be carried out with the correct value in the ghost ﬁelds 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

Veriﬁed iptables Firewall Analysis and Veriﬁcation

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 speciﬁc ﬁxed state. To additionally convince the reader of

the soundness of our approach, it would be possible to adapt the parser to give a unique

identiﬁer to every primitive which is not known to be stateless. This identiﬁer 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 ﬁrewall’s ﬁltering behavior is preserved,

formally:

Γ,γ, p

P rs, t

⇒ t

iff Γ,γ, p

rs, t

⇒ t

All our proofs are machine-veriﬁed with Isabelle. Therefore, once the reader is convinced

of the semantics as speciﬁed 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 deﬁned 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 inﬁnite 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

deﬁned in Fig. 2 occur in the ruleset; our parser rejects everything else.

5

Formalization: ﬁle 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 inﬁnite

calling loops), Γ is well-formed (i. e., all chain names that are called are deﬁned), 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: ﬁrst, we can statically verify that Γ is well-formed by verifying that

all chain names which are referenced in an action are deﬁned and that no unsupported actions

occur. Next, our tool veriﬁes that there are no inﬁnite loops by unfolding the ruleset (Sect. 5)

only a ﬁnite but sufﬁciently 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 ﬁrewalls we have analyzed. Those used very special iptables actions

8

not

supported by our semantics or special hand-crafted ﬁrewalls 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

Veriﬁed iptables Firewall Analysis and Veriﬁcation

[(¬ (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 ﬁrewall

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 ﬁltering behavior.

Since we have not formally veriﬁed 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, speciﬁc 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 ﬁrewall 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 ﬁrewall. Sup-

pose a new ﬁrewall 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,ﬁlesource/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 ﬁrewall

semantics. For ﬁrewall rules, the ﬁrst equation states that, if one condition matches, the ﬁnal

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 ﬁltering 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 ﬁltering behavior, a packet matching Unknown in the ﬁrst 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 deﬁnitely 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 ﬁrst tactic forces a match

if the rule’s action is Accept and a mismatch if it is Drop. The second tactic behaves in

123

Veriﬁed iptables Firewall Analysis and Veriﬁcation

the opposite manner. Note that an unfolded ruleset is necessary, since no behavior can be

speciﬁed 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 ﬁrewall 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 deﬁnition, 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 ﬁrewall.

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 ﬁnal 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 ﬁnal optimization, we remove all unknown primitives. We call this

algorithm pu (“process unknowns”). For this step, the speciﬁc 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-veriﬁed 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 unﬁnished 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 speciﬁed in a similar way. Thus, ⇒

α

can be treated as if it were deﬁned 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 simpliﬁed 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 ﬁrewalls process rules sequentially, the ﬁrst 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

Veriﬁed iptables Firewall Analysis and Veriﬁcation

ﬁrewall 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 ﬁrewall 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 ﬁltering behavior of a ﬁrewall, 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 ﬂows 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 speciﬁed 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 ﬁrewall, which has seen more

than 15 billion packets (>19TB data) since the last reboot, more than 95% of all packets matched the ﬁrst

RELATED,ESTABLISHED rule.

20

The same can be concluded for reﬂexive 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

ﬁrewalls 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 deﬁned 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 ﬁfth 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

speciﬁc 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 veriﬁed another

transformation which computes intersection of IP address ranges, which returns at most one

range. This is sufﬁcient 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 ﬁnal 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

Veriﬁed iptables Firewall Analysis and Veriﬁcation

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 ﬁrewall 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 ﬁrewall), we tested our algorithms on four other real-world ﬁrewalls. 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 ﬁrewall 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] ﬁrewall, running on a home router, with around

500 rules. We veriﬁed that our algorithms correctly unfolds, preprocesses, and simpliﬁes

this ruleset. We expected to see, in both the upper and lower closure, that the ﬁrewall d rops

packets from private IP ranges. However, we could not see this in the upper closure and

veriﬁed that the ﬁrewall does indeed not block such packets if their connection is in a certain

state. The administrator of the ﬁrewall conﬁrmed this issue and, upon further investigation,

rewrote the whole ﬁrewall.

Ruleset 2 is taken from a small ﬁrewall 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 ﬁrewall 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 veriﬁed the erroneous

behavior by installing the ﬁrewall on our systems. Thus, our unfolding algorithm alone can

provide valuable insights.

Ruleset 3 and 4 are taken from the main ﬁrewall 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 ﬁrewall. Details can be found in

the additional material, the beginning of the ruleset is shown in Fig. 5.Weremovedtheﬁrst

three rules. The ﬁrst 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 conﬁrmed this observation by changing the target

to a Log action on the real ﬁrewall 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 inﬂuence 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 (ﬁrst 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 ﬁrewall, was grouped into the same class as the rest of the Internet.

In contrast, using the upper and lower closure ruleset, ITVal correctly identiﬁes 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 signiﬁcantly 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 ﬁnish 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 simpliﬁed 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 speciﬁc primitives so far.

We said that iptables only accepts match expressions in NNF, but this condition alone is

insufﬁcient. 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 ﬂags set at the same time. However, without providing knowledge about

tcp ﬂags, our generic treatment of unknown match conditions may assume that this match

123

Veriﬁed iptables Firewall Analysis and Veriﬁcation

condition may apply and such rules remain after the simpliﬁcation. Hence, our simpliﬁcation

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 ﬁrewall 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 ﬁrewalls of Sect. 4. Section 10 will show how

rulesets can be translated between these two models. This preprocessing step converts ﬁrewall

rulesets from the real-world model to the simple model, which greatly simpliﬁes all future

static ﬁrewall analysis.

We will write simple ﬁrewall rules as tuple (m, a),wherem is a match expression and a

is the action the ﬁrewall performs if m matches for a packet. The ﬁrewall has two possibilities

for the ﬁltering decision: it may accept (

) the packet or deny (

) the packet. We will also

use the intermediate state (

?

) in which the ﬁrewall did not come to a ﬁltering decision yet.

Note that iptables ﬁrewalls always have a default policy and the

?

case cannot occur as ﬁnal

decision for the simple ﬁrewalls we will construct.

The semantics of the simple model is given by a recursive function. The ﬁrst parameter is

the ruleset the ﬁrewall 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 identiﬁer)

– 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 preﬁx, 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 ﬁrewall rulesets [3], we only found that it

would further be possible to add TCP ﬂags to the match expression without violating the

aforementioned conjunction property. Considering common features of ﬁrewalls 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

ﬁrewall makes proofs about the ﬁltering 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 deﬁned and it is no longer required to reason about an arbitrary but ﬁxed 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 deﬁned a subset

of γ , namely for all primitives supported by the simple ﬁrewall 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 ﬁrewall model is already accomplished. Translating the match expressions for

the simple ﬁrewall 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

Veriﬁed iptables Firewall Analysis and Veriﬁcation

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 ﬁrewalls 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 ﬁrst 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 ﬁrewall 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 ﬁrewall model)