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, as well as the correctness of rulesets has been proven with the help of our tool. For a detailed description, see:

- C. Diekmann, L. Hupel, and G. Carle, Semantics-Preserving Simplification of Real-World Firewall Rule Sets. In 20th International Symposium on Formal Methods, 2015. [pdf]
- C. Diekmann, L. Schwaighofer, and G. Carle, Certifying Spoofing-Protection of Firewalls. In 11th International Conference on Network and Service Management, 2015. [pdf]
- C. Diekmann, J. Michaelis, M. Haslbeck, and G. Carle, Verified iptables Firewall Analysis. In IFIP Networking, 2016. [pdf]
- C. Diekmann, Verified Firewall Ruleset Verification – Math, Functional Programming, Theorem Proving, and an Introduction to Isabelle/HOL. In 32. Chaos Communication Congress (32C3), 2015. [recording]