Verified Firewall Ruleset Verification - Math, Functional Programming, Theorem Proving, and an Introduction to Isabelle/HOL
32:30 · 32C3: gated communities · 1080p · 2015-12-28
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!