FWS: Analyzing,maintaining and transcompiling firewalls

Contributions

Our contributions can be summarized as follows.

We present FWS, a tool that translates real firewall configurations into abstract specifications. Differently from many available tools (cf. Section 8), our approach is independent of the specific target firewall system and language. The abstract specification can be seen as a table that declaratively represents the set of accepted packets with their possible translations. Roughly, each row corresponds to a configuration rule. However, the resulting table is more readable than the standard rulesets, because its rows are independent from each other, while in real firewall configurations the meaning of a rule depends on the others and on the firewall control flow (cf. Section 3.7). As a consequence, the table contains no anomalies, e.g., shadowing or redundancies.

Structure of the paper

In Section 2, we briefly survey iptables, ipfw, pf and Cisco IOS. We describe the syntax of their configuration languages and how they process packets. Section 3 illustrates FWS at work on a small yet realistic scenario. We focus on how network administrators can exploit FWS and use its query language for maintaining various firewall configurations. In particular, we show how one can check host reachability, policy implication, equivalence, difference and non-deterministic behavior, and how one can update the graphical representation of policies. In Section 4 we present our intermediate language IFCL, its formal semantics and the encodings of iptables, ipfw, pf and Cisco IOS. Section 5 presents the logical characterization of all packets accepted and dropped by a firewall, with their possible translations. It also describes the internals of the tool FWS and the algorithm for synthesizing abstract specifications and for analyzing policies. Finally, it proves the correctness of the first two stages of our pipeline. Section 6 describes the last stage, in particular the compilation strategy for generating target configurations. It also proves the source and target configurations equivalent, so establishing the correctness of the whole pipeline. In Section 7, we apply our tool on various real firewall policies to assess its effectiveness, scalability and usability. Section 8 compares our pipeline with other proposal in the literature and Section 9 concludes. All the proofs of our main theorems are in Appendix A that also contains additional results. In Appendix B, there is a table with the main notations used in the paper. Finally, Appendix C describes the command line interface and the SQL-like query language of FWS.

iptables

It is one of the most used tools for packet filtering being the default in Linux. It operates on top of Netfilter, the packets processing framework implemented in the Linux kernel [41].

The basic notions of iptables are tables and chains. Intuitively, a table is a collection of ordered lists of policy rules called chains. The most commonly used tables are: filter for packet filtering; nat for network address translation; mangle for packet alteration. There are five built-in chains that are inspected at specific moments of the packet life cycle [45]: PreRouting, when the packet reaches the host; Forward, when the packet is routed through the host; PostRouting, when the packet is about to leave the host; Input, when the packet is routed to the host; Output, when the packet is generated by the host. Tables do not necessarily contain all the predefined chains and further user-defined chains can be present.

Chains are inspected top-down to find a rule applicable to the packet under elaboration. Each rule specifies a condition and a target: if the packet matches the condition then it is processed according to the specified target, which can be either a built-in target or a user-defined chain. The most commonly used targets are: ACCEPT, to accept the packet; DROP, to discard the packet; RETURN, to stop examining the current chain and resume the processing of a previous chain; DNAT, to perform destination NAT, i.e., a translation of the destination address; SNAT, to perform source NAT, i.e., a translation of the source address. When the target is a user-defined chain, two “jumping” modes are available: call and goto. The difference between the two arises when a RETURN is executed or the end of the chain is reached: the evaluation resumes from the rule following the last matched call (just as for standard call-return of procedures). Some extensions also allow marking packets with a tag and to verify the tag value. Built-in chains have a user-configurable default policy (ACCEPT or DROP) which determines the future of a packet when no rule applies.

ipfw

It is the standard firewall for FreeBSD [44]. A configuration consists of a single ruleset that is inspected twice, when the packet enters the firewall and before it exits. It is possible to specify whether a rule should be applied only in one of the two directions using the keywords in and out.

Similarly to iptables, rules are inspected sequentially until the first match occurs and the corresponding action is taken. The packet is dropped if there is no matching rule. The most common actions in ipfw are the following: allow and deny are used to accept and reject packets; nat applies destination NAT to incoming packets and source NAT to outgoing packets; check-state accepts packets that belong to established connections; skipto, call and return allow to alter the sequential order of inspection of the rules in the ruleset. Differently from iptables, the targets of skipto and call are rules instead of rulesets. A packet is dropped if there is no matching rule.

Packet marking is supported also by ipfw: if a rule containing the tag keyword is applied, the packet is marked with the specified identifier and then processed according to the rule action.

pf

This is the standard firewall of OpenBSD [38] and is included in macOS since version 10.7. Each rule consists of a predicate which is used to select packets and an action that specifies how to process the packets satisfying the predicate. The most frequently used actions are pass and block to accept and reject packets, rdr and nat to perform destination and source NAT. Packet marking works as in ipfw. Differently from the other firewalls, the action taken on a packet is determined by the last matched rule, unless otherwise specified by using the quick keyword. There is a single ruleset in pf that is inspected both when the packet enters and exits the firewall. As in ipfw, keywords in and out can be used to specify whether a rule should be applied only in one direction. When a packet enters the host, DNAT rules are examined first and filtering is performed after the address translation. Similarly when a packet leaves the host: first its source address is translated by the relevant SNAT rules, and then the resulting packet is possibly filtered. Packets belonging to established connections are accepted by default, thus bypassing the filters.

