Firewall Management With FireWall Synthesizer

Abstract

Firewalls are notoriously hard to con gure and maintain. Policies are written in lowlevel, system-speci c languages where rules are inspected and enforced along non-trivial control ow paths. Moreover, rewalls are tightly related to Network Address Translation (NAT) since lters need to be speci ed taking into account the possible translations of packet addresses, further complicating the task of network administrators. To simplify this job, we propose FireWall Synthesizer (FWS), a tool that decompiles real rewall con gurations from di erent systems into an abstract speci cation. This representation highlights the meaning of a con guration, i.e., the allowed connections with possible address translations. We show the usage of FWS in analyzing and maintaining a con guration on a simple (yet realistic) scenario and we discuss how the tool scales on real-world policies.

Introduction

Firewalls are fundamental mechanisms for the protection of computer networks. The e ectiveness of a rewall system crucially depends on the correctness of its con guration, since an oversight in the policy may have dramatic e ects on the security or the functionality of the entire network.

Firewall management is a complex task also for skilled system administrators. A typical

con guration consists of a large number of rules and it is often hard to understand their e ect on the overall rewall behavior. Moreover, from time to time, con gurations must be adjusted to re ect the updates of the desired security policies. Since rules interact with each other, maintenance must be carefully carried out to avoid introducing unintended behaviors and subtle bugs that could expose the network to external threats.

Typically, policies are written in low-level con guration languages that are speci c to the

rewall system in use and support non-trivial control ow constructs, such as jumps and gotos. Network administrators must also keep in mind how packets are processed by the network stack of the operating system when writing their policy. Further complications come from Network Address Translation (NAT), the mechanism for translating addresses and performing port redirection, which modi es the packets while they traverse the rewall.

To simplify the work of system administrators, we have studied the problem of decompiling real con gurations into abstract speci cations that represent the set of the permitted connections. The abstract version of a rewall policy exposes the meaning of the con guration while discarding all its low-level details, so that it is easier to verify whether the intended security policy is correctly implemented. In addition, by comparing two abstract speci cations, an administrator can spot the di erences between the corresponding real con gurations and check whether the updates have the desired e ect on the rewall behavior.

Our tool FireWall Synthesizer (FWS) supports the above activities. It decompiles a real con guration into a human-readable form and analyzes it checking if it meets a given security

LAN 10.0.0.0/8

54.230.203.47 goal. Di erently from the other tools and techniques proposed in the literature (see e.g., [ 1, 3 ]), the novelty of FWS is that it does not target a speci c rewall system. Indeed, FWS analyzes con gurations for the most used rewall tools in Linux and Unix [ 5, 2, 4 ] and provides partial support for Cisco IOS routers. Furthermore, FWS can be easily extended to support new rewall systems by providing the corresponding front-ends. At [ 6 ] you can download FWS and the examples shown below. A full research paper describing the tool internals, the intermediate language, the algorithm and the underlying theory is presently submitted for presentation at an international conference. 2

FWS in Action

This section illustrates how FWS is used to analyze and manage real rewall con gurations. For lack of space, we only consider the case of iptables but our approach can be directly applied to other systems. Besides synthesizing abstract speci cations of the rewall policies, possibly projected using the query language provided by FWS, we show how the analyses implemented in the tool can be exploited while performing maintenance operations. These analyses include:

Reachability : is a certain host reachable from another one, possibly through NAT?

Policy implication and equivalence: are the packets accepted by one con guration at least/exactly those accepted by a di erent con guration?

Policy di erence: what are the packets accepted by one con guration and denied by another one?

Related rules : which rules a ect the destiny of the packets satisfying a given query?

Case study

We consider the simple (yet realistic) network setup shown in Figure 1:

the LAN network is assigned the set of private IP addresses 10.0.0.0/8; servers and production machines, including the HTTPS web server with address 54.230.203.47 are placed in the demilitarized zone (54.230.203.0/24).

The rewall has three interfaces: eth0 connected to the LAN with IP 10.0.0.1, eth1 connected to the DMZ with IP 54.230.203.1 and ext connected to the Internet with public IP 23.1.8.15.

We want to enforce the following policy on the tra c passing through the rewall: 2

