Verified iptables firewall analysis
We present a fully verified firewall ruleset analysis framework. Ultimately, it computes minimal service matrices, i.e. graphs which partition the complete IPv4 address space and visualize the allowed accesses between partitions for a fixed service. Internally, we are working with a simplified firewall model and a core contribution is the translation of complex real world iptables firewall rules into this model. The presented algorithms and translation are formally proven correct with the Isabelle theorem prover. A real world evaluation demonstrates the applicability of our tool. Both the iptables save datasets and the Isabelle formalization are publicly available.
2016 IFIP Networking Conference (IFIP Networking) and Workshops