Memory Simulations, Security and Optimization in a Verified Compiler
arXiv:2312.08117 · doi:10.1145/3636501.3636952
Abstract
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 values, 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.
Certified Programs and Proofs 2024, Jan 2024, London, United Kingdom, France