Skip to main page content
U.S. flag

An official website of the United States government

Dot gov

The .gov means it’s official.
Federal government websites often end in .gov or .mil. Before sharing sensitive information, make sure you’re on a federal government site.

Https

The site is secure.
The https:// ensures that you are connecting to the official website and that any information you provide is encrypted and transmitted securely.

Access keys NCBI Homepage MyNCBI Homepage Main Content Main Navigation
. 2018;61(1):191-242.
doi: 10.1007/s10817-017-9445-1. Epub 2018 Jan 3.

Verified iptables Firewall Analysis and Verification

Cornelius Diekmann  1 , Lars Hupel  1 , Julius Michaelis  1 , Maximilian Haslbeck  1 , Georg Carle  1
Affiliations

Verified iptables Firewall Analysis and Verification

Cornelius Diekmann et al. J Autom Reason. 2018.

Abstract

This article summarizes our efforts around the formally verified static analysis of iptables rulesets using Isabelle/HOL. We build our work around a formal semantics of the behavior of iptables firewalls. This semantics is tailored to the specifics of the filter table and supports arbitrary match expressions, even new ones that may be added in the future. Around that, we organize a set of simplification procedures and their correctness proofs: we include procedures that can unfold calls to user-defined chains, simplify match expressions, and construct approximations removing unknown or unwanted match expressions. For analysis purposes, we describe a simplified model of firewalls that only supports a single list of rules with limited expressiveness. We provide and verify procedures that translate from the complex iptables language into this simple model. Based on that, we implement the verified generation of IP space partitions and minimal service matrices. An evaluation of our work on a large set of real-world firewall rulesets shows that our framework provides interesting results in many situations, and can both help and out-compete other static analysis frameworks found in related work.

Keywords: Computer networks; Firewalls; Formal verification; Iptables; Isabelle; Netfilter; Semantics.

PubMed Disclaimer

Figures

Fig. 1
Fig. 1
Linux iptables ruleset of a Synology NAS (network attached storage) device
Fig. 2
Fig. 2
Big-step semantics for iptables
Fig. 3
Fig. 3
Alternative big-step semantics for iptables
Fig. 4
Fig. 4
Unfolded Synology firewall
Fig. 5
Fig. 5
Excerpt (first rules) of the 2013 iptables ruleset of our lab
Fig. 6
Fig. 6
Example ruleset. (Color figure online)
Fig. 7
Fig. 7
Service matrix of ruleset in Fig. 6
Fig. 8
Fig. 8
Lab SSH Service Matrix (2015)
Fig. 9
Fig. 9
Lab SSH Service Matrix with raw IP addresses (2015)
Fig. 10
Fig. 10
Lab IPv4 HTTP Service Matrix (2016)
Fig. 11
Fig. 11
Lab IPv6 HTTP Service Matrix (2016)
Fig. 12
Fig. 12
Firewall D SSH service matrix with input and output port rewriting
Fig. 13
Fig. 13
HTTP service matrix with state of a Docker host
See this image and copyright information in PMC

References

    1. Al-Shaer, E., Alsaleh, M.: ConfigChecker: a tool for comprehensive security configuration analytics. In: Configuration Analytics and Automation (SAFECONFIG), pp. 1–2. IEEE (2011). 10.1109/SafeConfig.2011.6111667
    1. Al-Shaer, E., Hamed, H.: Discovery of policy anomalies in distributed firewalls. In: Annual Joint Conference of the IEEE Computer and Communications Societies (INFOCOM), vol. 4, pp. 2605–2616 (2004). 10.1109/INFCOM.2004.1354680
    1. Analyzed firewall rulesets (raw data). https://github.com/diekmann/net-network. Accompanying material
    1. Anderson, C.J., Foster, N., Guha, A., Jeannin, J.B., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: semantic foundations for networks. In: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, pp. 113–126. ACM, San Diego (2014). 10.1145/2535838.2535862
    1. Baker, F., Savola, P.: Ingress filtering for multihomed networks. RFC 3704 (Best Current Practice) (2004)

LinkOut - more resources