POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Tue 16 Jan 2024 17:00 - 17:30 at Kelvin Lecture - Verified Compilation Chair(s): Arthur Charguéraud

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 Jan

Displayed time zone: London change

16:00 - 17:30
Verified CompilationCPP at Kelvin Lecture
Chair(s): Arthur Charguéraud Inria
16:00
30m
Talk
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
30m
Talk
Memory simulations, security and optimization in a verified compiler
CPP
David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag
17:00
30m
Talk
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
CPP