/Iptables_Semantics

Verified iptables Firewall Ruleset Analysis
  1. Isabelle 86.4%
  2. Haskell 8.9%
  3. TeX 3.5%
  4. Shell 0.5%
  5. Python 0.3%
  6. Standard ML 0.3%
  7. HTML 0.1%
Isabelle Haskell TeX Shell Python Standard ML HTML
Find file
Latest commit e505210 Dec 16, 2016 @diekmann unbreaking tests
Permalink
Failed to load latest commit information.
.travis stack support Jul 20, 2016
haskell_tool unbreaking tests Dec 16, 2016
images fffuu logo src Mar 14, 2016
thy Restore root files from non-afp version Nov 21, 2016
.gitignore Organize the two OpenFlow pdfs into one for the AFP Oct 5, 2016
.gitmodules removed l4v from .gitmodules Jun 23, 2016
.travis.yml tuned Jul 21, 2016
LICENSE full name to LICENSE Apr 20, 2016
README.md logopath Dec 16, 2016
ROOTS new directory structure Dec 4, 2015
check_theorems_doc.sh Short documentation string in check_theorems_doc.sh Aug 22, 2016

README.md

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.
  • ...

isabelle/hol logo

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!

FFFUU logo

Component Status
Haskell tool Build Status

See README.md in haskell_tool.

Isabelle Theory Files

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

Further References

Talks

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

Academic Publications

  • Cornelius Diekmann, Julius Michaelis, Maximilian Haslbeck, and Georg Carle. Verified iptables Firewall Analysis. In IFIP Networking 2016, Vienna, Austria, May 2016. [preprint]
  • 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]
  • 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.

Contributors