### Abstract

We present a simple model of a firewall. The firewall can accept or drop a packet and can match on interfaces, IP addresses, protocol, and ports. It was designed to feature nice mathematical properties: The type of match expressions was carefully crafted such that the conjunction of two match expressions is only one match expression. This model is too simplistic to mirror all aspects of the real world. In the upcoming entry "Iptables Semantics", we will translate the Linux firewall iptables to this model. For a fixed service (e.g. ssh, http), we provide an algorithm to compute an overview of the firewall's filtering behavior. The algorithm computes minimal service matrices, i.e. graphs which partition the complete IPv4 and IPv6 address space and visualize the allowed accesses between partitions. For a detailed description, see Verified iptables Firewall Analysis, IFIP Networking 2016.

### License

BSD License

### Topics

- Computer science/Networks

### Session Simple_Firewall

- Lib_Enum_toString
- L4_Protocol
- Simple_Packet
- Firewall_Common_Decision_State
- Iface
- SimpleFw_Syntax
- SimpleFw_Semantics
- List_Product_More
- Option_Helpers
- Generic_SimpleFw
- Shadowed
- IP_Partition_Preliminaries
- GroupF
- IP_Addr_WordInterval_toString
- Primitives_toString
- Service_Matrix
- SimpleFw_toString

### Depends on

- IP Addresses

### Used by

- Routing

### Auto-related entries

- Monadification, Memoization and Dynamic Programming
- Verification of the UpDown Scheme
- Information Flow Noninterference via Slicing
- Inter-Procedural Information Flow Noninterference via Slicing

## Cite

×

Simple_Firewall-AFP

    @article{Simple_Firewall-AFP,
      author  = {Cornelius Diekmann and Julius Michaelis and Max W. Haslbeck},
      title   = {Simple Firewall},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Simple_Firewall.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 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Aug 24, 2016 : Isabelle2016