PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams

Explore a conference talk presenting PfComp, a verified compiler for stateless firewall policies that leverages binary decision diagrams. Discover how the compiler optimizes policies into an intermediate representation before generating efficient program code. Learn about the compiler's proof of correctness using the Coq proof assistant and its extraction into OCaml code. Gain insights into the promising experimental results, showcasing the compiler's ability to handle large firewall policies and generate code that outperforms sequential rule evaluation. Delve into the innovative approach of using binary decision diagrams for packet filtering and the implications for network security and performance.