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.
License
Topics
Session Iptables_Semantics
- List_Misc
- Negation_Type
- WordInterval_Lists
- Repeat_Stabilize
- Firewall_Common
- Semantics
- Matching
- Ruleset_Update
- Call_Return_Unfolding
- Ternary
- Matching_Ternary
- Semantics_Ternary
- Datatype_Selectors
- IpAddresses
- L4_Protocol_Flags
- Ports
- Conntrack_State
- Tagged_Packet
- Common_Primitive_Syntax
- Unknown_Match_Tacs
- Common_Primitive_Matcher_Generic
- Common_Primitive_Matcher
- Example_Semantics
- Alternative_Semantics
- Semantics_Stateful
- Semantics_Goto
- Negation_Type_DNF
- Matching_Embeddings
- Fixed_Action
- Normalized_Matches
- Negation_Type_Matching
- Primitive_Normalization
- MatchExpr_Fold
- Common_Primitive_Lemmas
- Ports_Normalize
- IpAddresses_Normalize
- Interfaces_Normalize
- Word_Upto
- Protocols_Normalize
- Remdups_Rev
- Ipassmt
- No_Spoof
- Common_Primitive_toString
- Routing_IpAssmt
- Output_Interface_Replace
- Interface_Replace
- Optimizing
- Transform
- Conntrack_State_Transform
- Primitive_Abstract
- SimpleFw_Compliance
- Semantics_Embeddings
- Iptables_Semantics
- Code_Interface
- Parser6
- No_Spoof_Embeddings
- Parser
- Code_haskell
- Access_Matrix_Embeddings
- Documentation
Session Iptables_Semantics_Examples
- Parser_Test
- Parser6_Test
- Small_Examples
- Ports_Fail
- Contrived_Example
- iptables_Ln_tuned_parsed
- Analyze_Synology_Diskstation
- Analyze_Ringofsaturn_com
- Analyze_SQRL_Shorewall
- SQRL_2015_nospoof
- SNS_IAS_Eduroam_Spoofing
- Analyze_medium_sized_company
Session Iptables_Semantics_Examples_Big
- Analyze_topos_generated
- IP_Address_Space_Examples_All_Small
- Analyze_TUM_Net_Firewall
- Analyze_Containern
- TUM_Spoofing_new3
- TUM_Simple_FW
- IP_Address_Space_Examples_All_Large