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},
}
|