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

Current compilers implement security features and optimizations that require nontrivial semantic reasoning about pointers and memory allocation: the program after the insertion of the security feature, or after applying the optimization, must simulate the original program despite a different memory layout.

In this article, we illustrate such reasoning on pointer allocations through memory extensions and injections, as well as fine points on undefined calues, by explaining how we implemented and proved correct two security features (stack canaries and pointer authentication) and one optimization (tail recursion elimination) in the CompCert formally verified compiler.

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