Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator

Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko

TL;DR

StarMalloc tackles memory-safety risks in low-level software by delivering a formally verified, security-oriented, concurrent memory allocator that can replace standard malloc. It develops a Steel-based specification in F* with dependent types and modular abstractions, then extracts a complete, drop-in C implementation, and demonstrates practicality through Firefox integration and benchmarking against 10 allocators. The work provides extensive verification libraries and shows competitive performance with strong security properties, highlighting a path toward verifiable, production-grade system components. This work has practical impact by enabling deployment-ready, formally verified memory management in real-world software stacks.

Abstract

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: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator

TL;DR

StarMalloc tackles memory-safety risks in low-level software by delivering a formally verified, security-oriented, concurrent memory allocator that can replace standard malloc. It develops a Steel-based specification in F* with dependent types and modular abstractions, then extracts a complete, drop-in C implementation, and demonstrates practicality through Firefox integration and benchmarking against 10 allocators. The work provides extensive verification libraries and shows competitive performance with strong security properties, highlighting a path toward verifiable, production-grade system components. This work has practical impact by enabling deployment-ready, formally verified memory management in real-world software stacks.

Abstract

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.
Paper Structure (19 sections, 1 figure, 4 tables)

This paper contains 19 sections, 1 figure, 4 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Toward Secure Memory Allocators
  4. Verified Memory Allocators
  5. Design and Overview of StarMalloc
  6. System Architecture
  7. Allocator Hardening
  8. Modeling the Essence of a Security-Oriented Allocator
  9. Background
  10. Specifying the Allocator Architecture
  11. Specification of Security Mechanisms
  12. Implementing, Verifying, Extracting to C
  13. Evaluation
  14. Performance Evaluation
  15. Security Evaluation
  16. ...and 4 more sections

Figures (1)

  • Figure 1: Architecture of StarMalloc. All regular allocations live in a single 'd memory region (left). All metadata lives in a single distinct 'd memory region (right). All allocations are contiguous. All metadata is contiguous. Accessing the n-th slab of the m-th size class thus boils down to pointer arithmetic, and similarly for the metadata. We rely on virtual memory to ensure only in-use pages occupy memory. Only a single arena is shown for conciseness; other arenas and their metadata are laid out contiguously in the same two 'd regions.