Cisco IOS

It is the network infrastructure software used by Cisco devices, and it is one of the most widespread professional firewall systems. We consider the fragment of Cisco IOS for filtering and NAT. Filtering is configured through Access Control Lists (ACLs), i.e., lists of rules that dictate if a packet is accepted or dropped. ACLs have a default DROP policy: packets that are not accepted by one of the ACL rules are rejected. It is possible to associate at most two ACLs to each firewall interface, one for incoming and one for outgoing packets. NAT is defined in terms of inside and outside IPs, belonging to internal or external networks. To this aim, Cisco IOS requires configuring explicitly the interfaces as NAT inside or NAT outside. Translations can be bidirectional, e.g., when mapping a single IP, or monodirectional, e.g., when the source addresses of a whole private network are translated into a single public IP. A NAT translation happens in between incoming and outcoming filtering and before/after routing depending if it is from outside to inside or vice versa [9].

An overview of FWS interface

FWS is equipped with a graphical interface through which administrators can analyze, maintain and port configurations. The user can switch between query and compiler view. On the one hand, the query view is used to analyze one or more firewall configurations, helping the administrator to check their compliance with security requirements. On the other hand, the compiler view is needed to translate a high level specification of the expected behavior into one of the supported languages.

As shown in Fig. 1, the query view is divided in two panels, the one on the left allows the administrator to encode a series of analyses to be performed on the loaded policies, while the results of those analyses are shown on the right. Firewall policies are loaded and associated to a name using the Load Policy button. Then, the analyses are encoded using the query language, and, finally, they are executed and the results are printed when the Run button is clicked. Analyses are exemplified in the following subsections and discussed in depth in Appendix C.

The compiler view consists of a panel with the tabular representation of the firewall behavior. The administrator can edit the table and compile it in the chosen firewall language. More details are discussed in Section 3.6.

As running example, consider the network shown in Fig. 2. The internal network (10.0.0.0/16) consists of two subnetworks:

network lan0 (i.e. 10.0.1.0/24) contains servers and production machines, including a HTTPS server (web_server: 10.0.1.15) that runs the company website on port 443;

OPEN IN VIEWER

Fig. 2.

A case study of a firewall with three interfaces.

Requirements

We want to enforce the following requirements on the internal and external traffic:

internal networks can freely communicate;

connections to the public IP on ports 443 and 22 are translated (DNAT) to web_server and ssh_server, respectively. This condition permits external hosts to access the website by connecting to the public IP address ext_ip at port 443, that is redirected to the corresponding internal host; similarly for accessing the SSH server;

connections from the internal hosts to the Internet are allowed only towards HTTP and HTTPS web servers, i.e., with destination ports 80 and 443, respectively;

source addresses of packets from the internal hosts to the Internet are translated (SNAT) to the external IP address of the firewall. This allows hosts with private IPs to access the Internet;

the firewall can connect to any other host.

Below, we encode the requirements above as queries that are checked by FWS.

OPEN IN VIEWER

Fig. 3.

The example policy of Section 3.1 in iptables.

We provide a configuration in iptables for the example of Section 3.1. Then, we use FWS to decompile and analyze the configuration and check if it complies with the requirements 1–5 above.

Decompiling and analyzing the configuration

OPEN IN VIEWER

Table 1

Results of FWS when checking the iptables configuration of Fig. 3; * denotes any value, and * ∖ S denotes any value except for those included in S

(a) Requirement 1
Source IP	Source Port	Destination IP	Destination Port	Protocol	State
lan0	*	lan1	*	*	NEW
lan1	*	lan0	*	*	NEW

(b) Requirement 2
Source IP	Source Port	Destination IP	Destination Port	DNAT IP	Protocol	State
*	*	ext_ip	22	ssh_server	tcp	NEW
*	*	ext_ip	443	web_server	tcp	NEW

(c) Requirements 3 and 4
Source IP	Source Port	SNAT IP	Destination IP	Destination Port	Protocol	State
internal	*	ext_ip	* \ {internal}	443, 80	tcp	NEW

(d) Requirement 5
Source IP	Source Port	Destination IP	Destination Port	Protocol	State
ext_ip	*	*	*	*	NEW

We now use FWS to check that the configuration of Fig. 3 meets the requirements 1–5. First, we load the policy p into FWS by specifying the iptables rules and a configuration file that encodes what is shown in Fig. 2. We then ask the tool if arbitrary traffic is allowed among internal networks, raising the query

where srcIp, dstIp represent the fields for source and destination address of the IP packet entering the firewall interfaces, and state tells if a connection is new or established. The query checks whether hosts with srcIp in lan0 can start new connections towards those with dstIp in lan1, or vice versa, as stated by requirement 1. The operator = constrains a variable to be equal to a value or inside a certain interval; the operators and and or stand for logical conjunction and disjunction.

The output we obtain from the tool is in Table 1a. The table contains all the allowed connections matching the query, confirming that requirement 1 is satisfied. Note that FWS supports the projection of the result to a subset of the available columns using the project directive. Hence, from now onwards the results will be projected to the minimum set of columns that represent the considered packets.

We now check that external hosts can access the web and the SSH servers only by connecting to the firewall IP address ext_ip at port 443 and 22 respectively (requirement 2). To do that, we ask which packets reach the web_server and ssh_server hosts:

