Verified iptables Firewall Analysis and Verification

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 vulnerabilities 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, 84‐86].

The predominant firewall of Linux is iptables [78]. In general, an iptables ruleset is processed 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 beginning 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, 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 [47‐49, 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: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 implementation 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] in the future since they can be written as simple userspace programs [45]. Therefore, it is virtually 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).

To summarize, we provide the following contributions for simplifying iptables rulesets: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:

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., \(f\ a\) denotes function f applied to parameter a. We write for prepending a single element to a list, e.g., , and for appending lists, e.g., . The empty list is written as []. \([f\ a.\ a \leftarrow l]\) denotes a list comprehension, i.e., applying f to every element a of list l. \([f\ x\ y.\ \ x \leftarrow l_1,\; y \leftarrow l_2]\) denotes the list comprehension where f is applied to each combination of elements of the lists \(l_1\) and \(l_2\). For \(f\ x \ y = (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).

We first survey the common understanding of firewalls in the literature and present specific static firewall analysis tools afterwards.

We formalized the semantics of a subset of iptables. The semantics focuses on access control, which is done in the INPUT, OUTUT, and FORWARD 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 \(\gamma \) decides whether a packet matches a primitive. Formally, based on a set X of primitives and a set of packets P, a primitive matcher \(\gamma \) 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 conjunction, for example \(\texttt {src 192.168.0.0/24}\) and \({\texttt {tcp}}\). Disjunction is omitted because 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\):

The match expression \({\mathsf {Any}}{}\) matches any packet. For a primitive matcher \(\gamma \) and a match expression \(m \in M_X\), we write \({{\mathsf {match}\ {\gamma }}\ m \ p}\) if a packet \(p \in P\) matches m, essentially lifting \(\gamma \) to a relation over \(M_X\) and P, with the connectives defined as usual. With completely generic P, X, and \(\gamma \), 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: \({\mathtt {Accept}}\), \({\mathtt {Reject}}\), \({\mathtt {Drop}}\), \({\mathtt {Log}}\), \({\mathtt {Empty}}\), \({\mathtt {Call}}\ c\) for a chain c , and \({\mathtt {Return}}\). A rule 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 \({\texttt {DOS\_PROTECT}}\) chain in Fig. 1 is \([({\texttt {icmp}} \wedge {\texttt {icmptype 8 limit:}} \,\dots ,\, {\mathtt {Return}}),\, \dots ]\).

A set of named chains is called a ruleset. Let \(\varGamma \) denote the mapping from chain names to chains. For example, \(\varGamma \ {\texttt {DOS\_PROTECT}} \) returns the contents of the \({\texttt {DOS\_PROTECT}}\) chain. We assume that \(\varGamma \) is well-formed, that is, if a \({\mathtt {Call}}\ c\) action occurs in a ruleset, then the chain named c is defined in \(\varGamma \). This assumption is justified, because the Linux kernel only accepts well-formed rulesets.

In this section, we present algorithms to convert a ruleset from the complex chain model to the simple list model.

The function \(\mathsf {pr}\) (“process return”) iterates over a chain. If a \({\mathtt {Return}}\) rule is encountered, all subsequent rules are amended by adding the \({\mathtt {Return}}\) rule’s negated match expression as a conjunct. Intuitively, if a \({\mathtt {Return}}\) rule occurs in a chain, all following rules of this chain can only be reached if the \({\mathtt {Return}}\) rule does not match.

The function \(\mathsf {pc}\) (“process call”) iterates over a chain, unfolding one level of \({\mathtt {Call}}\) rules. If a \({\mathtt {Call}}\) to the chain c occurs, the chain itself (i.e., \(\varGamma \ c\)) is inserted instead of the \({\mathtt {Call}}\). However, \({\mathtt {Return}}\)s in the chain need to be processed and the match expression for the original \({\mathtt {Call}}\) needs to be added to the inserted chain.

The procedure \(\mathsf {pc}\) can be applied arbitrarily many times and preserves the semantics.⁹

