Séminaire APR

Memory Allocators: Formal Verification and Evaluation

Mardi 24 février 2026
Antonin Reitz (INRIA)

Commonly-used software is plagued by a class of security issues closely related to memory management called memory safety issues. To mitigate such issues, it is possible to use hardened memory allocators, that implement security mechanisms in addition to providing memory to applications 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 talk, we present a methodology to prove hardened memory allocators functionally correct, that we used to develop StarMalloc: a verified, efficient, hardened, and concurrent C 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, that implements in C the entire API surface of an allocator, and as such works as a drop-in replacement for real-world projects, notably the Firefox browser. Moreover, we show that StarMalloc exhibits competitive performance by evaluating it against state-of-the-art memory allocators on the mimalloc-bench benchmarking suite, which includes realistic workloads.