Automated Synthesis of Verified Firewalls
summary
Claim of correct-by-construction, stateful TCP/IP packet filters implemented as a verified compiler in Coq using the Fiat refinement framework and the Narcissus binary-format library. A DSL models iptables-like predicates; column-projection refinement is fully automated and proven, row-reduction heuristics have partial proofs, and a token bucket refinement replaces full-history counters with a single-token counter (proofs in progress). Extraction goes to OCaml; runtime performance testing is pending, and some optimizations propagate information down to packet parsing.
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
15mA Domain-Specific Language for Filtering in Application-Level Gateways
15mAutomated Verification of Network Function Binaries
58mAutomating Relational Verification of Infinite-State Programs
23mApplying Formal Verification to Microkernel IPC at Meta
30mVerifying Reliable Network Components in a Distributed Separation Logic with Dep...