Iptables_Semantics.

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 (http://iptables.isabelle.systems). 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, as well as the correctness of rulesets has been proven with the help of our tool. For a detailed description, see [2, 4, 3, 1]. Acknowledgements This entry would not have been possible without the help of Julius Michaelis, Max Haslbeck, Stephan-A. Posselt, Lars Noschinski, Manuel Eberl, Gerwin Klein, the Isabelle group Munich, and Georg Carle.