POPL 2024 (series) / CPP 2024 (series) / CPP 2024 /
Memory simulations, security and optimization in a verified compiler
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 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 |