The operator in constrains a variable to be equal or inside one of the intervals in the list, hence the notation is a syntactic sugar for dnatIp = web_server or dnatIp = ssh_server. The variable dnatIp represents the destination address of the packet after a DNAT translation. The result in Table 1b confirms that requirement 2 is satisfied: indeed, the servers are reachable from any host connecting to the firewall on ports 443 and 22, only.

The next query checks the requirements 3 and 4 together:

Intuitively, the query asks for the new connections that are allowed from an internal source to an external destination. The answer in Table 1c shows that both the requirements are met. Indeed, the notation * \ {internal} represents all destination addresses except those in the internal subnet. Finally, by checking requirement 5 with the query

we obtain the output of Table 1d showing that the firewall can reach any host.

We can thus conclude that the configuration in Fig. 3 is correct with respect to the requirements.

Figure 4 implements the example policy in ipfw. On purpose, we introduce subtle but realistic differences with respect to that of iptables and we show how FWS spots them in a clear and concise way.

OPEN IN VIEWER

Fig. 4.

The policy of Section 3.1 in ipfw.

Decompiling and analyzing the configuration

We now use FWS to check if the configuration of Fig. 4 meets the requirements 1–5 of Section 3.1. We pose exactly the same queries done for iptables in Section 3.2. In fact, one of the advantages of our approach is that the analysis is fully independent of the particular firewall system and of the language analyzed.

Queries for the requirements 1 and 5 give exactly the same results we got for iptables (cf. Tables 2a, 2d and 1a, 1d). Instead, we get an interesting difference while considering requirement 2. For the ipfw configuration we obtain that the web_server and ssh_server hosts cannot be reached by the internal network and by the firewall host via DNAT (cf. Table 2b). This is because in the ipfw configuration, rule 0100 is defined for interface ext, i.e., for packets received from the Internet. In fact, requirement 2 could be interpreted in this stricter way by a system administrator, as hosts web_server and ssh_server are anyway reachable from internal hosts even without DNAT. FWS spots this subtle difference in the two configurations. To make the ipfw configuration behave as the iptables one (for requirement 2), it is enough to remove recv ext from rule 0100.

In checking the requirements 3 and 4, FWS reports that the hosts web_server and ssh_server can start new connections from source ports 443 and 22, respectively, to any other host. This is due to rules 0201 and 0301 that enable the two hosts to answer connections done through the DNAT and provides an alternative way to make connection-oriented protocols work without exploiting the check-state command. In principle, this should be considered non-compliant with requirement 3 as new connections from 443 and 22 from the two hosts will access any port and not just 80 and 443, as requested. Again, FWS spots this difference in the policy. This error can be rectified by removing rules 0201 and 0301 and by adding the keep-state keyword to the rules 0200 and 0300.

Interestingly, FWS can compute the equivalence of configurations written for different firewall systems/languages. In this particular case, FWS outputs that the fixed ipfw configuration and the iptables one are equivalent, as far as the five requirements are in order.

OPEN IN VIEWER

Fig. 5.

The example policy of Section 3.1 in Cisco IOS.

Figure 5 implements the example policy in Cisco IOS. As done in Section 3.3, we show that naively porting the iptables introduces subtle differences that violate the requirements, spotted by FWS.

Decompiling and analyzing the configuration

OPEN IN VIEWER

Table 3

Results of FWS when checking the Cisco IOS configuration of Fig. 5

(a) Requirement 1
Source IP	Source Port	Destination IP	Destination Port	Protocol	State
lan0	*	lan1	*	*	NEW
lan1	*	lan0	*	*	NEW

(b) Requirement 2
Source IP	Source Port	Destination IP	Destination Port	DNAT IP	Protocol	State
* \ { lan0, lan1, ext_ip }	*	ext_ip	22	ssh_server	tcp	NEW
* \ { lan0,  lan1, ext_ip }	*	ext_ip	443	web_server	tcp	NEW

(c) Requirements 3 and 4
Source IP	Source Port	SNAT IP	Destination IP	Destination Port	Protocol	State
lan0, lan1	*	ext_ip	* \ {internal}	443, 80	tcp	NEW

(d) Requirement 5
Source IP	Source Port	Destination IP	Destination Port	Protocol	State
ext_ip	*	*	443, 80	tcp	NEW
ext_ip	*	lan0, lan1	*	*	NEW

(e) Requirement 5 for the fixed configuration
Source IP	Source Port	Destination IP	Destination Port	Protocol	State
ext_ip	*	*	*	*	NEW

As we did for ipfw, we use FWS to check if the configuration of Fig. 5 meets the requirements 1–5 of Section 3.1.

Queries for the requirements 1, 3 and 4 give exactly the same results obtained for iptables (cf. Tables 3a, 3c and 1a, 1c). Similarly to ipfw, for requirement 2, we get that web_server and ssh_server hosts cannot be reached by the internal network (and by the firewall) via DNAT (cf. Table 3b). This is consistent with the fact that DNAT only applies from outside to inside IPs. Access to local servers for Cisco IOS networks is usually achieved through a suitable DNS configuration, as often discussed in official support forums. The most important difference concerns requirement 5: since we are filtering on the ext interface we cannot distinguish packets coming from internal networks, going through the source NAT, from packets originated by the firewall. They both have the same source IP when they reach the ext out interface. As a consequence requirement 5 cannot be satisfied: the firewall will be subject to the same filters as the internal networks.

