StarMalloc: Verifying a Modern, Hardened Memory Allocator
summary
StarMalloc is a verified, concurrent, hardened user-space allocator implemented in F/Steel, extracted to C and proven functionally correct relative to a C-standard translation using SMT and custom tactics. It implements the full malloc API, supports configurable security features (guard pages, quarantine, zeroing), and targets real workloads (runs as a drop-in for Firefox, evaluated on Redis, Lean, Z3). The artifact totals ~42,000 lines of verified code with ~6,000 lines of extracted C* and matches performance of 10 state-of-the-art allocators.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:06Why harden allocators
- 2:10StarMalloc contributions
- 3:12Allocator specification example
- 3:53StarMalloc architecture
- 6:23Verification with Steel
- 7:50Data structures in StarMalloc
- 9:55Security mechanisms
- 11:17Abstraction layers
- 12:42Configurability and concurrency
- 13:23Evaluation results
- 14:08Summary
- 14:31Q&A session part one
- 15:36Q&A session part two
- 17:11Q&A session part three
related talks
49mMost Malleable Memory Management Method in C++
01h 11mDynamic Memory Allocation Challenges in C++ Safety Critical Systems
57m“An allocator model for std2”
08mChatGPT, Make a Secure Malloc for me
36mMesh: Automatically Compacting Your C++ Application's Memory
01h 08mHeaps Don’t Lie - Guidelines for Memory Allocation in C++
01h 23mElsewhere Memory (C++20 Abstract Machine) + Virtual Memory
01h 06mmemory-safe C++