Iptables Semantics

Title:	Iptables Semantics
Authors:	Cornelius Diekmann and Lars Hupel
Submission date:	2016-09-09
Abstract:	We present a big step semantics of the filtering behavior of the Linux/netfilter iptables firewall. We provide algorithms to simplify complex iptables rulests to a simple firewall model (c.f. AFP entry Simple_Firewall) and to verify spoofing protection of a ruleset. Internally, we embed our semantics into ternary logic, ultimately supporting every iptables match condition by abstracting over unknowns. Using this AFP entry and all entries it depends on, we created an easy-to-use, stand-alone haskell tool called fffuu. The tool does not require any input —except for the `iptables-save` dump of the analyzed firewall— and presents interesting results about the user's ruleset. Real-Word firewall errors have been uncovered, and the correctness of rulesets has been proved, with the help of our tool.
BibTeX:	@article{Iptables_Semantics-AFP, author = {Cornelius Diekmann and Lars Hupel}, title = {Iptables Semantics}, journal = {Archive of Formal Proofs}, month = sep, year = 2016, note = {\url{http://isa-afp.org/entries/Iptables_Semantics.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Native_Word, Routing
Used by:	LOFT
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.