In order to fix this issue we reconfigure the firewall so as to place output filters in the internal interfaces. In particular we disable ACL 120 in ext out and enable the following ACL 140 in both lan0 in and lan1 in:

By ACL 140 we enforce the filters on destination ports 80 and 443 (requirement 3) and enable internal traffic (requirement 1), together with established connections. Running again FWS we get that requirement 5 is satisfied by the new configuration (cf. Table 3e).

Some languages permit writing rules that translate the addresses of a packet into values not uniquely specified. For example, the NAT rules in iptables can specify a range of addresses within which a specific one is taken at run time, and the manual does not precisely state which value is chosen. We empirically observed that round robin is commonly used to redirect connection requests to a pool of duplicated servers so implementing a rough load balancing mechanism.

Since the actions of the firewall depend on the field values of the packet, such unspecified choices may unpredictably influence the effect of the subsequent rules. It may even happen that a packet is accepted if one value in the permitted range is used in the translation, or dropped if another admissible value is used instead. In other words, given two completely identical connection requests, received while the system is in the same state, the firewall may misbehave, by refusing the first and accepting the second. Regardless of other legitimate usages, this kind of non-determinism is arguably a misbehaviour.

Now we show how FWS can detect non-determinism of policies. Suppose that the web_server host has a slow backend so we replicate it for ensuring an acceptable quality of service. The new servers are assigned IP addresses 10.0.1.16 and 10.0.1.17. In this scenario iptables can also be used for load balancing at the connection level, by specifying a range of IP addresses in the DNAT target:

This rule redirects new connections to a different server in the range following a round-robin discipline. The packets after the DNAT need to be explicitly accepted in the FORWARD chain:

Suppose now that the host 10.0.1.16 is isolated from the network for maintenance or to mitigate a breach. A naive solution is dropping every connection directed to the server:

However, this rule introduces non-determinism in the firewall behavior: a connection to ext_ip on port 443 is dropped if the DNAT target is 10.0.1.16, while it is accepted if another server is selected. Our tool identifies these situations and synthesizes the affected packets. The following query performs this check, and the output in Table 4 confirms that the examined configuration is non-deterministic:

OPEN IN VIEWER

Fig. 6.

FWS editing and compiling a table.

The synthesis procedure returns a table consisting of a complete declarative description of the behavior of the firewall. In this way, the administrator can inspect the semantics of the configuration in a visual readable way. In addition, FWS can compile this description into any of the supported languages, for porting (when source and target languages are different) or refactoring (when source and target languages coincide).

For example, for porting the iptables policy presented in Section 3.2 to ipfw, the administrator (1) selects the compiler view of FWS, (2) loads the iptables policy, (3) synthesizes its declarative specification, and, finally, (4) compiles the table to ipfw. As shown in Fig. 6, the compiler view is composed by a single panel that shows the semantics of the firewall, plus a recap of the aliases. Once one of the supported language is selected, the compile button generates a proper policy, complying with the expected semantics.

Before compiling, the administrator can act on the expected semantics by editing the declarative specification in the table obtained through decompilation. Every field of the rows is editable and new rows can be added in order to change the declarative semantics of the firewall. In this way, the configuration can be repaired or modified to comply with new specifications.

In this section, we show how FWS can be used to perform maintenance of the iptables policy presented in Section 3.2.

Suppose that the company has added a new machine to the lan0 subnet, which has been assigned the IP address 10.0.1.22. Differently from the other hosts of the network, we want to allow Internet access (with SNAT) to this machine only over HTTPS. The other requirements on the traffic should be preserved. We can proceed at two different levels: at the low level by editing the iptables policy in hand, or at the high level by operating directly on the table. Maintaining a firewall configuration by editing the table is easier, faster and safer. We recommend it rather than maintaining the source configuration by hand. Given the intricacy of traditional firewall configuration languages, they are viewed as machine code in the approach we advocate. Their management should be performed by administrators through dedicated tools. Only specialized technicians may be interested in interacting directly with the low level for performing specific tasks.

Maintaining by editing the configuration

To edit the iptables policy directly, we add the following rule to the FORWARD chain, which drops connections to port 80 from host 10.0.1.22:

However, we must be careful about the position where to place this rule in order to fulfill the desired requirement and avoid to unintentionally block legal traffic. We discuss below three cases and show how FWS helps in determining the correct position.

The first case is when we place the new rule at the end of the FORWARD chain, which has no effect: the policy equivalence analysis of FWS reports that the new policy is equivalent to the previous version. To understand the reason why, we use the related rules analysis to detect which rules are relevant for processing HTTP packets. The output of the tool only includes the following filtering rule from the FORWARD chain:

The above rule accepts all the HTTP traffic from the internal networks and is evaluated before the new DROP rule. Hence, our new rule should be placed before this one.

The second case is when we insert the new rule before those of the other requirements, e.g., after the rules that allow packets of incoming connections. Now, FWS reports that the policy is not equivalent to the previous one. We check the impact of our changes by running the policy difference analysis projected over the HTTP traffic:

The answer to the query is shown in Table 5a. The first column is + or - for lines that appear in the synthesis or disappear after the updates, respectively. We see that host 10.0.1.22 is now unable to connect to the Internet, as desired (second table of Table 5a). However, our update also prevents communications over HTTP with other machines on the internal networks, thus violating requirement 1 (first table of Table 5a).

