Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Simple Firewall


view this post on Zulip Email Gateway (Aug 22 2022 at 14:02):

From: Tobias Nipkow <nipkow@in.tum.de>
Simple Firewall
Cornelius Diekmann, Julius Michaelis and Max Haslbeck

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.

https://www.isa-afp.org/entries/Simple_Firewall.shtml

Enjoy!
smime.p7s


Last updated: Apr 30 2024 at 04:19 UTC