Automated Synthesis of Verified Firewalls
summary
A verified-compiler pipeline turns a high-level firewall DSL (iptables-like history queries and monadic composition) into executable OCaml using Fiat synthesis library and binary encoders from Narcissus, plus Coq proofs tying refinements to implementations. Automated column-reduction proofs are robust; row-reduction proofs are partial. A token-bucket refinement replaces an O(k)-history counter with one token counter and proves at most r·k + b packets pass in k ticks. Extraction targets OCaml; end-to-end performance benchmarks are pending.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:13What does a firewall do?
- 1:09Optimizations
- 1:53Motivation
- 2:48Firewall model
- 3:29Firewall specifications
- 5:00Column reduction
- 7:19Extension to rate limiting
- 8:35Future work
- 10:48Row reduction
related talks
12mAutomated Synthesis of Verified Firewalls
31mPfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagr...
34mFormally verified hardening of C programs against hardware fault injection
21mSecuring Verified IO Programs Against Unverified Code in F*
58mAutomating Relational Verification of Infinite-State Programs
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
20mFoundational Integration Verification of a Cryptographic Server
27mUniversally Composable Security for Program Partitioning