OPEN IN VIEWER

Table 5

Maintenance of the iptables configuration. The rules in lines with a + are added, while those with a − are removed

(a) Policy differences after the wrong update
+/-	Source IP	Source Port	Destination IP	Destination Port	Protocol	State
+	internal \ {10.0.1.22}	*	internal	80	tcp	NEW
-	internal	*	internal	80	tcp	NEW

+/-	Source IP	Source Port	SNAT IP	Destination IP	Destination Port	Protocol	State
+	internal \ {10.0.1.22}	*	ext_ip	* \ {internal}	80	tcp	NEW
-	internal	*	ext_ip	* \ {internal}	80	tcp	NEW

(b) Policy differences after the correct update
+/-	Source IP	Source Port	SNAT IP	Destination IP	Destination Port	Protocol	State
+	internal \ {10.0.1.22}	*	ext_ip	* \ {internal}	80	tcp	NEW
-	internal	*	ext_ip	* \ {internal}	80	tcp	NEW

The correct place where to add the new rule is between the rule for requirement 1 and those for requirement 3. In this way we only allow HTTP traffic from 10.0.1.22 to the internal networks. If we repeat the check for policy difference, we see that now the only difference is just in the HTTP traffic towards the Internet, as desired (cf. Table 5b).

4.1. Decompiling real languages into IFCL

Here we encode the firewalls system considered so far as triples ( C , ρ , c ) of our framework (stage 1). Notably, the encoding provides a formal semantics for those systems defined in terms of IFCL (see Section 4.2).

Modelling iptables. Let L be the set of local addresses of a host, i.e., those associated with its network interface; and let ψ 1 and ψ 2 be the predicates over packets defined as follows: ψ 1 ( p ) = s a ( p ) ∈ L ψ 2 ( p ) = d a ( p ) ∈ L . Figure 7a shows the control diagram C of iptables, where unlabeled arcs carry the label “ true .” It also implicitly defines the transition function according to Definition 5. In iptables there are twelve built-in chains, each of which correspond to a single ruleset. So we define the set ρ p ⊆ ρ iptables of primitive rulesets as the one made of R I NP man , R I NP nat , R I NP fil , R O UT man , R O UT nat , R O UT fil , R P RE man , R P RE nat , R F OR man , R F OR fil , R P OST man and R P OST nat , where the superscript represents the chain name and the subscript the table name. Needless to say, the set ρ iptables ∖ ρ p contains the user-defined chains.

The mapping function c : Q ↦ ρ is defined as follows: c ( q i ) = R c ( q f ) = R c ( Pre m ) = c ( Pre M ) = R P RE man c ( Pre n ) = R P RE nat c ( Inp m ) = c ( Inp M ) = R I NP man c ( Fwd f ) = R F OR fil c ( Inp n ) = R I NP nat c ( Inp f ) = R I NP fil c ( Out m ) = R O UT man c ( Out n ) = R O UT nat c ( Out f ) = R O UT fil c ( Fwd m ) = R F OR man c ( Fwd f ) = R F OR fil c ( Post m ) = R P OST man c ( Post n ) = R P OST nat where R is an empty ruleset with ACCEPT as default policy.

Finally, note that the action CALL(_) implements the built in target JUMP(_) .

Modelling ipfw.  The control diagram C of ipfw, displayed in Fig. 7b, is simpler than the one of iptables. The node Inp represents the procedure executed when an IP packet reaches the host from the net. Dually, Out is for when the packet leaves the host. The predicates ψ 1 , ψ 2 are defined as for iptables and check whether the packet has been generated by or is addressed to the host itself, respectively. The transition function δ easily follows from C , according to Definition 5.

OPEN IN VIEWER

Fig. 7.

Control diagrams of the four firewall languages.

We present the construction of the rulesets associated with the node Inp . Let R = [ r id 1 , … , r id k ] be the unique ruleset of ipfw, where id i are numeric identifiers associated with the rules, and the last rule r id k encodes the default policy set by the user. The idea is to generate k different rulesets R i I , one for each rule in R. If the rule r id i contains the keyword out, i.e., the rule is not considered when the packet enters the firewall, we let R i I = [ ( true , GOTO( R i + 1 I ) ) ] . Otherwise, we define R i I = [ trs ( r id i ) , ( true , GOTO( R i + 1 I ) ) ] , where the translation trs is defined by cases below: trs ( r ) = ( ϕ , GOTO( R n I ) ) if r = ( ϕ , skipto id n ) ( ϕ , CALL( R n I ) ) if r = ( ϕ , call id n ) ( ϕ , t ) if r = ( ϕ , t ) The construction of the rulesets R i O for the node Out is similar, but in this case the rules containing the keyword in are ignored. The mapping function c returns R 1 I for Inp , R 1 O for Out , and empty ruleset with ACCEPT as default policy for q i and q f . These rulesets form the component ρ ipfw .

Modelling pf. Also pf has a single ruleset and, differently from above, the rule applied to a packet is the last matching one, except in the case of the so-called quick rules: as soon as one of these matches the packet, its action is applied and the remaining part of the ruleset is skipped.

