Iptables_Semantics

A formal semantics of the Linux netfilter iptables firewall. Written in the Isabelle interactive proof assistant.

It features

• A real-world model of IPv4/IPv6 addresses as 32bit/128bit machine words.
• Executable code.
• Support for all common actions in the iptables filter table: ACCEPT, DROP, REJECT, LOG, calling to user-defined chains, RETURN, GOTO to terminal chains, the empty action.
• Support for ALL primitive match conditions (by abstracting over unknown match conditions).
• Translation to a simplified firewall model.
• Certification of spoofing protection.
• Service Matrices: For a fixed port, which IP addresses are allowed to connect which other IP addresses? Shows a partition of the complete IPv4/IPv6 addresses.
• ...

Obtaining

$ git clone https://github.com/diekmann/Iptables_Semantics.git

Haskell Tool

Don't want to install Isabelle? Don't want to mess with formulas or proofs? Just want a working tool? Cool, checkout our stand-alone Haskell tool!

Component	Status
Haskell tool

See README.md in haskell_tool.

Further References

Talks

• 32C3: Verified Firewall Ruleset Verification, Cornelius Diekmann, Hamburg, Germany, December 2015 [description] [video] [youtube mirror]

  

Academic Publications

• Cornelius Diekmann, Lars Hupel, Julius Michaelis, Maximilian Haslbeck, Georg Carle. Verified iptables Firewall Analysis and Verification. In Journal of Automated Reasoning, January 2018. [preprint], [springer]
• Cornelius Diekmann, Provably Secure Networks: Methodology and Toolset for Configuration Management. PhD thesis, Technische Universität München, July 2017. [preprint], [mediatum]
• Cornelius Diekmann, Julius Michaelis, Maximilian Haslbeck, and Georg Carle. Verified iptables Firewall Analysis. In IFIP Networking 2016, Vienna, Austria, May 2016. [preprint], [ifip]
• Cornelius Diekmann, Lukas Schwaighofer, and Georg Carle. Certifying spoofing-protection of firewalls. In 11th International Conference on Network and Service Management, CNSM, Barcelona, Spain, November 2015. [preprint], [ieee | paywall]
• Cornelius Diekmann, Lars Hupel, and Georg Carle. Semantics-Preserving Simplification of Real-World Firewall Rule Sets. In 20th International Symposium on Formal Methods, June 2015. [preprint], [springer | paywall]

The raw data of the iptables rulesets from the Examples is stored in this repositoy.

Isabelle Theory Files

This repository is probably not up to date and still uses Isabelle2016-1. Get the theories for the current Isabelle release directly from the afp.

Checking all proofs:

$ isabelle build -v -D . -o document=pdf

This needs about 14 CPU hours (about 7 hours real time on an x220, i7 2.7GHz, 16GB ram). The session Iptables_Semantics_Examples_Large1 needs about 5-6 hours CPU time and Iptables_Semantics_Examples_Large2 needs about 7 hours of CPU time; you may want to skip those.

Building the documentation:

$ isabelle build -d . -v -o document=pdf Iptables_Semantics_Documentation

The build takes less than 10 minutes on my laptop (14min CPU time, 2 threads). The documentation summarizes the most important definitions and theorems. It is deliberately very very brief and only provides results. It should contain the summarizing correctness theorems for all executable functions we export. This is probably the best point to get started working with the theory files.

To develop, we suggest to load the Bitmagic theory as heap-image:

$ isabelle jedit -d . -l Bitmagic

Check the Examples directory to get started

Contributors

• Cornelius Diekmann
• Lars Hupel
• Julius Michaelis
• Max Haslbeck
• Stephan-A. Posselt
• Lars Noschinski