POPL 2024 (series) / CPP 2024 (series) / CPP 2024 /
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
We present a verified compiler for stateless firewall policies. The policy is first compiled into an intermediate representation taking the form of a binary decision diagram that is optimised in terms of decision nodes. The decision diagram is then compiled into a Clight program. The compiler is proved correct using the Coq proof assistant and extracted into OCaml code. Our preliminary experiments show promising results. The compiler generates code for relatively large firewall policies and the generated code outperforms a sequential evaluation of the policy rules.
Tue 16 JanDisplayed time zone: London change
Tue 16 Jan
Displayed time zone: London change
16:00 - 17:30 | |||
16:00 30mTalk | Lean Formalization of Extended Regular Expression Matching with Lookarounds CPP Ekaterina Zhuchko Tallinn University of Technology, Margus Veanes Microsoft Research, Gabriel Ebner Microsoft Research | ||
16:30 30mTalk | Memory simulations, security and optimization in a verified compiler CPP David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag | ||
17:00 30mTalk | PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams CPP |