back

Verified Firewall Ruleset Verification

Math, Functional Programming, Theorem Proving, and an Introduction to Isabelle/HOL

If you suspend your transcription on amara.org, please add a timestamp below to indicate how far you progressed! This will help others to resume your work!

Please do not press “publish” on amara.org to save your progress, use “save draft” instead. Only press “publish” when you're done with quality control.

Video duration
00:32:30
Language
English
Abstract
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 <i>arbitrary</i> 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.

Talk ID
7195
Event:
32c3
Day
2
Room
Hall G
Start
5:30 p.m.
Duration
00:30:00
Track
Science
Type of
lecture
Speaker
Lukas Schieren
Talk Slug & media link
32c3-7195-verified_firewall_ruleset_verification
English
0.0% Checking done0.0%
0.0% Syncing done0.0%
0.0% Transcribing done0.0%
100.0% Nothing done yet100.0%
  

Work on this video on Amara!

English: Transcribed until

Last revision: 2 years, 2 months ago