[isabelle] new in the AFP: Iptables_Semantics



Iâm happy to announce a substantial new entry by Cornelius Diekmann and Lars Hupel:

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

https://www.isa-afp.org/entries/Iptables_Semantics.shtml

There is a separate session of examples, which apparently take several hours to run!

Larry Paulson






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.