Figure 7c shows the control diagram C pf for pf. The nodes Inp n and Inp f represent the procedure executed when an IP packet reaches the host from the net. Dually, Out n and Out f are for when the packet leaves the host. The predicates ψ 1 and ψ 2 are those defined for iptables. Given the pf ruleset R pf we include the following rulesets in ρ pf :

R dnat contains the rule ( state = = 1 , CHECK-STATE ( → ) ) as the first one, followed by all the rules rdr of R pf ;

Modelling Cisco IOS. The control diagram C of Cisco IOS is displayed in Fig. 7d. The predicate ψ 1 is as for iptables and checks whether the packet has been generated by the host. In this case, it only goes through the output filters. Each device interface I is associated with the two rulesets, or ACLs, R in I and R out I , applied to incoming and outgoing packets with DROP as default policy. If there is no ACL for direction d (in or out) we let R d I be empty, with ACCEPT as default policy. Let I 1 , … , I n be the firewall interfaces, with I n representing the interface corresponding to the default gateway. We let R in = ( srcIp ∈ net ( I 1 ) , GOTO( R in I 1 ) ) , … , ( srcIp ∈ net ( I n − 1 ) , GOTO( R in I n − 1 ) ) , ( true , GOTO( R in I n ) ) R out = ( dstIp ∈ net ( I 1 ) , GOTO( R out I 1 ) ) , … , ( dstIp ∈ net ( I n − 1 ) , GOTO( R out I n − 1 ) ) , ( true , GOTO( R out I n ) ) where net ( I ) is the set of IP addresses of the interface I. Intuitively, R in / R out apply the ACL of the interface that corresponds to the packet source/destination IP address. We do not consider here the case of overlapping networks on different interfaces, meaning that net ( I j ) are all disjoint sets. When no match is found the default gateway interface is chosen.

We let R inat contain the rule ( state = = 1 , CHECK-STATE ( → ) ) as the first one, followed by all the NAT rules that translate outside addresses into inside ones. Dually, we let R onat contain the rule ( state = = 1 , CHECK-STATE ( ← ) ) as the first one, followed by all the NAT rules that translate inside addresses into outside ones. When NAT is bidirectional (as the DNAT in the example of Fig. 5) the corresponding CHECK-STATE is omitted, since a single NAT rule is modeled as two complementary (SNAT/DNAT) IFCL rules. The mapping function c ios is defined as follows, where R is an empty ruleset with ACCEPT as default policy: c ios ( q i ) = R c ios ( In f ) = R in c ios ( Out n ) = R onat c ios ( q f ) = R c ios ( In n ) = R inat c ios ( Out f ) = R out

Now, we formally define the semantics of IFCL through two transition systems operating in a master-slave fashion. The master has a labeled transition relation of the form s → p , p ′ s ′ . The intuition is that the state s of a firewall changes to s ′ when a new packet p reaches the host and becomes p ′ .

The configurations of the slave transition system are triples ( q , s , p ) where:

q ∈ Q is a control diagram node;

In the slave transition relation, we use the following predicate, which describes an algorithm that runs a ruleset R on a packet p in the state s p , s ⊧ R S ( t , p ′ ) This predicate searches for a rule in R matching the packet p through p ⊧ R ( t , i ) . If it finds a match with target t, t is applied to p to obtain the packet p ′ resulting from possible transformations.

Recall that actions CALL(R) , RETURN and GOTO(R) are similar to procedure calls, returns and jumps in imperative programming languages. To correctly deal with them, our predicate p , s ⊧ R S ( t , p ′ ) uses a stack S to implement a behavior similar to the one of procedure calls. We will denote with ϵ the empty stack and with · the concatenation of elements on the stack. This stack is also used to detect and prevent loops in ruleset invocation, as it is the case in real firewalls.

In the stack S we overline a ruleset R to indicate that it was pushed by a GOTO(_) and it has to be skipped when returning. For that, we use the following pop ∗ function in the semantics of the RETURN : pop ∗ ( ϵ ) = ϵ pop ∗ ( R · S ) = ( R , S ) pop ∗ ( R ‾ · S ) = pop ∗ ( S ) If the top of S is overlined, pop ∗ behaves as a standard pop operation; otherwise it extracts the first non-overlined ruleset. When S is empty, we assume that pop ∗ returns ϵ to signal the error.

Furthermore, in the definition of p , s ⊧ R S ( t , p ′ ) the notation R k indicates the ruleset [ r k , … , r n ] ( k ∈ [ 1 , n ] ) resulting from dropping the first k − 1 rules from the given ruleset R = [ r 1 , … , r n ] .

We also assume as given the function establ that, taken an action α from the state, a packet p and the fields X ∈ { ← , → , ↔ } to rewrite, returns a possibly changed packet p ′ , e.g., in case of an established connection. Also establ depends on the specific firewall we are modeling, and so it is left unspecified.

Finally, we assume as given a function nat ( p , s , d n , s n ) that returns the packet p translated under the corresponding NAT operation in the state s. The argument d n is used to modify the destination range of p, i.e., destination NAT (DNAT), while s n is used to modify the source range, i.e., source NAT (DNAT). Recall that a range of the form ⋆ : ⋆ is interpreted as the identity translation, whereas one of the form a : ⋆ modifies only the address. Also this function is left abstract.