1 * nat 2 # ACCEPT policy in nat chains 3 : PREROUTING ACCEPT [0:0] 4 : INPUT ACCEPT [0:0] 5 : OUTPUT ACCEPT [0:0] 6 : POSTROUTING ACCEPT [0:0] 7 8 # R3 - Apply SNAT on connections from the LAN towards the Internet 9 -A POSTROUTING -s 10.0.0.0/8 -o ext -j MASQUERADE 10 11 COMMIT 12 13 * filter 14 # DROP policy in filtering chains 15 : INPUT DROP [0:0] 16 : FORWARD DROP [0:0] 17 : OUTPUT DROP [0:0] 18 19 # Allow established packets 20 -A FORWARD -m state -- state ESTABLISHED -j ACCEPT 21 # R2 - LAN hosts can connect to DMZ 22 -A FORWARD -s 10.0.0.0/8 -d 54.230.203.0/24 -j ACCEPT 23 # R3 - LAN hosts can connect to the Internet over HTTP / HTTPS 24 -A FORWARD -s 10.0.0.0/8 -o ext -p tcp -- dport 80 -j ACCEPT 25 -A FORWARD -s 10.0.0.0/8 -o ext -p tcp -- dport 443 -j ACCEPT 26 # R1 - Any host can connect to the HTTPS server in the DMZ 27 -A FORWARD -d 54.230.203.47 -p tcp -- dport 443 -j ACCEPT 28 29 COMMIT

R1 Hosts from the Internet can connect to the HTTPS server in the DMZ;

R2 LAN hosts can freely connect to any host in the DMZ;

R3 LAN hosts can connect to the Internet over HTTP and HTTPS (with source NAT).

Analysis of an iptables con guration

where dstIp is the destination address of the packet entering the rewall and state is used to distinguish between new and established connections. The operator == constrains a variable to be equal to a value or inside a certain interval, while && is the logical and. In particular, the query checks whether new connections are allowed towards hosts in the subnet 54.230.203.0/24.

The output of the tool is in Table 1a, where * denotes any value. The rst line of the table states that any host can communicate over HTTPS (port 443) with the server 54.230.203.47 (R1); whereas the second line says that any machine in the LAN can freely communicate with the hosts in the DMZ (R2).

Src IP Src Port * * 10.0.0.0/8 *

Dst IP Dst Port 54.230.203.47 443 54.230.203.0/24 *

Protocol State tcp NEW * NEW (a) Requirements R1 and R2 Src IP Src Port SNAT IP 10.0.0.0/8 * 23.1.8.15 Dst Port 80 443

We now check requirement R3. To do that, we ask which packets from the LAN can reach hosts that are not in the DMZ:

srcIp == 10.0.0.0/8 && not(dstIp == 54.230.203.0/24) && state == NEW The answer to the query is in Table 1b: Internet hosts can be reached over HTTP and HTTPS (ports 80 and 443) and the source IP address of outgoing packets is rewritten to 23.1.8.15, the external address of the rewall. In the fourth column we use n (set di erence) on addresses to denote all addresses except those of the LAN, DMZ and loopback interface (the Internet).

Maintaining existing con gurations

Suppose to add a new computer with IP address 10.13.3.7 to the LAN. Di erently from other machines, we allow access to the hosts on the Internet only over HTTPS. The other requirements on tra c should be preserved. To this purpose, we can add the following rule to the FORWARD chain, which drops connections to port 80 from host 10.13.3.7:

-A FORWARD -s 10.13.3.7 -p tcp --dport 80 -j DROP However, we must be careful about where to place this rule in order to ful ll the desired requirement and avoid to unintentionally block legal tra c.

If we place the new rule at the end of the FORWARD chain, the policy equivalence analysis implemented in FWS reports that the new policy is equivalent to the previous version. Then, we use the related rules analysis to understand which rules are relevant for processing new HTTP packets. The output of this analysis includes the ltering rules at lines 22 and 24 of the

FORWARD chain (see Figure 2):

-A FORWARD -s 10.0.0.0/8 -d 54.230.203.0/24 -j ACCEPT -A FORWARD -s 10.0.0.0/8 -o ext -p tcp --dport 80 -j ACCEPT If we add the new rule before the line 21, FWS reports that the policy is not equivalent to the previous one. In order to check the impact of our changes we run the policy di erence analysis projected over the HTTP tra c using the query protocol == tcp && dstPort == 80. The output is in Table 2. In the rst column, + (resp. -) stands for lines that appear (resp. disappear) in the synthesis after the updates. Now the host 10.13.3.7 cannot connect to the Internet over HTTP, as desired (lower part of Table 2). However, our update also prevents +/+ +/+ communications over HTTP with machines on the DMZ, thus violating the requirement R2 (upper part of Table 2).

The correct placement of the new rule is between the lines 22 and 23, i.e. the rule for the requirement R2 and those for the requirement R3. In this way we allow HTTP tra c from 10.13.3.7 only to the DMZ. If we repeat the analysis, we see that now the only di erence is just in the HTTP tra c towards the Internet, as desired.

3

Conclusions

We have shown how our tool FWS can be used to verify the compliance of a rewall policy with the desired functionality and security requirements of a network in a simple yet realistic case study. Moreover, we have discussed how the various analyses implemented by the tool can to simplify maintenance operations.

