Verified iptables firewall analysis
Cornelius Diekmann, Julius Michaelis, Maximilian P. L. Haslbeck, Georg Carle · 2016
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.