The predominant firewall of Linux is iptables. An evaluation of our work on a large set of real-world firewall rulesets shows that our framework provides interesting results in many situations, and can both help and out-compete other static analysis frameworks found in related work. Based on that, we implement the verified generation of IP space partitions and minimal service matrices. We provide and verify procedures that translate from the complex iptables language into this simple model. For analysis purposes, we describe a simplified model of firewalls that only supports a single list of rules with limited expressiveness. Around that, we organize a set of simplification procedures and their correctness proofs: we include procedures that can unfold calls to user-defined chains, simplify match expressions, and construct approximations removing unknown or unwanted match expressions. This semantics is tailored to the specifics of the filter table and supports arbitrary match expressions, even new ones that may be added in the future. We build our work around a formal semantics of the behavior of iptables firewalls. This article summarizes our efforts around the formally verified static analysis of iptables rulesets using Isabelle/HOL.
0 kommentar(er)
