  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.
