In this work, we present StarMalloc, a verified, security-oriented, concurrent memory allocator that can be used as a drop-in replacement in real-world projects. Using the Steel separation logic framework, we show how to specify and verify StarMalloc, relying on dependent types and modular abstractions to enable efficient verification. As part of StarMalloc, we also develop several generic datastructures and proof libraries directly reusable in future systems verification projects. We finally show that StarMalloc can be used with real-world projects, including the Firefox browser, and evaluate it against 10 state-of-the-art memory allocators, demonstrating its competitiveness.

翻译：本文提出 StarMalloc，一款经过验证的安全导向并发内存分配器，可作为即插即用替代方案应用于实际项目。我们借助 Steel 分离逻辑框架，展示了如何通过依赖类型与模块化抽象来规范并验证 StarMalloc，从而实现高效验证。作为 StarMalloc 的组成部分，我们还开发了多个通用数据结构与证明库，可直接复用于未来的系统验证项目。最后，我们证明 StarMalloc 可应用于包括 Firefox 浏览器在内的实际项目，并通过与 10 款主流内存分配器的对比评估，展示了其竞争力。