|
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.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Automatic_Refinement, IP_Addresses, Native_Word, Routing, Simple_Firewall, Word_Lib |
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.
|
|