We develop a tool to verify Linux netfilter/iptables firewalls rulesets. Then, we verify the verification tool itself. Warning: involves math! This talk is also an introduction to interactive theorem proving and programming in Isabelle/HOL. We strongly suggest that audience members have some familiarity with functional programming. A strong mathematical background is NOT required. TL;DR: Math is cool again, we now have the tools for "executable math". Also: iptables!
We all know that writing large firewall rulesets can be hard. One huge problem. Let's write a tool to statically verify some properties of our rulesets! Now we have three huge problems: (1) writing flawless firewall rulesets. (2) making sure that our verification tool does the right thing. (3) making sure that the internal firewall model of our tool corresponds to the real world. In this talk, we will solve these problems from front to back. We focus on problems (2) and (3). Warning: this talk involves math! First, we need to specify the behavior of the Linux netfilter/iptables firewall. In order to be convincing, this model must be small and simple. It should fit on one slide. However, firewalls can be quite complex and the model must cope with this. For example, looking at `man iptables-extensions`, we see numerous match conditions. But nobody required that our model must be executable code; we will specify the model mathematically. For example, this allows to define arbitrary match conditions. Technically speaking, we define the filtering behavior of iptables in terms of bigstep semantics. Mathematical specifications can be very powerful, in particular when we get to the point where the specification is not directly "executable". Enough math, let's write some executable code to do something with our ruleset. For example, unfolding the jumps to user-defined chains, checking that some packets will be certainly blocked, or checking that we got the spoofing protection right. Second, based on our firewall model, we can now prove that our algorithms do the right thing. In contrast to testing, a mathematical proof allows assertions for all possible values. For example: For all possible packets, rulesets, and firewall-matching-features, our unfolding algorithm does not change the filtering behavior of the firewall. Yes, we can even show that our tool will still be correct, even if the netfilter team pushes a new matching feature. Finally, we now have a verified verification tool. We can use it to verify our firewall ruleset and finally sleep well at night again. We developed an iptables verification library over the last few years in Isabelle/HOL. Isabelle can export executable definitions (i.e. our algorithms) to functional languages such as Haskell, Scala, SML, or OCcaml. Writing the input/output functions manually in Haskell, we have a fast and stand-alone tool. This talk is also an introduction to interactive theorem proving and programming in Isabelle/HOL. We strongly suggest that audience members have some familiarity with functional programming. A strong mathematical background is not required.
Speakers: Cornelius Diekmann