Science

Verified Firewall Ruleset Verification

Math, Functional Programming, Theorem Proving, and an Introduction to Isabelle/HOL
Hall G
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 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.

Additional information

Type lecture
Language English

More sessions

12/27/15
Science
greenstadt
Hall 2
What does the fact that Tor users can’t edit wikipedia mean for the quality of the ``encyclopedia that anyone can edit?’’ How do captchas and blocking of anonymity services affect the experiences of Tor users when they are trying to contribute content? This talk will discuss the increasing limitations of active participation in the anonymous Internet and the findings of our interview study of Tor users and wikipedia editors concerning these issues. We believe that by understanding the ...
12/27/15
Science
Hall 6
The REXUS/BEXUS programme allows students from universities and higher education colleges across Europe to carry out scientific and technological experiments on research rockets and balloons. Each year, two rockets and two balloons are launched, carrying up to 20 experiments designed and built by student teams. By reference of two experiments we were involved in, we will explain the way from the experiment idea to the launch and test of it.
12/27/15
Science
Philipp Winter
Hall 1
Several years ago, the Great Firewall of China was silently upgraded to find and block circumvention servers that employ encryption to defeat deep packet inspection. The system is now used to block protocols such as Tor, SoftEther, and SSH. In this talk, we will give an overview of how this system works, and how it can be circumvented.
12/27/15
Science
Peter Buschkamp
Hall 6
Light of astronomical objects gets distorted as it passes earth’s atmosphere. Adaptive optics can correct this distortion and create images that are as sharp as those taken in space. The correction needs a bright reference star. If there is no such star nearby, an artificial Laser Guide Star can be created in the upper atmosphere.
12/28/15
Science
Julia Maria Mönig
Hall G
In my talk I am 1) discussing philosophical concepts of privacy, especially Hannah Arendt's philosophy. I am 2) explaining why in a liberal-democratic system we need to protect our privacy and 3) what we can morally do to prevent catastrophes such as a totalitarian system from happening again. With Hannah Arendt's arguments and her analysis of totalitarian systems in mind, I am referring to three examples from today's privacy discussions: cybermobbing, Behavioral Advertising and secret services.
12/28/15
Science
Nicolas Pouillard
Hall 6
In this presentation I will present the experimental language Ling. We shall get an intuitive understanding of the language through familiar concepts from imperative programming. We shall cover how Ling enables a modular and precise control on memory allocation, through a general optimization called fusion. This optimization, fusion is a cost-free abstraction mechanism which brings high level programming to system programming.
12/28/15
Science
Christian Schaffner
Hall 2
I will entertain the audience with a science talk about quantum cryptography, covering both some classics (Quantum Key Distribution) and the latest developments (position-based quantum cryptography) in this fascinating research field. [No previous knowledge of quantum mechanics is required to follow the talk.]