Precise and Efficient Memory Analysis of Low-level Languages
Wednesday 17 December 2025 at 14h00
ENS Paris-Saclay, Room 1Z61 and online
Abstract: Memory safety is crucial for systems like embedded software and operating systems, where errors such as buffer overflows or use-after-free can lead to serious security issues. This thesis presents a sound, automated, and practical static analysis to prove spatial memory safety in binary code or C programs. The method builds on a novel dependent type system called TypedC which extends C's types to express complex memory properties. It works without modifying source code and uses abstract interpretation to check types and ensure spatial memory safety. A second contribution is a new framework for building relational compositional abstract domains called AADT. It enables precise analysis of complex data types like arrays, structs, and unions. The approach is implemented in the Codex platform and tested on real-world low-level code, showing strong results in verifying memory safety. The defense will be in English.
Jury:
- Antoine Miné, Professor at Sorbonne University (Reviewer)
- Thomas Jensen, Research Director at INRIA (Reviewer)
- Isabella Mastroeni, Associate Professor at the Università degli Studi di Verona (Examiner)
- Xavier Rival, Research Director at INRIA (Examiner)
- Tomáš Vojnar, Professor at Masaryk University (Examiner)
- Mihaela Sighireanu, Professor at ENS Paris-Saclay (co-advisor)
- Matthieu Lemerre, Research Director at CEA (co-advisor)