Version française : voir ici.
I will defend my thesis, entitled "Memory Allocators: Formal Verification and Evaluation", on Friday, December 5th 2025 at 2pm! The defense will take place at the Inria Paris Centre (48 rue Barrault, 75013 Paris), in the Jacques-Louis Lions amphitheatre.
The most up-to-date version of the manuscript is available here.
The jury is composed of:
Software has become pervasive in our lives. Most commonly-used software, including web browsers, instant messaging applications, office suites as well as videoconferencing tools, routinely handles memory to store various contents, such as pictures, music, videos, PDF documents. The memory allocator is the software component providing such user applications with memory. Unfortunately, user applications do not always handle provided memory correctly; in fact, commonly-used software is plagued by a class of security issues closely related to memory management: memory safety issues. To mitigate such issues, it is possible to use hardened memory allocators, that provide memory to applications while mitigating memory safety issues and thus must satisfy heterogeneous goals. In turn, ensuring that these delicate software components are reliable and actually correct is desirable, prompting the use of formal methods, that can be leveraged to increase the trust one can place into software.
In this thesis, we present a methodology to prove hardened memory allocators functionally correct, that we used to develop StarMalloc, a verified, efficient, hardened, and concurrent memory allocator. Using the Steel separation logic framework, we show how to specify and verify a variety of low-level patterns and delicate security mechanisms, by relying on a combination of dependent types, SMT, and modular abstractions to enable efficient, iterative verification.
We produce a verified artifact, in C, that implements the entire API surface of an allocator, and as such works as a drop-in replacement for real-world projects, notably the Firefox browser. We then evaluate StarMalloc and show that it exhibits competitive performance by evaluating it against state-of-the-art memory allocators, and against a variety of real-world projects. Finally, aiming at gaining more understanding about memory allocators behaviors, we developed a hardware-based heap tracing prototype.