PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagr...
summary
A verified compiler for stateless firewall policies compiles a rule list into ordered reduced BDDs, applies BDD restriction to drop infeasible paths, uses an external variable reordering pass, and emits C via code extracted from Coq to OCaml. The compiler proves semantic equivalence between the policy and the generated C (Cil/Clight) and can target assembly via CompCert. Microbenchmarks show BDD-based code outperforms naive rule scanning and scales better with restriction, though it does not beat nftables’ constant-time sets.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:51Binary decision diagrams
- 6:12Filtering policy DSL
- 9:23Frontend compiler steps
- 14:17Backend correctness proof
- 19:44Benchmarking efficiency
- 22:37Conclusion and future work
- 24:05Q&A
related talks
12mAutomated Synthesis of Verified Firewalls- 12mAutomated Synthesis of Verified Firewalls
15mMy Journey in Secure Compilation
15mA Domain-Specific Language for Filtering in Application-Level Gateways
36mThe journey of BPF from restricted C language towards extended and safe C.
19mPanel: Compilation Frameworks
32mDemystifying eBPF - eBPF Firewall from scratch
13mInteractive Bit Vector Reasoning using Verified Bitblasting