### 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

BSD License

### Topics

- Computer science/Networks

### 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

### Depends on

- Native Word
- Routing

### Used by

- LOFT — Verified Migration of Linux Firewalls to SDN

## Cite

×

Iptables_Semantics-AFP

    @article{Iptables_Semantics-AFP,
      author  = {Cornelius Diekmann and Lars Hupel},
      title   = {Iptables Semantics},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Iptables_Semantics.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Sep 9, 2016 : Isabelle2016