In each iteration, the algorithm unfolds one level of \({\mathtt {Call}}\)s. 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,¹⁰ both our algorithm and the resulting ruleset are guaranteed to terminate.

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:Therefore, after unfolding and optimizing, a chain which only contains \({\mathtt {Accept}}\) or \({\mathtt {Drop}}\) actions is left. In the subsequent sections, we require this as a precondition. As an example, recall the firewall in Fig. 1. Its \({\texttt { 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.

As we argued earlier, it is infeasible to support all possible primitives of a firewall. Suppose a new firewall module is created which provides the \({\texttt { ssh\_blacklisted }}\) and 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 ruleset transformations must take unknown primitives into account. To achieve this, we lift the primitive matcher \(\gamma \) to ternary logic, adding \(\mathsf {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.

Ruleset unfolding may result in non-atomic match expressions like \(\lnot \,(a \wedge b)\). The iptables user interface only supports match expressions in Negation Normal Form (NNF).²¹ There, a negation may only occur before a primitive, not before compound expressions. For example, \(\lnot \,({\texttt { src}} \, ip ) \,\wedge \, \mathtt {tcp}\) is a valid NNF formula, whereas \(\lnot \,\left( \left( {\texttt { src }} \, ip \right) \,\wedge \, \mathtt {tcp}\right) \) 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 \(\texttt { ! --src}\, ip {\texttt { -p\, tcp }}\). We normalize 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, \(\left[ \left( \lnot \;({\texttt { src}} \, ip \;\wedge \; {\texttt { tcp }}),\, {\mathtt {Accept}}\right) \right] \) and \([(\lnot \;{\texttt { src}} \, ip ,\; {\mathtt {Accept}}),\, (\lnot \; {\texttt { tcp }},\, {\mathtt {Accept}})]\) are equivalent. This introduces a “meta-logical” disjunction consisting of a sequence of consecutive rules with a shared action. For example, \([(m_1,\, a),\; (m_2,\, a)]\) is equivalent to \([(m_1 \vee 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 rulesetsis equivalent to the rulesetThis can be illustrated with a situation where \(a = {\mathtt {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 \(\mathsf {n}\) (“normalize”) of type \(M_X \Rightarrow M_X\ list \) is defined as follows:

The second equation corresponds to the distributive law, the third to the De Morgan rule. For example, \(\mathsf {n}\ \left( \lnot \,({\texttt { src }}\; ip \wedge {\texttt { tcp }})\right) = \left[ \lnot \,{\texttt { src }}\; ip ,\, \lnot \, {\texttt { tcp }}\right] \). 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.

We show soundness and completeness wrt arbitrary \(\gamma \), \(\alpha \), and primitives.²³ 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.²⁴

After having been normalized by \(\mathsf {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 evaluation. 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.

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 \(20\text {k}\) 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 \(\gamma \) 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 drops 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 unfolding, 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 purpose, 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 have 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. We removed the first three rules. The first rule was the ESTABLISHED rule, as discussed in Sect. 6.4. Our focus 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 \({\mathtt {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 \({\mathtt {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.

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 > 40 GB 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 \(\gamma \). 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 condition may apply and such rules remain after the simplification. Hence, our simplification is still too coarse grained 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.

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)\), where m 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 (\(\textcircled {\checkmark }\)) the packet or deny ( ) the packet. We will also use the intermediate state (\(\textcircled {?}\)) in which the firewall did not come to a filtering decision yet. Note that iptables firewalls always have a default policy and the \(\textcircled {?}\) 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.

A function \(\mathsf {smatch}\) tests whether a packet p matches the match condition m.²⁵ The match condition is an 7-tuple, consisting of the following primitives:

In contrast to iptables, negating matches is not supported. In detail, the following primitives are supported: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.²⁶ 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 \(\mathsf {any}\).²⁷

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.

With this type of match expression, it is possible to implement a function \(\mathsf {conj}\) which takes two match expressions \(m_1\) and \(m_2\) and returns exactly one match expression being the conjunction of both.²⁸

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 \(\mathsf {conj}\) of two well-formed matches is again well-formed.²⁹

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 expression, 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 over the semantics of Fig. 2 is that it is a simple recursive function. In addition, 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 function of is completely defined and it is no longer required to reason about an arbitrary but fixed function \(\gamma \).

The semantics given in Sect. 4 includes a primitive matcher \(\gamma \) that decides whether a certain primitive matches a packet. The model and all algorithms on top of it are proven correct for an arbitrary \(\gamma \), hence, this model supports all iptables matching features. Obviously, there is no executable code for an arbitrary \(\gamma \). However, the algorithms to transform rulesets we present are executable. To have a clear semantics of the primitives, we have defined a subset of \(\gamma \), namely for all primitives supported by the simple firewall and some further primitives, detailed in Sect. 11. We assume that \(\gamma \) behaves as expected on our subset, but it may show arbitrary behavior for all other primitives. We say we agree on \(\gamma \). For example, \(\gamma \) 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: \({\mathtt {Accept}}\) and \({\mathtt {Drop}}\).³⁰ 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 limited model, so we will make use of the \(\mathsf {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., \({{-}{-}{} \texttt {ctstate NEW}}\) and \({{-}{-}{} \texttt {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.³¹ This is a core contribution and we expand on the translation in the following section.

Any packet dropped by the translated, overapproximated simple firewall ruleset is guaranteed to be dropped by the real-world firewall, for arbitrary \(\gamma \), \(\varGamma \), \( rs \). Similar guarantees for definitely accepted packets can be given by considering the translated underapproximation. Given the simplicity of the model, it is much easier to write algorithms to analyze and verify the translated rulesets.

Example. Because this article proceeds to focus more on individual primitives, we will increasingly use the more precise syntax of iptables-save which is also described by the man pages iptables(8) and iptables-extensions(8). We consider a FORWARD chain with a default policy of \(\mathtt {Drop}\) and a user-defined chain foo.

This ruleset, although it only consists of three rules and a default policy, is complicated to analyze. Our translation algorithm translates it to the simple firewall model, where the ruleset becomes remarkably simple. We use \(*\) to denote a wildcard:

No over- or underapproximation occurred since all primitives could be translated. Note the 10.128.0.0/9 address range, which is the result of the intersection of 10.0.0.0/8 and the negation of 10.0.0.0/9.

In this section, we present algorithms to transform specific primitives without changing the behavior of the firewall.³² As a result, the primitive matches on interfaces, IP addresses, protocols, and ports will be normalized such that the translation to the is obvious. Since iptables supports over 200 individual options for match conditions, we cannot cover all. For example, we do not support any IPsec ah or esp matches or bpf matches, but we will simply abstract over them using our algorithm \(\mathsf {pu}\). However, we support the most common features found in common iptables rulesets. Simple matches, such as -s or -d to match on source or destination IP addresses are already supported by the . The iprange or multiport module allow matching on IP addresses and ports, but are more expressible than the supports. We translate them without the loss of information, but at the cost of increased ruleset size. Other modules, such as conntrack state or tcp flags cannot be expressed in the at all. However, we are sometimes able to rewrite them directly to \({\mathsf {Any}}\) or \(\lnot \;{\mathsf {Any}}\). We continue by describing the normalization of all common primitives found in iptables rulesets.

In this section, we will show two algorithms that work on rulesets translated to the model.

We used Isabelle’s code generation features [34, 35] to build a stand-alone tool in Haskell. Since all analysis and transformation algorithms are written in Isabelle, we only needed to add parsers and user interface. Overall, more than 80% of the code is generated by Isabelle, which gives us strong trust in the tool.

We call our tool fffuu, the “fancy formal firewall universal understander”.

fffuu requires only one parameter to run, namely, an iptables-save dump. This makes it very usable. Optionally, one may pass an ipassmt, change the table or chain which is loaded, pass a routing table for output port rewriting, or select the services for the service matrix.

fffuu can be easily compiled from source using stack,⁵⁰ which ensures reproducible builds well into the future.

Example. We demonstrate fffuu by a small example. We want to infer the intention behind the ruleset shown in Fig. 6. Though this ruleset was artificially crafted to demonstrate certain corner cases, it is based on actual rules from real-world firewalls [3, 16]. Also note that the interface name

with UTF-8 symbols and shell escapes for color [53] is perfectly valid.

It is hard to guess what the ruleset is implementing. We load the ruleset into fffuu, not requiring any additional parameters or manual steps to compute it. The resulting service matrix (for arbitrary ports) is shown in Fig. 7 and provides insight into the intention of the ruleset. An arrow from one IP range to another IP range indicates that the first range may set up connections with the second.

At the bottom, we see the localhost range of 127.0.0.0/8. The reflexive arrow (localhost to localhost) shows that the firewall does not block its own localhost traffic, which is usually a good sign. However, localhost traffic is usually not interesting for a firewall analysis since this range is usually not routed [15]. We will ignore it from now.

On the top, in the cloud, we see a large set of IP addresses. This corresponds to the Internet. On the left, we see the 131.159.21.0/24 range. It may access the Internet and the 131.159.15.240/28 range. On the right, we see the 131.159.15.240/28 range, which may only access the Internet, but not the 131.159.21.0/24 range.

Carefully looking at the figure, we might recognize the overall architecture: the firewall implements the “Demilitarized Zone” (DMZ) architectural pattern. This can usually be described as a local network that is segmented into two parts; a public one that is reachable from the outside Internet (hosting services that need to be reachable from the outside, e.g., a mail or a web server) and an internal one that can only connect to the Internet, but not the opposite direction. To mitigate a situation where some host in the public segment gets compromised, the firewall also prohibits connection from the public into the internal segment. Starting from the original iptables-save input, without the help of fffuu, this architecture would have been difficult to uncover and verify.

We obtained real-world rulesets from over 15 firewalls. Some are central, production-critical devices. They are written by different authors, utilize a vast amount of different features and exhibit different styles and patterns. The fact that we publish the complete rulesets is an important contribution (cf. Wool [82, 84]). To the best of our knowledge, this is the largest, publicly available collection of real-world iptables rulesets. Note: some administrators wish to remain anonymous so we replaced their public IP addresses with public IP ranges of our institute, preserving all IP subset relationships.

Table 1 summarizes the evaluation’s results. The first column (“Fw”) labels the analyzed ruleset. Column 2 (“Rules”) contains the number of rules (only the filter table) in the output of iptables-save. We work directly on these real-world data sets. Column 3 describes the analyzed chain. Depending on the type of firewall, we either analyzed the FORWARD (“FW”) or the INPUT (“IN”) chain. For a host firewall, we analyzed IN; for a network firewall, e.g., on a gateway or router, we analyzed FW. In parentheses, we wrote the number of rules after unfolding the analyzed chain. The unfolding also features some generic, straight-forward optimizations, such as removing rules where the match expression is \(\lnot \,{\mathsf {Any}}{}\). Column 4 (“Simple rules”) is the number of rules when translated to the simple firewall. In parentheses, we wrote the number of simple firewall rules when interfaces are removed. This ruleset is used subsequently to compute the partitions and service matrices. In column 5 (“Use”), we mark whether the translated simple firewall is useful. We will detail on the metric later. Column 6 (“Parts”) lists the number of IP address space partitions. For comparison, we give the number of partitions computed by ITVal in parentheses. In Columns 7 and 8, we give the number of partitions for the service matrices for SSH and HTTP. In column 9 (“Time (ITVal)”), for comparison, we put the runtime of the partitioning by ITVal in parentheses in seconds, minutes, or hours. In column 10 (“Time (this)”), we give the overall runtime of our analysis.

When translating to the simple firewall, to accomplish support for arbitrary matching primitives, some approximations need to be performed. For every firewall, the first row states the overapproximation (more permissive), the second row the underapproximation (more strict).

In contrast to the intermediate evaluation, there is no longer the need to manually exclude certain rules from the analysis (cf. Sect. 6.4). For some rulesets, we do not know the interface configuration. For others, there were zone-spanning interfaces. For these reasons, as proven in Sect. 11.6, in the majority of cases, we could not rewrite interfaces. This is one reason for the differences between over- and underapproximation.

We loaded all translated simple firewall rulesets (without interfaces) with iptables-restore. This validates that our results are well-formed. We then used iptables directly to generate the firewall format required by ITVal (iptables -L -n). Our translation to the simple firewall is required because ITVal cannot understand the original complex rulesets and produces flawed results for them.

Performance. We have two possibilities to execute our algorithms, depending on whether the user wants to run them inside of Isabelle or as an external stand-alone application [34].

For our evaluation, we utilize Isabelle’s code reflection capabilities. In essence, it gives us a way to execute our algorithms as if they were implemented in Isabelle’s implementation language (Standard ML). Isabelle’s code generator introduces its own unoptimized version for data structures that are already present in the standard libraries of many programming languages. Hence, the generated code may be quite inefficient.⁵¹ For example, lookups in Isabelle-generated dictionaries have linear lookup time, compared to constant lookup time of standard library implementations. In contrast, ITVal is highly optimized C++ code. We benchmarked our tool on a commodity i7-2620M laptop with 2 physical cores and 8 GB of RAM. In contrast, we executed ITVal on a server with 16 physical Xeon E5-2650 cores and 128 GB RAM. The runtime measured for our tool is the complete translation to the two simple firewalls, computation of partitions, and the two service matrices. In contrast, the runtime of ITVal only consists of computing one partition. The reported time of our tool also includes the runtime of Isabelle’s code generator, but for ITVal we did not add its compilation time. This is one reason why ITVal outperforms our tool for runtimes of < 1 min.

Table 1 shows that our tool outperforms ITVal for large firewalls. We added ITVal’s memory requirements to the table if they exceeded 20 GB. ITVal requires an infeasible amount of memory for larger rulesets while our tool can finish on commodity hardware. The overall numbers show that the runtime for our tool is sufficient for static, offline analysis, even for large real-word rulesets.

For our daily use and convenience, we use our Haskell tool fffuu which adds another order of magnitude of speedup to our numbers of Table 1.

Quality of results. The main goal of ITVal is to compute a minimal partitioning while ours may not be minimal. A smaller number of partitions is better, since the result is more overseeable. It can be seen that ITVal provides better results than our approach in Column 6. Since a service matrix is more specific than a partitioning, the partitions of a service matrix (Column 7 and 8) can be even smaller. Our service matrices are provably minimal and thus improve on ITVal’s partitioning. Since a partitioning cannot be smaller than a service matrix, the numbers in Column 6 must be greater or equal than the numbers in Column 7 or 8. For firewalls A and R, it can be seen that ITVals’s results are spurious, while ours are provably correct. In general, if the number of partitions calculated by ITVal is smaller than those of a service matrix, this is an error in ITVal.

In Column 5, we show the usefulness of the translated simple firewall (including interfaces). We deem a firewall useful if interesting information was preserved by the approximation. Therefore, we manually inspected the rulesest and compared it to the original. For the overapproximation, we focused on preserved (non-shadowed) \({\mathtt {Drop}}\) rules. For the underapproximation, we focused on preserved (non-shadowed) \({\mathtt {Accept}}\) rules. If the firewall features some rate-limiting for all packets in the beginning, the underapproximation is naturally a drop-all ruleset because the rate-limiting could apply to all packets. According to our metric, such a ruleset is of no use (but the only sound solution). We indicate this case with a superscript ^r. The table indicates that, usually, at least one approximation per firewall is useful.

For brevity, we only elaborate on the most interesting rulesets and consequences of their analysis.

The firewall starts with some rate-limiting rules. Therefore, its stricter approximation assumes that the rate-limiting always applies and transforms the ruleset into a deny-all ruleset. The more permissive approximation abstracts over this rate-limiting and provides a very good approximation of the original ruleset.

The SSH service matrix is visualized in Fig. 8 and in Fig. 9 with the raw IP addresses. The figure can be read as follows: the vast majority of our IP addresses are grouped into internal and servers. Servers are reachable from the outside, internal hosts are not. \( ip _1\) and \( ip _2\) are two individual IP addresses with special exceptions. There is also a group for the backbone routers of the connected AS. INET is the set of IP addresses which does not belong to us, basically the Internet. INET’ is another part of the Internet. With the help of the service matrix, the administrator confirmed that the existence of INET’ was an error caused by a stale rule. The misconfiguration has been fixed. Figure 8 summarizes over 4000 firewall rules and helps to easily visually verify the complex SSH setup of our firewall. The administrator was also interested in the Kerberos (kerberos-adm) and LDAP service matrices. They helped verifying the complex setup and discovered potential for ruleset cleanup.

We have used the fffuu tool further on to analyze our firewall. For example, Figs. 10 (IPv4) and 11 (IPv6) were created from a recent snapshot of June 2016 and depict the service matrix for HTTP. This snapshot is not listed in the table. The figures show the raw IP addresses. It can be seen that the “two INETs” bug has been fixed, but the overall complexity of the firewall increased. Note that the service matrix is minimal, i.e., there is no way to compress it any further. The two figures reveal the intrinsic complexity of this firewall. However, the figures, though complicated, can still be visualized on one page. This would be impossible for the thousands of rules of the actual ruleset. It demonstrates that our service matrices can give a suitable overview of complicated rulesets.

Roughly speaking, the firewall connects interfaces to each other, i.e., it heavily uses -i and -o. This can be easily seen in the overapproximation. There are also many zone-spanning interfaces. As we have proven, it is impossible to rewrite interfaces in this case. In addition, for some interfaces, no IP ranges are specified. Hence, this ruleset is more of a link layer firewall than a network layer firewall. Consequently, the service matrices are barely of any use.

Later on, having obtained more detailed interface and routing configurations, we tried again with input and output port rewriting. The result is not shown in the table, but visualized in Fig. 12. The figure now correctly summarizes the network architecture enforced by the firewall. It shows the general Internet, a Debian update server (141.76.2.4), and four internal networks with different access rights.

Firewall E. This ruleset was taken from a NAS device from the introduction (Fig. 1). The ruleset first performs some rate-limiting. Consequently, the underapproximation corresponds to the deny-all ruleset. The table lists a more recent version of the ruleset after a system update. Our SSH service matrix reveals a misconfiguration: SSH was accidentally left enabled after the update. After this discovery, the flaw was fixed. The service matrix for the other services provided by the NAS (not listed in the table) verifies that these services are only accessible from the local network. This finally yields the expected result as motivated in the introduction.

Firewall H. This ruleset from 2003 appears to block Kazaa filesharing traffic during working hours. In addition, a rule drops all packets with the string “X-Kazaa-User”. The more permissive abstraction correctly tells that the firewall may accept all packets for all IPs (if the above conditions do not hold). Hence, the firewall is essentially abstracted to an allow-all ruleset. According to our metric, this information is not useful. However, in this scenario, this information may reveal an error in the ruleset: the firewall explicitly permits certain IP ranges, but the default policy is \({\mathtt {Accept}}\) and includes all these previously explicitly permitted ranges. By inspecting the structure of the firewall, we suspect that the default policy should be \({\mathtt {Drop}}\). This possible misconfiguration was uncovered by the overapproximation.

The underapproximation does not understand the string match on “X-Kazaa-User” in the beginning and thus corresponds to the deny-all ruleset. However, a manual inspection of the underapproximation still reveals an interesting error: the ruleset also tries to prevent MAC address spoofing for some hard-coded MAC/IP pairs. However, we could not see any drop rules for spoofed MAC addresses in the underapproximation. Indeed, the ruleset allows non-spoofed packets but forgets to drop the spoofed ones. This firewall demonstrates the worst case for our approximations: one set of accepted packets is the universe, the other is the empty set. But because this ruleset is severely broken, no better approximation would be possible. Nevertheless, the manual inspection of the simplified ruleset helped reveal several errors. This demonstrates that even if the service matrices do not contain any information, the other output of our tool may still contain interesting information.

We calculated the simplified firewall rules and service matrices. Using the underapproximation, we could also give guarantees about the packets which are definitely allowed by the firewall. The administrator critically inspected the output of our tool. Finally, they confirmed that the firewall was working exactly as intended. This demonstrates: not only finding errors but showing correctness is one of the key strengths of our tool.

After the analysis, the administrator revealed their true intentions. They have previously upgraded the system to iptables. Their users (the company’s employees) became aware of that. They received some complaints about connectivity issues and the employees were blaming the firewall. However, the administrator was suspecting that the connectivity issues were triggered by some users who are behaving against the corporate policy, e.g., sharing user accounts. With the help of our analysis, the administrator could reject all accusations about their firewall configuration and follow their initial suspicion about misbehaving employees.

A few months later, we received feedback that the firewall was perfect and “users are stupid”.

Firewall R. This ruleset was extracted from a Docker host and partly generated by topoS [21]. For remote management, the ruleset allows unconstrained SSH access for all machines, which can be seen by the fact that the SSH service matrix only shows one partition. In contrast, an advanced setup is enforced for HTTP and the HTTP matrix is visualized in Fig. 13. Being able to verify the publicly exposed HTTP setup while neglecting the SSH maintenance setup demonstrates the advantage of calculating our access matrices for each service. We extended fffuu to also show flows which can be in an ESTABLISHED state. This is visualized by an orange dashed line. Due to special, scenario-specific requirements, we can see that 10.0.0.2 is a true information sink and may not even answer to ESTABLISHED connections. The lower closure also exhibits one interesting detail: except for one host which is rate limited, SSH connectivity is guaranteed. Ironically, ITVal segfaults on the original ruleset. With our processing, it terminates successfully but returns a spurious result.

OpenFlow [64, 67] is a standard for configuring OpenFlow-enabled switches. It is usually referred to in the context of Software-Defined Networking (SDN) and has been hot topic in network management and operations for almost 10 years.

This article focused on the analysis of iptables instead of OpenFlow for several reasons: despite OpenFlow 1.0 [67] having been available for over 5 years, it is a relatively young and not very wide-spread product. In contrast, iptables is battle-tested, real-world approved, supports a large amount of features, and has been in productive use for over a decade. There are also decade-old configurations which utilize a vast amount of features, which are no longer fully understood by administrators [3]. As of July 2016, the popular systems and networking Q&A site Server Fault⁵² counts more than a hundred times more questions related to iptables than OpenFlow. The related Super User⁵³ site counts even a thousand times more questions related to iptables than OpenFlow.

Over the years, iptables has evolved into a system with an enormous amount of (legacy) features. Compared to this, OpenFlow is a tidy piece of technology. But we anticipate to see similar feature creep over the years, considering, e.g., Nicira extensions [61] or attempts to enhance OpenFlow with generic FPGAs to add “exotic functionality” [12]. In a broader context, by extending OpenFlow or one of its proposed stateful, more feature-rich, successors [7], many iptables features have already been reimplemented on top of it [65].

Our declared goal was to provide scientific methods to understand challenging configurations (as observed in iptables) and evaluate our methodology on complex, real-world, legacy-grown systems. The insights we obtained can also be applied to OpenFlow. In particular, a large portion of this article focuses on match conditions, e.g., abstracting over unknowns, optimizing, rewriting, normalizing, or even replacing interfaces by IP addresses. Our work on match conditions can be directly reused in future work within the context of OpenFlow.

However, iptables is not OpenFlow. In particular, the OpenFlow standard defines a vast amount of actions which can be performed for a packet. In contrast, iptables filtering primarily uses the two actions \(\mathtt {Accept}\) and \(\mathtt {Drop}\). This is because a firewall cleanly separates filtering from other network functions, such as packet rewriting. OpenFlow implementations tend to mix those. We have shown how to deal with unknown match conditions, but unknown actions are an unsolved problem. We discussed what would be required for a full OpenFlow semantics. In particular, a mutable packet model (cf. Sect. 4.2) would be necessary, which our methods do not support. However, there is no technical need for OpenFlow switches to mix packet filtering with other operations. For example, the pipelined OpenFlow Router architecture constructed by Nelson et al. [57, Sect. 3, Fig. 3] clearly separates packet filtering from packet forwarding and rewriting. In general, using pipeline processing as specified in recent OpenFlow standards [64] might be a step forward to separate filtering from forwarding and rewriting. This may also help compilers which produce OpenFlow rules and suffer from a large blow-up which is induced by a cross product over several tables to join rules for different actions into one table [76]. Such a filtering table implemented by OpenFlow rules without unspecified behavior could be analyzed by our presented methods.

In contrast to firewall rules, OpenFlow flow table entries are usually not written by hand, but high-level programming languages (such as NetCore [52], NetKAT [4], or Flowlog [56]) can be used. The overall question arises whether the analysis of low-level OpenFlow rules is necessary, since for example a verified compiler from NetCore to OpenFlow exists [33]. Therefore, the analysis and verification of the high-level programming language may be more interesting than the analysis of generated low-level OpenFlow entries. The Flowlog language was especially designed with built-in verification and analysis in mind [55, 58] and NetKAT was explicitly designed as a Kleene Algebra with Tests (KAT) which is suitable for formal analysis and it also features an automated decision procedure [30].

This work was motivated by the fact that we could not find any tool which helped us analyze our lab’s and other firewall rulesets. Though much related work about firewall analysis exists, all academic firewall models are too simplistic to be applicable to those real-world rulesets. With the transformations presented in this article, they became processable by existing tools.

We have demonstrated the first fully verified, real-world applicable analysis framework for firewall rulesets. Our tool fffuu supports the Linux iptables firewall because it is widely used and well-known for its vast amount of features. It directly works on iptables-save output. We presented an algebra on common match conditions and a method to translate complex conditions to simpler ones. Further match conditions, which are either unknown or cannot be translated, are approximated in a sound fashion. This results in a translation method for complex, real-world rulesets to a simple model. The evaluation demonstrates that, despite possible approximation, the simplified rulesets preserve the interesting aspects of the original ones.

Based on the simplified model, we presented algorithms to partition the IPv4 and IPv6 address space and compute service matrices. This allows summarizing and verifying the firewall in a clear manner.

The analysis is fully implemented in the Isabelle theorem prover. No additional input or knowledge of mathematics is required by the administrator.

The evaluation demonstrates applicability on many real-world rulesets. For this, to the best of our knowledge, we have collected and published the largest collection of real-world iptables rulesets in academia. We demonstrated that our approach can outperform existing tools with regard to correctness, supported match conditions, CPU time, and memory requirements. Our tool helped to verify lack of errors or, alternatively, to discover previously unknown errors in real-world, production rulesets.

https://​github.​com/​diekmann/​Iptables_​Semantics

It is the first fully machine-verified iptables analysis tool. A stable version of the theory files can also be obtained from the “Archive of Formal Proofs” (AFP) [19, 22, 24, 51]. AFP maintenance policy ensures that our formalization will keep working with newer Isabelle releases.

The raw data of the analyzed firewall rulesets can be found at

https://​github.​com/​diekmann/​net-network

To the best of our knowledge, this is the largest, publicly-available collection of real-world iptables firewall rulesets.