一句话：用 Steel 分离逻辑验证一个并发、安全加固的内存分配器，可作为 Firefox 等真实项目的即插即用替代。
内存分配器是系统底层的关键组件，同时承载诸多精巧的安全加固机制，这使其正确性验证十分困难。本文提出 StarMalloc：一个经过验证、高效、面向安全且支持并发的内存分配器。作者基于 Steel 分离逻辑框架，结合依赖类型、SMT 求解与模块化抽象，为大量底层编程模式与微妙的安全机制给出规约并完成验证，从而在保证验证效率的同时覆盖真实实现。其成果是一份用 C 编写的已验证工件，实现了分配器的完整 API，可直接替换现实项目（如 Firefox 浏览器）中的分配器。作为副产品，工作还提供了若干可复用的通用数据结构与证明库，并扩展了 Steel 工具链以表达此前无法描述的底层惯用法。评估方面，作者将 StarMalloc 与 10 个最先进的分配器进行性能对比，并在 Redis、Lean 编译器、Z3 SMT 求解器等多个真实项目上进行了测试，显示出有竞争力的性能。
We present StarMalloc, a verified, efficient, security-oriented, and concurrent memory allocator. Using the Steel separation logic framework, we show how to specify and verify a multitude of low-level patterns and delicate security mechanisms, by relying on a combination of dependent types, SMT, and modular abstractions to enable efficient 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. As part of StarMalloc, we develop several generic datastructures and proof libraries directly reusable in future systems verification projects. We also extend the Steel toolchain to express several low-level idioms that were previously missing. Finally, we show that StarMalloc exhibits competitive performance by evaluating it against 10 state-of-the-art memory allocators, and against a variety of real-world projects, such as Redis, the Lean compiler, and the Z3 SMT solver.
@article{ReitzFP24,
title = {StarMalloc: Verifying a Modern, Hardened Memory Allocator},
author = {Antonin Reitz and Aymeric Fromherz and Jonathan Protzenko},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689773}
}