Verified Firewall Ruleset Verification

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

Cornelius Diekmann

Playlists: '32c3' videos starting here / audio / related events

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!


These files contain multiple languages.

This Talk was translated into multiple languages. The files available for download contain all languages as separate audio-tracks. Most desktop video players allow you to choose between them.

Please look for "audio tracks" in your desktop video player.