Table 7 shows the rules defining p , s ⊧ R S ( t , p ′ ) . The first inference rule deals with the case when the packet p matches a rule with target ACCEPT or DROP ; in this case the ruleset execution stops returning the found action and leaving p unmodified. When a packet p matches a rule with action CHECK-STATE , we query the state s: if p belongs to an established connection, we return ACCEPT and p ′ , obtained rewriting p. Otherwise, p is matched against the remaining rules in the ruleset. When a packet matches a NAT rule, we return ACCEPT and the packet resulting by the invocation of the function nat . There are two cases when a packet p matches a GOTO(_) . If the ruleset R ′ is not already in the stack, we push the current ruleset R onto the stack overlined to record that this ruleset dictated a GOTO(_) . Otherwise, R ′ is in the stack, we detect the loop and discard p. The case when a packet p matches a rule with action CALL(_) is similar, except that the ruleset pushed on the stack is not overlined. When p matches a rule with action RETURN , we pop the stack and match p against the top of the stack. Finally, when no rule matches, an implicit return occurs: we continue from the top of the stack, if non empty. The MARK rule simply changes the tag of the matching packet to the value m. If none of the above applies, we return the default action t d of the current ruleset.

We now define the slave transition relation as follows. c ( q ) = R p , s ⊧ R ϵ ( ACCEPT , p ′ ) δ ( q , p ′ ) = q ′ ( q , s , p ) → ( q ′ , s , p ′ ) The rule describes how we process the packet p when the firewall is in state s and performs the step represented by the node q. We match p against the ruleset R associated with q and if p is accepted as p ′ , we continue considering the next step of the firewall execution represented by the node q ′ .

Finally, we define the master transition relation that transforms states and packets as follows (as usual, below → + stands for the transitive closure of →): ( q i , s , p ) → + ( q f , s , p ′ ) s → p , p ′ s ⊎ ( p , p ′ ) This rule says that when the firewall is in the state s and receives a packet p, it elaborates p starting from the initial node q i of its control diagram. If this elaboration succeeds, i.e., if the node q f is reached, p is accepted as p ′ , and we update the state s by storing information about p, its translation p ′ and the connection they belong to, by the function ⊎, left unspecified for the sake of generality.

We empirically validated the semantics inherited from IFCL by the firewall systems we have considered in Section 4.1. The validation process is composed of three main phases.

We first inferred the expected behavior of the various processing steps of the real firewall system F in hand from its documentation, and collected a set of configurations playing the role of test cases T. We then run F in a simulated environment, built on some virtual machines. Also, we synthesize the abstract specification of F through FWS. Furthermore, we generated synthetic network traffic to make sure that we cover all the test cases in T. Finally, we compare the logs of F against the results obtained by FWS, so as to check the correspondence between the actual behavior of F and the one dictated by the semantics it inherits from IFCL.

We focused on corner cases that are not clearly explained in the official documentation of F , or not even taken into account. Feedback from system administrators has been particularly helpful in detecting these cases. Often the corner cases concern local packets, i.e., packets generated by the firewall and directed to a local address of the firewall itself, in combination with NAT rules.

As an example, consider iptables. A local packet first enters the Output chain, being generated by the host, and then the PostRouting chain. Instead of leaving the firewall, it enters the PreRouting and Input chains, being also a packet directed to a local address. In these two chains, the processing of this kind of packets differs from the one of a generic packet coming from outside F . Indeed a local packet does not traverse the nat table in the PreRouting and Input chains, skipping the NAT processing. This behavior is correctly encoded in the control diagram of Fig. 7a. The validation phase sketched above helped us in discovering this subtle behavior, which was not considered in the preliminary version of the iptables control diagram [6].

5.1. Unfolding rulesets

Our intermediate language deals with involved control flows, by using the targets GOTO(_) , CALL(_) and RETURN (see Example 1). The following unfolding operation ⟦ _ ⟧ rewrites a ruleset into an equivalent one with no such control flow rules.

Hereafter, let r ; R be a non empty ruleset consisting of a rule r followed by a possibly empty ruleset R; and let R 1 @ R 2 be the concatenation of R 1 and R 2 .

The unfolding of a ruleset R is defined as follows: ⟦ R ⟧ = ∙ ⟦ R ⟧ { R } true m ⟦ ϵ ⟧ I f = ϵ m ⟦ ( ϕ , t ) ; R ⟧ I f = ( f ∧ ϕ ′ , t ) ; m ⟦ R ⟧ I f if t ∉ { RETURN , CALL(R’) , GOTO(R’) , MARK ( m ) } m ⟦ ( ϕ , RETURN ) ; R ⟧ I f = m ⟦ R ⟧ I f ∧ ¬ ϕ ′ m ⟦ ( ϕ , CALL(R’) ) ; R ⟧ I f = m ⟦ R ′ ⟧ I ∪ { R ′ } f ∧ ϕ ′ @ m ⟦ R ⟧ I f if R ′ ∉ I ( f ∧ ϕ ′ , DROP ) ; m ⟦ R ⟧ I f otherwise m ⟦ ( ϕ , GOTO(R’) ) ; R ⟧ I f = m ⟦ R ′ ⟧ I ∪ { R ′ } f ∧ ϕ ′ @ m ⟦ R ⟧ I f ∧ ¬ ϕ ′ if R ′ ∉ I ( f ∧ ϕ ′ , DROP ) ; m ⟦ R ⟧ I f ∧ ¬ ϕ ′ otherwise m ⟦ ( ϕ , MARK ( m ′ ) ) ; R ⟧ I f = ( f ∧ ϕ ′ , MARK ( m ′ ) ) ; m ′ ⟦ R ⟧ I f ∧ ϕ ′ @ m ⟦ R ⟧ I f ∧ ¬ ϕ ′ where ϕ ′ is ϕ with its sub-predicate on the current tag replaced by its evaluation on m.