In order to evaluate the e ectiveness of FWS on real-world scenarios we have tested on several iptables policies collected by the authors of [ 1 ]. We have measured the time needed by FWS to synthesize policies of size ranging from 15 to 263 rules and most of the analyses terminate in less than 3 seconds. The 3 most complex cases of size 77, 90 and 263 rules terminate in 28, 25 and 355 seconds, respectively. We stress that the reported times are those required to perform a complete synthesis of a policy, whereas in a typical usage the user will run the analyses on a speci c set of hosts or services using the query language of FWS. The thirds argument allows the user to provide fws with input le, the query to execute, the format of the output (e.g., ASCII, LATEX), etc. The options we are using in the following are: Additionally, some useful shorthands are available to project the analysis on speci c subsets of ows that packets can traverse: synthesis implication equivalence diff convert query -i -f -s -q --loopback --input --output --forward --nat --filter

Synthesize a speci cation

Check for policy implication

Check for policy equivalence

Synthesize di erences between two rewalls

Convert a con guration to the generic language

Display the rules that a ect the selected packets

Interfaces le

Main con guration le

Con guration to compare with the main one

Query to check on the main con guration

Flows with local source and local destination

Flows with remote source and local destination

Flows with local source and remote destination

Flows with remote source and remote destination

Flows with NATs

Flows without NATs

Appendix: Using FWS

In this section we describe how using our tool to replicate the results of Section 2. FWS can be downloaded from [ 6 ], and installed following the instruction inside README.MD le.

Once installed, the command fws is available on the command line. The syntax is

fws FRONTEND ACTIONS OPTIONS where FRONTEND speci es which the rewall system we want to decompile: the supported rewalls are cisco, ipfw, iptables, pf. The second argument ACTION de nes the operation to perform on the con guration. Currently, fws implements the following:

In the rest of this section we assume that the current directory contains the les of the directory examples/itasec18 of the archive at [ 6 ]. To decompile the iptables con guration of Figure 1 we invoke fws as follows

$ fws iptables synthesis -i interfaces -f iptables . txt where the le iptables.txt contains the con guration and the le interface the information about each network interface. More precisely, it includes a line for each network interface; each line contains the name of the interface, the address range of the sub-network it communicates with and its IP address. For example, the interface le for our case study contains the following lo eth0 eth1 ext 127.0.0.0/8 10.0.0.0/8 54.230.203.0/24 0.0.0.0/0 127.0.0.1 10.0.0.1 54.230.20 23.1.8.15 For example, the interface eth0 communicates with hosts in the sub-network 10.0.0.0/8 and its IP address is 10.0.0.1.

The content of Tables 1a and 1b are obtained by the following invocations of fws: 6

+/- Src IP Src Port SNAT IP + 10.0.0.0/8 \ { * 23.1.8.15 10.31.3.37 tcp }

To check that the policy obtained by adding the rule to drop connections to port 80 from host 10.13.3.7 at the end of the FORWARD chain is equivalent to the original one, we can run the command

$ fws iptables equivalence -i interfaces -f iptables . txt \ -s iptables_wrong_update_1 . txt

To get the rules that are relevant in processing HTTP packets of new connections we launch fws as follows:

$ fws iptables query -i interfaces -f iptables . txt \ -q " protocol == tcp && dstPort == 80 && state == NEW "

The output of the tool is the following:

-t nat -A POSTROUTING -s 10.0.0.0/8 -o ext -j MASQUERADE -t filter -A FORWARD -s 10.0.0.0/8 -d 54.230.203.0/24 -j ACCEPT -t filter -A FORWARD -s 10.0.0.0/8 -o ext -p tcp -- dport 80 -j ACCEPT

Finally, we can compute the di erence between the original con guration in Figure 1 and the new version concerning the connections to port 80 running:

$ fws iptables diff -i interfaces -f iptables . txt \ -s iptables_correct_update . txt \ -q " protocol == tcp && dstPort == 80 " -- forward The output of the tool, reported in Table 3, shows that our modi cation a ects only connections to the Internet, as expected.

References

[1] Cornelius Diekmann , Julius Michaelis, Maximilian P. L. Haslbeck , and Georg Carle . Veri ed iptables Firewall Analysis . In Proceedings of the 15th IFIP Networking Conference , Vienna, Austria, May 17 -19, 2016 , pages 252 { 260 , 2016 .

[2] The IPFW Firewall . https://www.freebsd.org/doc/handbook/firewalls-ipfw.html.

[3] Robert M. Marmorstein . Formal Analysis of Firewall Policies . PhD thesis , College of William and Mary, Williamsburg, VA, May 2008 .

[4] Packet Filter (PF). https://www.openbsd.org/faq/pf/.

[5] The Net lter Project . https://www.netfilter.org/.

[6] FireWall Synthesizer (FWS): Tool and Examples. https://github.com/secgroup/fws.