Speaker: Cornelius Diekmann 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 th