The auxiliary procedure m ⟦ R ⟧ I f recursively inspects the ruleset R. The formula f accumulates conjuncts of the predicate ϕ ′ ; the set I stores the rulesets traversed by the procedure and helps detecting loops; m records the tag associated with the packets that satisfy f. If a rule neither affects the control flow nor it is a MARK , we just substitute the conjunction f ∧ ϕ ′ for ϕ, and continue to analyze the rest of the ruleset with the recursive call m ⟦ R ⟧ I f .

In the case of a return rule ( ϕ , RETURN ) we generate no new rule, and we continue to recursively analyze the rest of the ruleset, by updating f with the negation of ϕ ′ . For the rule ( ϕ , CALL(R’) ) we have two cases: if the callee ruleset R ′ is not in I, we replace the rule with the unfolding of R ′ with f ∧ ϕ ′ as predicate, and append { R ′ } to the traversed rulesets; if R ′ is already in I, i.e., we have a loop, we replace the rule with a DROP , with f ∧ ϕ ′ as predicate; in both cases, we continue unfolding the rest of the ruleset. We deal with the rule ( ϕ , GOTO(R’) ) as in the previous one, except that the rest of the ruleset has f ∧ ¬ ϕ ′ as predicate. Finally, the rule ( ϕ , MARK ( m ′ ) ) originates two lists. The first is for the packets satisfying ϕ ′ and thus the rule becomes ( f ∧ ϕ ′ , MARK ( m ′ ) ) and its tag m ′ . The other list is for packets not satisfying ϕ ′ , so MARK ( m ′ ) never applies and the tag m is left unchanged.

We now prove that a firewall F and its unfolded version ⟦ F ⟧ are semantically equivalent, i.e., they perform the same action over a given packet p in a state s, and reach the same state s ′ . Formally:

Theorem 1 (Correctness of unfolding).

Let F = ( C , ρ , c ) be a firewall and ⟦ F ⟧ its unfolding. Let s → p , p ′ X s ′ be a step of the master transition system performed by the firewall X ∈ { F , ⟦ F ⟧ } . Then s → p , p ′ F s ′ ⟺ s → p , p ′ ⟦ F ⟧ s ′ .

5.2. Logical characterization of firewalls

We construct two logical predicates that characterize the packets accepted and those dropped by an unfolded ruleset, together with the relevant translations.

To deal with NAT, we define an auxiliary function tr that computes the set of packets resulting from all possible translations of a given packet p. The parameter X ∈ { ← , → , ↔ } specifies if the translation applies to source, destination or both addresses, respectively, similarly to CHECK-STATE ( X ) . tr ( p , d n , s n , ↔ ) ≜ { p [ d a ↦ a d , s a ↦ a s ] | a d ∈ d n , a s ∈ s n } tr ( p , d n , s n , → ) ≜ { p [ d a ↦ a d ] | a d ∈ d n } tr ( p , d n , s n , ← ) ≜ { p [ s a ↦ a s ] | a s ∈ s n } Furthermore, we model the default policy of a ruleset R with the predicate d p , true when the policy is ACCEPT , false otherwise.

Given an unfolded ruleset R, we build two predicates: P R ( p , p ˜ ) that holds when the packet p is accepted as p ˜ by R, and D R ( p ) when p is instead dropped. Their definition in Table 9 induces on the rules in R. Recall that formulas ϕ also predicate on the firewall state, e.g., checking if the packet belongs to an established connection. As a sanity check, we assume that this is always the case when the target is CHECK-STATE . We briefly comment on the definition of P R ( p , p ˜ ) . The empty ruleset applies the default policy d p ( R ) and does not transform the packet, reflected by the constraint p = p ˜ . The rule ( ϕ , ACCEPT ) considers two cases: when ϕ ( p ) holds and the packet is accepted as it is; when instead ¬ ϕ ( p ) holds, p is accepted as p ˜ only if the continuation R accepts it. The rule ( ϕ , DROP ) accepts p only if the continuation does and ϕ ( p ) is false. The rule ( ϕ , NAT ( d n , s n ) ) works similarly to the rule ( ϕ , ACCEPT ) , expect that, when ϕ ( p ) holds, and it gives p ˜ by applying to p the NAT translations tr ( p , d n , s n , ↔ ) . Finally, ( ϕ , CHECK-STATE ( X ) ) works similarly to the rule NAT that applies all possible translations of kind X (written as tr ( p , ⋆ : ⋆ , ⋆ : ⋆ , X ) ). Intuitively, we over-approximate the state by considering any possible translations, because we abstract away from the actual established connections. At run-time, only the connections corresponding to the actual state will be possible. The rule ( ϕ , MARK ( m ) ) works similarly to the rule NAT, but when ϕ ( p ) holds it requires that the continuation accepts p tagged by m as p ˜ . Apart from being monadic, the definition of D R ( p ) follows the same schema.