# StarMalloc: Verifying a Modern, Hardened Memory
## Allocator

Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko

<figure><img src="image_1.png" /></figure>

To cite this version:

Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko. StarMalloc: Verifying a Modern, Hardened Memory Allocator. Proceedings of the ACM on Programming Languages, 2024, 8 (OOPSLA2), pp.1757 - 1786. 10.1145/3689773. hal-04837244

HAL Id: hal-04837244

https://hal.science/hal-04837244v1

Submitted on 13 Dec 2024

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# StarMalloc: Verifying a Modern, Hardened Memory Allocator

ANTONIN REITZ, Inria, France

AYMERIC FROMHERZ, Inria, France

JONATHAN PROTZENKO, Microsoft Azure Research, USA

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.

**CCS Concepts:** • **Theory of computation** → **Separation logic**; • **Security and privacy** → **Logic and verification**.

Additional Key Words and Phrases: Formal Verification, Separation Logic, Memory Allocators

## ACM Reference Format:

Antonin Reitz, Aymeric Fromherz, and Jonathan Protzenko. 2024. StarMalloc: Verifying a Modern, Hardened Memory Allocator. *Proc. ACM Program. Lang.* 8, OOPSLA2, Article 333 (October 2024), 30 pages. https://doi.org/10.1145/3689773

## 1 Introduction

In recent years, memory-safe languages such as Rust and Go have significantly risen in popularity and adoption, and to this date remain some of the fastest-growing languages [GitHub Team 2023]. However, for safety-critical, low-level applications, C and C++ remain the languages of choice, owing to their ability to interact with the operating system and the memory in extremely low-level ways. While C and C++ allow developers to achieve high performance, particularly in resource-constrained environments, C and C++ are also fundamentally memory-unsafe, meaning they empower developers to “shoot themselves in the foot” with great ease, resulting in a wide range of attacks due to memory corruption bugs [Szekeres et al. 2013]. Indeed, recent studies by Google [Chromium Project 2020] and Microsoft [MSRC Team 2019] estimate that memory-related errors, e.g., buffer overflows or dangling pointers, are the root cause of 70% of the security vulnerabilities in widely deployed software.

As argued by Berger [2012], “the software industry is in a position similar to that of the automobile industry of the 1950s, delivering software with lots of horsepower and tailfins but no safety measures of any kind”. To mitigate the impact of incorrect memory management in low-level programs, Berger therefore advocates for the addition of “seatbelts and airbags”, in particular through the

Authors' Contact Information: Antonin Reitz, Inria, Paris, France, antonin.reitz@inria.fr; Aymeric Fromherz, Inria, Paris, France, aymeric.fromherz@inria.fr; Jonathan Protzenko, Microsoft Azure Research, Redmond, USA, protz@microsoft.com.
development of *hardened* memory allocators. Modern, hardened memory allocators [Berger and Zorn 2006; GrapheneOS Development Team 2021; Leijen et al. 2019; LLVM Project 2023; Novark and Berger 2010; Silvestro et al. 2017, 2018] thus include mitigations against common heap vulnerabilities, for instance by randomizing the placement of allocations, or by separating heap metadata from the heap itself. The net effect is that attacks are harder to conduct, and the allocator thus successfully provides some degree of protection against incorrect programs.

Unfortunately, hardening allocators increases the complexity of an already subtle piece of software. Allocators are expected to fulfill numerous goals [Wilson et al. 1995], e.g., high performance, low memory consumption, maximizing concurrency, minimizing heap contention, and so on. Meeting these goals requires custom data structures and low-level pointer and bit manipulations, and typically entails bugs, which can even be found in widely used allocators such as glibc's [glibc 2017a,b, 2020; HFT guy 2020; MSRC Team 2021; MySQL 2019; Portal 2013; Sautereau 2021].

To increase the confidence in a critical component of the software ecosystem, we investigate the formal verification of a modern, hardened memory allocator. The verification of a modern allocator raises several technical challenges common to other low-level, systems verification projects e.g., the need for highly efficient datastructures, requiring bitwise operations and fine-grained memory control or support for concurrency to achieve thread-safety between clients of the allocator. We set an additional goal for ourselves: we want our verification methodology to be modular, and support a *living* artifact where changes can be performed iteratively, and where development can proceed while minimizing changes to the proofs. We aim to do so because it is frequent that one data structure should be replaced by an optimized variant; or that a novel hardening mechanism should be added when a new attack is discovered.

To achieve this goal, we rely on the combination of three components: concurrent separation logic, dependent types, and SMT solvers. Separation logic [Ishtiaq and O'Hearn 2001; O'Hearn et al. 2001; Reynolds 2002] provides a logical framework to efficiently and modularly reason about heap manipulating programs; dependent types enable us to define higher-order, parametric abstractions and combinators; SMT solvers enable automated reasoning about program-related theories (e.g., arithmetic or sequences). Supporting these three features, the Steel framework [Fromherz et al. 2021; Swamy et al. 2020] forms the basis of our work: compared to other state-of-the-art separation logic frameworks such as Iris [Jung et al. 2018, 2015; Krebbers et al. 2017], Steel explicitly targets program verification and provides extraction facilities to executable, verified C code.

Fromherz et al. [2021] showed how to use the Steel framework to separate verification conditions between separation logic terms and first-order logic queries amenable to automated SMT verification. In this paper, we show how to scale up the Steel verification methodology to systems programming. We design dependently-typed, higher-order, generic combinators and abstractions which enable us to modularly reason about different components of the allocator, minimizing the impact of code changes on proofs and simplifying iterative verified programming. Along with several extensions of Steel and its core libraries, this leads us to the verification of the safety and correctness of StarMalloc, the first verified, concurrent, hardened, userspace memory allocator usable as a drop-in replacement for real-world programs, and one order of magnitude larger than other verified allocators. While our verification effort includes the implementation of several hardening mechanisms, our verification guarantees solely include their memory safety and correctness. In particular, establishing theorems about the security of StarMalloc is out of scope; we instead leverage the extensive literature on allocator design to motivate their usefulness.

The rest of this paper is as follows. We present the design of StarMalloc, inherited from hardened_malloc [GrapheneOS Development Team 2021], a modern, security-oriented allocator, and emphasize the verification challenges it entails (Section 2). We illustrate our methodology through the verification of a core datastructure in StarMalloc: doubly-linked lists residing in a fixed-size
<figure><img src="image_3.png" /><figcaption>Fig. 1. Architecture of StarMalloc. All regular allocations live in a single mmap'd memory region (left). All metadata lives in a single distinct mmap'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 reserved, but uncommitted 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 mmap'd regions.</figcaption></figure>

array, demonstrating how the combination of dependent types, higher-order separation logic combinators, and SMT solving simplifies iterative extensions to our verified implementation (Section 3). We describe extensions to our toolchain, including support for POSIX locks, const arrays, and `size_t` and `ptrdiff_t` integers, which enabled verified, concurrent systems programming in Steel (Section 4). Leveraging our methodology, we present StarMalloc, a verified, hardened memory allocator resulting in 6,000 lines of C code, while also contributing several reusable proof and datastructure Steel libraries (Section 5). We evaluate the performance of StarMalloc against other state-of-the-art allocators on allocator-specific benchmarks, as well as on the Mozilla Firefox browser, demonstrating its competitiveness (Section 6).

## 2 StarMalloc's Architecture

We start this paper with an overview of StarMalloc's architecture. This design is entirely inherited from `hardened_malloc` [GrapheneOS Development Team 2021], a modern, security-oriented memory allocator heavily based on the OpenBSD design, and is therefore not a contribution of this paper. Our choice of `hardened_malloc` as a baseline stems from several reasons: its advanced design and hardening features raise verification challenges representative of modern allocators, and its emphasis on security makes formally ruling out implementation bugs even more attractive than for other allocators. The design choices especially aim for low fragmentation, low contention, security by default, and good long-term performance and scalability. While the high-level architectures are identical, StarMalloc's implementation differs however from `hardened_malloc` in several small ways; we develop on this in Section 5. We take advantage of this section to introduce several verification challenges in userspace memory allocators, which we tackle in our work.

### 2.1 System Architecture

Figure 1 describes the overall architecture of StarMalloc. We proceed top-down, and describe the sequence of steps taken in order to fulfill a memory allocation request.

**AVL tree for large allocations.** If the allocation exceeds the page size (4kB), it is deemed a "large allocation". Large allocations are tracked in an auxiliary map, implemented using an AVL tree (not shown in Figure 1). Large allocations are directly forwarded to the OS (via mmap); once the syscall returns, StarMalloc receives a fresh address of the desired size; inserts a new entry into the AVL
tree that maps the fresh address to its size; and returns the fresh address to the client. (We explain in the free paragraph, below, why keeping track of the large allocation size is important.)

**Memory-mapped region for regular allocations.** If the allocation is equal to, or smaller than the page size (4kB), it is a regular allocation. Relying on modern OSes and their treatment of virtual memory, we perform a single call to mmap at allocator initialization time, which reserves a region of virtual memory for *all* regular allocations. At the beginning, none of the corresponding pages are used; unless the client program allocates substantial amounts of memory, the virtual memory manager guarantees that the actual memory usage will be correspondingly low. Throughout StarMalloc, we take care to return unused pages to the OS to be used for other purposes, but retain the virtual address space which remains unchanged throughout the execution of the program, preserving invariants relating the metadata to the memory layout.

***Challenge: Interaction with the OS.*** Both the handling of large and regular allocations rely on syscalls, in particular, mmap. Therefore, a formal, precise model of the behavior of used OS primitives is required to apply formal verification to a memory allocator (Section 5.2).

**Arenas.** The large memory region for regular allocations is first subdivided into *arenas*. The goal is to spread concurrent allocations from multiple threads onto distinct arenas, to avoid contention. The number of arenas is set at compile time; using thread-local storage, we associate an arena to each thread (e.g., `thread_id % n_arenas`). When a thread requests memory, the allocator looks up its associated arena then allocates there. Threads can however access and free memory located in a different arena, the main point of arenas is to spread out allocations in order to statically reduce contention. Arenas are *not* protected by locks, which operate at a smaller level of granularity.

***Challenge: Concurrency.*** Modern allocators commonly operate in highly parallel environments, where different threads may request and free memory concurrently. To ensure thread-safety, this allocator design relies on locks, which require both an efficient implementation and a (standard) separation logic model (Section 4.1).

**Size classes.** Each arena is further subdivided into size classes, which contain allocations of a given size; each regular allocation is rounded up to the nearest available size class. Just like the number of arenas, the number of size classes is statically fixed: in the default version of StarMalloc, there are 27 size classes for different multiples of 16 bytes up to the page size.

Thanks to virtual memory, only the portions of each size class that are in use are backed by physical memory. Each size class is associated to metadata that needs to be updated whenever an allocation takes place within that size class: for that reason, size classes are each protected by an individual lock. Recall that the mapping of threads to arenas is not injective (the number of arenas is fixed): the lock thus prevents two threads from racing to allocate within the same size class.

***Challenge: Configurability.*** Different usecases might require diverse arena and size class configurations. For instance, sequential settings only require one arena, while ARM systems handling 64kB large pages can efficiently use a wider range of size classes compared to systems with 4kB pages. The allocator's architecture must therefore be easily configurable at compile time (Section 3.5).

**Slabs.** Each size class is made up of slabs. A slab is exactly one page, divided into allocation units, called slots. All slabs within a size class are divided into the same slot size. That is, within the 4kB size class, each slab contains one slot; and within the 32B size class, each slab contains 128 slots.

Each size class tracks all of its slabs using *size class metadata*. The metadata keeps track of free slabs, and to reduce memory fragmentation, it also separately tracks partially filled slabs, which are prioritized for allocation. The tracking of all three kinds of slabs is achieved using doubly-linked lists to efficiently insert/remove when implementing malloc/free. The metadata also contains two
additional lists related to hardening mechanisms (detailed in Section 2.2). (In practice, our lists have a special marker for the last used slab, so as not to initially contain, e.g., 1M elements for the list of free slabs.) To fulfill an allocation request, the allocator acquires the lock for that size class, looks for a partial or free slab (i.e., one where there is space left) in the metadata, then proceeds.

**Slots.** Each slab is made up of individual slots. The design of StarMalloc ensures that each individual allocation is aligned to at least 16 bytes, a safe overapproximation of what some older ABIs (e.g., Linux x86) permitted. To keep track of which slots are used or available within a given slab, StarMalloc maintains *slab metadata*; in practice, this is a bitmap. We eschew free lists, because we cannot guarantee that an attacker will be unable to corrupt them in the presence of buffer overflows. Conversely, our bitmaps live in a separate mmap'd region, which makes it harder for an attacker to guess the metadata virtual address. This is the final step for the allocator: once a suitable slab is identified, a slot is taken within that slab, the *slab metadata* is updated, the size class lock is released, and the address of the corresponding slot is returned to the client program.

**Challenge: Non-Local Reasoning.** The main invariant of a memory allocator is that its metadata is coherent with respect to the memory available, that is, the memory it still owns. We therefore require predicates to model slot ownership or that a slab is partially filled, and establish invariants with respect to metadata values stored in a different memory region (Section 3.2).

**Challenge: Efficient Datastructures.** During its execution, an allocator mostly reads and modifies metadata. To be performant, it therefore needs to rely on efficient datastructures for storing metadata such as doubly-linked lists or bitmaps, that require fine-grained reasoning to establish their correctness (Section 3.2).

**Freeing.** In order to free, the allocator first performs pointer comparisons to determine whether the pointer belongs to the mmap'd region of regular allocations. If so, further pointer difference operations and bit manipulations allow determining the arena and size class that the pointer belongs to. StarMalloc then acquires the relevant lock, locates the suitable slab, updates the bitmap (slab metadata), size class metadata, then releases the lock. If this leads to a new empty slab, the corresponding slab is moved to quarantine (more on quarantine below), and returned back to the OS. Should the pointer be invalid (i.e., not correspond to a slot), the allocator leaves the bitmap unchanged and releases the lock. If the pointer belongs to none of the allocator's arenas, then the pointer must be a large allocation. A lookup in the AVL map allows: i) ensuring that the pointer is indeed valid, and ii) retrieving its size. This allows StarMalloc to call munmap, which given a pointer and its size, releases the corresponding pages back to the OS.

## 2.2 Allocator Hardening

Our design not only incorporates all of the mechanisms described above, but adds extra mechanisms in order to defend against heap corruption vulnerabilities. This highlights the need for verification: the design above is non-trivial with many subtle invariants, and becomes even more so once the security mechanisms are added. Many hardening techniques continue to be proposed. We adopt the most widely-implemented ones [Yun et al. 2021], suggesting their importance and effectiveness. We now review the main security mechanisms StarMalloc implements.

**Segregated metadata.** As mentioned above, our metadata lives in a separate address space (i.e., an mmap'd region that is disjoint from the regular allocation region). If an attacker manages to write past a given slot, the damage is limited since the allocator's internal data structures are untouched.

**Zeroing.** Just like Apple's OSX allocator [Apple Security Research 2022], we zero-out memory upon freeing. We do this either using a cryptographic-grade secure zeroing function (regular allocations)
which is resistant to aggressive C compiler optimizations, or munmap (large allocations). This
defends against an attacker observing sensitive data through a reused memory allocation slot.
Furthermore, upon allocation, we verify that the memory is still zeroed out. If not, the memory
was corrupted, and we return NULL as a further defensive security measure.

**Quarantine.** Once a slab becomes empty, we do not reuse it immediately and instead keep it in quarantine. This is implemented using a fourth linked list within a given size class, which keeps track of quarantined slabs. Unlike the other linked lists (full, empty, partial), the quarantine list exposes a *queue* interface. The idea is to let the slab “cool off” to make any subsequent accesses to any pointer in it an OS page fault error. This defends against double frees, and generally accessing freed memory. Using a queue allows us to reclaim pages from quarantine in a first-in, first-out order, relying on customizable compile-time parameters to specify what is a sufficiently long time before a quarantined page becomes reusable.

**Guard pages.** Within size classes, some of the slabs, called guard pages, are marked as inaccessible via mmap, meaning that any access to them causes a fault. They are tracked in the final, fifth linked list. This prevents against large buffer overruns linearly reading past an allocation unit.

**Canaries.** Each slot is terminated by a canary, consisting of a magic number, which can absorb small buffer overflows instead of corrupting the next slot. We check the integrity of a canary when freeing a slot, which can detect overflows *a posteriori* (but often too late to entirely prevent attacks).

*Challenge: Iterating on Verified Implementations.* Security mechanisms such as those presented in this section are commonly added once the basic functionalities of an allocator are implemented. Furthermore, newly discovered attacks often lead to the design of novel hardening techniques, that must be integrated in existing allocators. We therefore need a verification methodology that is robust to iterations, and minimizes the proof effort required to update implementations (Section 3.3).

## 3 Iterative Verified Programming through SMT and Dependent Types

We now set our sights on verifying an implementation of the design previously presented. Beyond challenges inherent to the outlined architecture, our chief goal is to design a verification methodology that allows easily updating and extending the allocator implementation, while reducing the overhead of adapting the proofs. The natural first step, well-known to formal verification practitioners, is to rely on modular abstractions which separate different parts of the proof and code; in type-theory based proof assistants, this is commonly done through dependent types and higher-order predicates. However, despite recent advances in proof repair [Gopinathan et al. 2023; Ringer et al. 2019, 2018], adapting such proofs when modifying code remains challenging. On the other end of the spectrum, SMT solvers can automatically discharge verification conditions, and can thus simplify proof repair when reverifying a modified program or specification. Unfortunately, verification tools based on SMT solvers commonly suffer from proof instability, which requires controlled proof contexts and isolated verification conditions to be tamed [Zhou et al. 2023].

We now leverage Steel's design, and notably its separation of spatial proofs, which are tactic-
driven, and pure functional predicates, which are SMT-driven. With this foundation, we design
modular abstractions based on dependent types and higher-order separation logic and targeted
towards an efficient interoperation with automated SMT solvers. Doing so, we aim to show how
to scale low-level systems verification up to several thousand lines of code, while avoiding the
pitfalls and limitations of either fully manual or fully automated theorem proving. We start with a
brief presentation of Steel before showing our methodology on one of the most complex bits of
StarMalloc: doubly-linked lists within a static array, each with its own invariant on its values.
## 3.1 Background

**Concurrent Separation Logic.** Separation logic [Ishtiaq and O'Hearn 2001; O'Hearn et al. 2001; Reynolds 2002] is a Hoare-style program logic that is well-suited to reasoning about heap-manipulating programs: the Hoare triple {$P$} {$c$} {$Q$} represents that, if precondition $P$ is initially satisfied, then the program $c$ executes without error, that is, the program is memory safe, and the post-condition $Q$ is satisfied when $c$ terminates, which can be used to specify the functional correctness of the program. As an example, the specification of memory allocation is {$emp$} {$r = alloc(v)$} {$r \mapsto v$}, where $emp$ corresponds to the empty predicate, always trivially true, while $r \mapsto v$ represents that $r$ is live and points to the value $v$. Separation logic predicates can be composed: $P * Q$ represents that $P$ and $Q$ relate to separated (i.e., disjoint) regions of memory. This enables modular reasoning through the separation logic frame rule: if {$P$} {$c$} {$Q$} holds, then so does {$P * R$} {$c$} {$Q * R$}; any predicate $R$ relating to a part of memory separated from the execution of $c$ is left unchanged.

Concurrent Separation Logic (CSL) [Brookes 2007; O'Hearn 2007] extends separation logic to provide guarantees in concurrent settings. In CSL, the Hoare triple {$P$} {$c$} {$Q$} captures the thread-safety of the program $c$, namely, the memory safety and functional correctness guarantees still hold in the presence of threads executing concurrently.

**F\* and KaRaMeL.** F\* [Swamy et al. 2016] is a proof assistant and program verification framework. It allows users to write, specify, and prove programs in a functional language with a rich type system based on dependent types and user-extensible effects [Rastogi et al. 2021]. To simplify verification, F\* discharges proof obligations using an automated SMT solver [de Moura and Bjørner 2008], while also offering metaprogramming and tactic-based verification facilities [Martínez et al. 2019] in a style similar to Lean [Ebner et al. 2017] or Idris [Brady 2013].

While F\* code extracts to OCaml by default, a subset of the F\* language also extracts to idiomatic C code through the KaRaMeL compiler [Protzenko et al. 2017]. This toolchain was previously successfully used to provide verified C implementations of security-critical applications such as cryptographic libraries [Ho et al. 2022; Polubelova et al. 2020; Protzenko et al. 2020] or binary parsers and conditionizers [Ramananandro et al. 2019; Swamy et al. 2022].

**Steel.** Steel [Fromherz et al. 2021; Swamy et al. 2020] is a recent framework embedded in F\* that allows the use of concurrent separation logic to specify and prove the correctness and safety of concurrent F\* programs. To introduce the reader to Steel and to the F\* syntax used throughout this paper, we present below the signature of the malloc function that we aim to implement.

val malloc (size: size_t) : Steel (array uint8) emp (λ r → null_or_slarray r)
(requires λh0 → T) (ensures λh0 r h1 → not (is_null r) =⇒ length r ≥ size)

The malloc function takes as argument the number of bytes size that must be allocated. It has the Steel effect, indicating that it belongs to the Steel framework. This effect has several indices. First, array uint8 corresponds to the return type of this function. The second and third indices are separation logic predicates, of type slprop. They mimic the specification of memory allocation we introduced earlier: malloc consumes emp (second index), which carries no ownership, and returns null_or_slarray r, where r refers to the returned value. slarray r is the Steel equivalent of r $\mapsto \_$, but applied to arrays instead of references. To faithfully model malloc according to the C standard, we account for the fact that r may be null. Steel's separation logic predicates can capture a rich class of properties about memory; for this paper's purposes, it is sufficient to see them as representing a notion of memory ownership.

The fourth and fifth indices lighten the formalism and simplify the verification effort. In Steel, these indices allow us to specify properties about the contents of memory using the requires and
ensures clauses, operating on the initial memory h0 and the final memory h1. This style has been used successfully by tools such as Dafny [Leino 2010] or Steel's predecessor, Low* [Protzenko et al. 2017], and seems to be a natural style for writing these specifications. Here, the precondition (fourth index) is trivial. The post-condition (fifth index) states that, if the array returned is not NULL, then its length is at least the size initially requested. As we will see in Section 5.2, this predicate can also be used to specify the values stored in the array after the execution of the program, yielding the Steel equivalent of the standard $r \mapsto v$ separation logic predicate. However, one specificity of Steel is that verification conditions related to these indices are discharged by SMT, while those related to the separation logic predicates are handled by a custom decision procedure implemented as an F\* tactic [Fromherz et al. 2021]. To avoid breaking the abstraction of separation logic, these predicates cannot be arbitrary memory predicates, instead, they must be self-framing [Parkinson and Summers 2012], that is, they must only refer to the memory footprint of the separation logic predicates in the context. The Steel framework provides facilities to ensure that the fourth and fifth indices are self-framing by construction. To simplify the presentation, we omit this technicality in this paper, and refer the interested reader to the complete description in Fromherz et al. [2021].

When written in the KaRaMeL-compatible fragment, Steel code extracts to idiomatic C code. For instance, the Steel malloc signature above will yield the following standard C function prototype: `uint8_t* malloc(size_t size)`. This signature is more precise than that of the C standard (`uint8_t*` instead of `void*`); in practice, we add a wrapper that performs a cast, so as to match the expected ABI and thus provide a drop-in replacement for existing userspace memory allocators.

**Steel Combinators.** While Steel's approach allows to separate between properties about the *shape* and *contents* of memory, many common separation logic predicates require a mix of the two. As an example, consider the case of a pointer *p* to a struct, which itself contains a pointer (e.g., a linked list node). Modeling full ownership of the structure and its inner pointer usually requires existentially quantifying on the value of the struct that *p* points to, e.g., $\exists v. p \mapsto v * v. \text{next} \mapsto _$, thus breaking separation between shape (ownership of *p*), and contents reasoning. To this end, Steel offers generic predicates such as sldep, which captures the combination of two slprops *p* and *q*, where the second depends on the contents of the first. Its associated memory view is a dependent pair whose components are the contents of *p* and *q*.

## 3.2 SMT-Friendly Higher-Order Combinators

We now present our handling of slabs, that is, memory pages containing an array of allocation slots. This exhibits several challenges representative of our verification of a modern allocator. Those challenges are all present in the design we ultimately verify; but tackling all of them had to be done iteratively. We now illustrate our methodology on slabs; show how we leverage our specific cocktail of dependent types, SMT, and shallow embedding; and how we promote iterative proofs.

**Modeling Slab Metadata.** In their simplest form, slabs can be of two kinds: either a slab is full, or it contains empty slots which can be used for allocation. The role of the allocator is to keep track of which slabs are available, relying on *slab metadata*.

Abstractly, the metadata slabs_md maps each slab to a value of type status = | Full | Available, indicating whether the slab has remaining free slots. Foreshadowing future extensions, we directly use an inductive type for status instead of a simple boolean. Using the function dispatch shown below, the function associates to each value a corresponding separation logic predicate available_slab or full_slab, omitted here, which captures both the ownership of the underlying free slots and whether at least one slot is available.

```
type mempage = a:array uint8{length a == page_size}
```
let dispatch stat (slab: mempage) = match stat with | Available → available_slab slab | Full → full_slab slab

Our metadata is conceptually a map from slabs to statuses. In our specifications, however, we use
a different formulation that avoids tedious reasoning on the domain of the map. Since we statically
know the number of slabs, and that each slab has associated metadata, we can represent metadata
as a sequence of statuses slabs_md<sub>v</sub> of length equal to the number of slots.

Tying metadata and slabs therefore requires relating a sequence of metadata values with their
corresponding slabs. This pattern, corresponding to an iterated conjunction, is generic and oc-
curs in several contexts, as we will describe in Section 3.4. We therefore capture this through a
helper combinator, called starseq, which given a sequence of length n and a predicate p, returns
p s[0] 0 * ... * p s[n] n. Unbound names (e.g., the type a below) are implicitly bound at the top.

type idx_t (s:seq a) = i:nat{i ≤ length s}
let starseq' (p: a → nat → slprop) (s:seq a) (i:idx_t s) =
  if i = length s then emp else p s.[i] i * starseq' p s (i + 1)
let starseq p s : slprop = starseq' p s 0

Leveraging dependent types and separation logic predicates as first-class values, this combinator is fully generic and works for sequences of any type a with any separation logic predicate p. We remark that the definition of starseq is carefully crafted to behave properly with regards to the unifier and normalizer of F\*; notably, this recursive definition does not unfold during type-checking. This means we avoid a profusion of slprops in the context, which would cause performance and unification issues. Instead, we provide generic lemmas to, e.g., extract the slprop corresponding to a given index, or to easily update the sequence s and modify starseq accordingly without needing to unfold its definition. This leads to much better behavior of F\* and thus an improved user experience.

Iterated conjunctions are not specific to Steel: other tools such as Viper [Müller et al. 2016] or CN [Pulte et al. 2023] also support them in conjunction with SMT verification. Our approach differs however in two key ways. First, the starseq predicate is not natively encoded in Steel, rather, it is defined as a verified library on top of the Steel program logic, therefore ensuring that it is not a trusted component of the framework. Second, the predicates it iterates over are arbitrary separation logic predicates, which are more expressive than Viper's permission logic and do not exhibit the shape limitations required by CN's symbolic execution [Pulte et al. 2023, p14]. In particular, the predicates inside the iterated conjunction can themselves be iterated conjunctions: starseq is just another separation logic resource, of type slprop, which can be passed to functions and predicates in Steel. As we will see in the rest of this paper, we heavily rely on this genericity to nest predicates across abstraction layers.

This approach provides us with a first dose of modularity: we can define proof idioms and helpers
generically, and instantiate them when needed in the codebase, reducing code duplication and
proof effort. Instantiating starseq with slab-related predicates is straightforward, as shown below.

let slabs_sl_aux slabs_md<sub>v</sub> (slabs: array uint8{length slabs % page_size == 0}) =
    starseq (λ stat i → dispatch stat slabs[i*page_size..(i+1)*page_size]) slabs_md<sub>v</sub>

The remaining part is to model storage of slab metadata in memory, and to link it against the
slabs_sl predicate. In our case, we will store the slab metadata as an array of status values, whose
contents are represented as a sequence. To link the two, we will therefore rely on the Steel sldep
predicate previously presented. We emphasize that adopting a different memory representation for
metadata would be straightforward: the only requirement is to provide an slprop whose contents can
be interpreted as a seq status. This first refinement from implementation to "concrete" specification
provides a first layer of abstraction which hides implementation details and serves as a foundation
for subsequent proof layers.
let slabs_sl (slabs_md: array status) (slabs:array uint8{length slabs % page_size == 0}) =
sldep (slarray slabs_md) (λ slabs_mdv → slabs_sl_aux slabs_mdv slabs)

**Optimizing Slab Metadata.** The predicate slabs_sl gives us a separation logic model of the slabs, their metadata, and their respective memory representations. It ensures the well-formedness of the slab architecture, namely, that metadata are coherent with respect to the parts of each slab that the allocator still owns, that is, that were not given to clients. While simple, this first model is also inefficient when attempting to pick a slab during allocation: a linear traversal of the metadata is required to find the first available slab.

To solve this issue, one natural solution is to use a linked list to keep track of the available slabs, thus skipping full slabs when traversing metadata. While lists have a well-known, textbook separation logic specification, one difficulty arises however when attempting to use them to implement a memory allocator. List-like structures typically rely on dynamic memory allocation when, e.g., creating and inserting a new cell, which is exactly what our allocator must implement! To circumvent this circularity, we leverage the fact that the maximum number of slabs is statically known, and instead implement a library for linked lists where all cells are part of one single static array: the slab metadata. We call this datastructure an *arraylist*.

A standard linked list implementation consists of cells with data and a pointer to the next element; the corresponding ownership predicate recursively covers all of the cells in the list. This, however, cannot apply here, as cells are already owned by the outer array. A natural solution is to rely on a non-separating conjunction to combine ownership of the outer array with a shape predicate that captures the structure of the list. However, the automation facilities (notably the framing tactic) in the Steel framework do not support non-separating conjunction well.

To circumvent this issue, we rely on two components. First, as we know that all list elements are located in a given array, we replace next pointers by array indices, of type `size_t`. Second, we separate the specification into two parts: the ownership of the underlying array, and the well-formedness of a list operating on a sequence view `slabs_mdv` of the array contents, and expressed through `is_list`.

type cell (a:Type) = {data : a; next: size_t}
let rec is_list' (slabs_mdv: seq (cell a)) (pred: a → prop) (idx: size_t) (count: nat) : prop =
  if count > length slabs_mdv then ⊥// Cyclic list
else if idx = null_idx then T// Terminal case
else if idx < 0 || idx ≥ length slabs_mdv then ⊥// Out-of-bound
else pred slabs_mdv[idx].data ∧ is_list' slabs_mdv pred (slabs_mdv[idx].next) (count+1)
let is_list slabs_mdv pred idx = is_list' slabs_mdv pred idx 0

The predicate `is_list`' has two particular points of interest. First, it takes as parameter an abstract predicate `pred` operating on data, which must hold for all elements in the list. In our case, we instantiate it below with the property that all statuses in the list are Available. Second, this predicate does not capture ownership, and has therefore type `prop`, and not `slprop`.

Leveraging our combinator-based approach, we finally tie the list shape with ownership of the underlying array. To do so, we use `slrefine`, another generic Steel separation logic combinator. `slrefine` `slp p` captures the ownership of the separation logic predicate `slp`, and that `p` holds on the memory contents of `slp`. The predicate `is_list` also requires the start index of the list. We store it in an additional pointer `r`, and combine it with `arraylist_sl` using the `sldep` predicate previously seen.

let arraylist_sl (ptr: array (cell a)) (pred: a → prop) (idx: size_t) : slprop =
slrefine (slarray ptr) (λ slabs_mdv → is_list slabs_mdv pred idx)
let ind_arraylist_sl (ptr: array (cell a)) (pred: a → prop) (r: ref size_t) : slprop =
sldep (slptr r) (λ idx → arraylist_sl ptr pred idx)
Equipped with this predicate, we can now propagate changes to slabs_sl to replace the simple
array of metadata by an arraylist. Importantly, the link between metadata contents and slabs,
captured by the predicate slabs_sl_aux remains unchanged. The view of predicate ind_arraylist_sl
remains a sequence of statuses<fnref n="1" />, and the use of the sldep combinator separates between properties
about the underlying datastructure shape (the arraylist) and predicates depending on its contents.

$$
\begin{align*}
\text{let is_available (x: status) = x == Available} \\
\text{let slabs_sl (r: ref size_t) (slabs_md: array (cell status)) slabs : slprop =} \\
\quad \text{sldep (ind_arraylist_sl slabs_md is_available r) (\lambda (idx, slabs_md_v) \rightarrow slabs_sl_aux slabs_md_v slabs)}
\end{align*}
$$

The example presented throughout this section is highly representative of our methodology. By relying on custom separation logic combinators, we achieve a high degree of modularity: case in point, the replacement of the initial metadata array by a more complex arraylist structure did not impact proofs relating to the metadata contents. The definition of these combinators relied on two key ingredients, namely, dependent types, and the ability to parameterize over separation logic predicates. Our dependently typed combinators also enable genericity, and reduce code duplication. In particular, by abstracting over the values stored in the array and predicates they must satisfy, we could define helpers on the generic arraylist once and for all (omitted here), e.g., to access metadata in constant time or to update the list, and instantiate them at no extra cost for our specific usecase; this datastructure would be directly reusable in other contexts and with other predicates. Finally, our structure allowed us to preserve the Steel separation between shape and contents reasoning, and to leverage Steel's facilities for SMT solving: predicates operating on memory contents, e.g., to reason about indices or on the metadata values, can be handled by SMT, lowering the cost of verification. In the next section, following our workflow during the development and verification of StarMalloc, we show how this methodology allows us to efficiently iterate on our implementation, progressively obtaining the architecture outlined in Section 2.

3.3 Iterating on Verified Implementations

The arraylists presented in the previous section allow us to efficiently find an available slab in
which to allocate. This model however presents some limitations. First, while it guarantees that all
slabs in the list are available for allocation, it does not ensure that all available slabs are present in
the list, possibly leading to some unused memory, degrading the performance of the allocator.

To avoid this issue, we modify our invariants to also model that full slabs form a list, and that the
two lists partition the metadata. Materializing both lists at runtime presents several advantages;
notably, rather than relying on a global universally-quantified predicate, we can instead perform
our proofs in a constructive manner by directly manipulating those lists, which leads to much
better proof performance. This also makes inductive predicates over those lists much easier to
write, a design decision that will prove useful as we later add even more structure onto our slabs.

Thanks to the structure of our separation logic predicates, these changes are well-contained. We
only need to extend the arraylist_sl predicate, and to add an additional pointer r<sub>f</sub> to the head of the
new list. In particular, proofs and code operating at the array level (e.g., to access metadata) or
on the metadata sequence (to tie its values with ownership of the slabs) are entirely unchanged.
Similarly, incremental changes allow us to add support for the additional lists for partial slabs, as
well as quarantine and guard pages needed to harden our allocator.

$$
\text{let arraylist_sl (ptr:array (cell a)) (pred_a pred_f: a \to prop) (idx_a idx_f: size_t) : slprop =} \\
\text{slrefine (slarray ptr) (\lambda slabs_md_v \to}
$$

<footnote n="1">¹In the presentation, the view of predicate ind_arraylist_sl is actually a seq (cell status); our implementation relies on an additional combinator to transform it into a seq status, omitted for brevity.</footnote>
$\mathit{is_list}$ slabs\_md\_v $\mathit{pred}_a$ $\mathit{idx}_a \wedge \mathit{is_list}$ slabs\_md\_v $\mathit{pred}_f$ $\mathit{idx}_f \wedge \mathit{partition}$ slabs\_md\_v $\mathit{idx}_a$ $\mathit{idx}_f$) \\
$\mathit{let ind\_arraylist\_sl}$ (ptr: array (cell a)) ($\mathit{pred}_a$ $\mathit{pred}_f$: a $\rightarrow$ prop) ($r_a$ $r_f$: ref size\_t) = \\
\mathit{sldep}$ (slptr $r_a$ * slptr $r_f$) ($\lambda$ ($\mathit{idx}_a$, $\mathit{idx}_f$) $\rightarrow$ arraylist\_sl ptr $\mathit{pred}_a$ $\mathit{pred}_f$ $\mathit{idx}_a$ $\mathit{idx}_f$)

A second limitation relates to our handling of another base operation: freeing memory. While
allocation only appends and removes elements from the head of the list (e.g., moving the head of
the available list to the full list when the slab becomes full) which can be done efficiently, freeing
often requires removing an element in the middle of a list: the client can free allocated memory
in any order, and is therefore not required to free an element in the slab that last became full.
Removing an arbitrary element from a linked list induces a complexity linear in the list length in the
worst case; this is at odds with the performance expected from modern allocators. To circumvent
this issue, we instead replaced our implementation of singly linked lists with doubly linked lists,
which allow removal in constant time. Changes were again small: we needed to extend the cell
struct with an additional prev field, and to replace the is_list invariant by its is_dlist counterpart,
capturing additional properties about the doubly linked list structure. Importantly, our reliance
on the SMT solver to reason about the is_list predicate, enabled by the design of our combinators,
greatly simplified updating proofs when switching to is_dlist: most of the inductive proofs, e.g., to
show that the is_(d)list invariant is preserved when inserting or removing an element, are required
by the combinators to have the same structure. This not only forces modularity, but also imposes
the same shape on SMT queries, meaning the SMT solver was often able to automatically prove the
new versions, or only required minimal changes.

One last change focused on the handling of quarantined slabs, by implementing a queue datas-
tructure on top of the corresponding doubly linked list. Following our methodology, this change
was localized to the is_dlist predicate corresponding to quarantine in the arraylist_sl predicate. In
particular, in addition to not modifying proofs relating to the underlying array or the link between
metadata and concrete slabs, this change also did not impact helpers and proofs on neighboring
lists. Required modifications to interpret the doubly linked list as a queue were technical, but are a
standard algorithmic construction; we omit them for brevity.

3.4 Reusing Generic Predicates

Designing generic abstractions parameterized by abstract predicates is a common pattern in higher-
order logics, which allows writing generic proofs that can then easily be instantiated. Our approach
is no exception, most of the predicates presented in the previous sections were defined in a generic,
parametric manner before being specialized with allocator-specific concepts. As we saw, this fosters
resilient and robust proofs in the presence of SMT, and provides a strong structured foundation for
further proofs. We now move beyond slabs and metadata, and show further examples of instantiating
our combinators throughout our codebase.

**Tying Slots and Metadata.** As described in Section 2, a slab is a memory page seen as an array of slots of the same bytesize *size*. During allocation, ownership of one of these slots is given to a client when *size* or fewer bytes of memory are requested. The allocator’s chief objective is to keep track of which slots were previously allocated, and which ones the allocator still owns.

Abstractly, the handling of slots’ and slabs’ metadata share many similarities: in both cases,
metadata maps each slot (resp. slab) to a boolean (resp. status), with a separation logic predicate
capturing slot or slab ownership based on the metadata value. Leveraging the genericity of the
starseq predicate, we can follow the same proof structure, but with a different instantiation of starseq.
First, instead of the arraylist used for slabs, we rely on efficient bitmaps to store slot metadata; to
this end, we implemented and verified a Steel library for bitmaps, which we intend to upstream to
expand the Steel standard library. The Bitmap.as_seq helper is part of this library, and reflects the
contents of the bitmap as a sequence of booleans. The use of bitmaps is made possible because slot metadata requires less information than slab metadata: while slabs can be in five different states (full, partial, empty, quarantine, guard page), requiring the use of an enumeration, slots are either available or in use, which can be captured by a simple bit of information. We remark that we were able to verify a very low-level data structure, and keep the same high-level sequence view of it, without having to resort to a less efficient representation even if to facilitate verification.

The second and last step is to replace the `slabs_sl_aux` predicate by `available slot` shown below. This captures that, depending on the boolean `b`, a slot is either owned by the allocator, i.e., available for allocation, or that the allocator has no ownership (the `emp` predicate), i.e., the slot is currently in use. Combining these two components to instantiate `starseq` provides us with the `slab_sl` predicate, which relates a given slab with its corresponding metadata slots_md.

```
let availableSlot b slot : slprop = if b then slarray slot else emp
let slots_sl size slots_md_v (slab: mempage) : slprop =
    starseq (λ b i → available b slab[i*size..(i+1)*size-1]) slots_md_v
let slab_sl size (slots_md:bitmap) (slab:mempage) : slprop =
    sldep (Bitmap.sl slots_md) (λ slots_md_v → slots_sl size (Bitmap.as_seq slots_md_v) slab)
```

**Reusing the Slab Allocator.** We also leverage our generic abstractions when handling large allocations, that is, allocations larger than a page size. As described in Section 2, these allocations are directly forwarded to the OS via the mmap syscall. The main role of the allocator is to keep track of the pointers currently in use, as well as their size; this is done through an AVL tree.

Similarly to the lists previously presented, tree-like structures have standard separation logic definitions; in our setting, the main implementation challenge is that they typically rely on dynamic allocation to, e.g., create new tree nodes when inserting a value, which is what the allocator aims to provide. To do this, our initial implementation was creating and freeing AVL nodes on-demand through the use of mmap and munmap. This was however largely inefficient, both in terms of speed and memory usage: syscalls such as mmap are expensive, and the OS can only provide memory at the page granularity; much more than needed to store a small AVL node.

To avoid this issue, we instead reinstantiated our code for slab allocations to support dynamic allocation for AVL tree nodes. Concretely, we instantiated a slab allocator with only one size class, corresponding to the size of AVL nodes. To do so, we reused the `arraylist_sl` predicate and leveraged the genericity of our implementation in the size class configuration (further described in Section 3.5). Adapting the AVL tree library we implemented to replace node allocation through mmap by our optimized allocation was then straightforward: node allocation and deallocation was already abstracting over implementation details, and performing the change did not impact the rest of the code and proofs.

## 3.5 Partial Evaluation and Genericity

The approach presented so far focused on designing modular, generic abstractions that reduced the verification effort. However, the benefits of genericity can also appear in implementation efforts, namely, in making StarMalloc easily configurable.

General-purpose allocators such as StarMalloc can be used in many contexts: clients operating in a purely sequential setting might want to disable arenas (Section 2) to avoid memory waste and unneeded locking, while clients that only perform very small allocations might want to disable the larger size classes. When modifying the allocator configuration, some changes simply require modifying global variables (e.g., to adapt the size of a global array), but others are more involved, requiring deeper changes to the allocator's implementation (e.g., to initialize different numbers of size classes for different sizes, and hence with different slot layouts).
When implementing an unverified, configurable allocator in C, a common technique is to rely on preprocessor macros, which are expanded at compile time into specialized code depending on static, user-supplied parameters. This is however error-prone, and not ideal for security-critical code. Performing deep modifications into the code is also not acceptable; even in a verified setting where these changes could be safely performed, the effort involved would deter most clients.

In this section, we show how to write a generic Steel implementation, parametric in a number of arenas and size class architecture, while ultimately retrieving specialized, idiomatic C implementations after extraction. The key technical ingredient is to leverage custom compile-time reduction through F\*’s normalizer, a technique previously applied to other verification projects [Ho et al. 2023, 2022; Swamy et al. 2022]. The normalizer is a key component of typecheckers in dependently typed languages, which allows to reduce pure terms. In F\*, compiler hooks (such as norm described below) enable its application at F\*-compile time, that is, after verification, but before extraction to C takes place. We describe how to apply this in the context of Steel.

Our goal is to write an allocator generic in a size class architecture. For instance, we wish to write the size class initialization function init_size_classes below, which takes as arguments arrays for the size classes and metadata, as well as a list of sizes l representing the size classes configuration.

```c
let rec init_size_classes size_classes md l = match l with
  | [] → () | slot_size :: tl → init_size_class slot_size size_classes[0] md[0];
        init_size_classes tl size_classes[1..] md[1..]
let init size_list = let size_classes = mmap .. in let md = mmap .. in
  init_size_classes size_classes md size_list
```

While this code is valid Steel and successfully verifies, it is not compatible with KaRaMeL extraction: pure lists do not extract to C (they would require a GC, since their ownership is not tracked). For presentation, we will assume that a client wishes to have two size classes, of slot size 16B and 32B respectively; they will specify this by modifying the global variable sc_list. We rely on the F\* primitive norm to instruct the compiler to reduce the application init sc_list, according to the reduction steps custom_steps (omitted), which include e.g. unfolding the definition sc_list and reducing pattern matchings operating on lists, but not unfolding the definition of init_size_class. After normalization, all the recursive calls to init_size_classes have been unfolded, and all occurrences of lists are gone, which enables KaRaMeL to extract to the idiomatic C init shown below.

```c
let sc_list = [16; 32]
let init = norm custom_steps (init sc_list)

void init() { // Generated C code after normalization
    size_classes = mmap .. ;
    md = mmap ..;
    init_size_classes size_classes[0] md[0] 16;
    init_size_classes size_classes[1] md[1] 32; }
```

This approach makes it straightforward to configure StarMalloc according to a client’s needs. We only need to modify the value sc_list and to recompile our project; apart from this variable, all the code and proofs are left unchanged. We apply this methodology to all parts of StarMalloc where the static configuration impacts the shape of the code; this includes for instance selecting an appropriate size class in which to allocate, and handling arenas. This style is pervasive: for instance, quarantine, guard pages, and zeroing are all conditional on F\* compile-time switches, meaning that if the user opts out of those, F\* completely eliminates the corresponding if false expressions and those features are absent from the generated C code. We emphasize that this specialization at
extraction-time does not extend our trusted computing base: F*'s normalizer is a key component
of its typechecker, and hence already part of the TCB.

**Implementation differences with hardened_malloc.** Our support of different size classes configurations departs from hardened_malloc's implementation, which hardcodes one specific configuration. Our approach allows us to easily adapt StarMalloc to a wide range of contexts; however, it also comes at a cost. Configurations are abstract in the generic Steel code that implements, e.g., size class initialization; these functions cannot be optimized based on one concrete configuration.

One telling example is our function selecting a size class in which to allocate, based on the
number of bytes requested. To be applicable to any list of size classes, our generic implementation
successively compares the requested number of bytes *n* to the size of each size class, until it finds
one large enough to accomodate *n*. After specialization, this results in a cascade of if-then-else
branching, which can be expensive when branch prediction is poor. Leveraging its specific choice of
configuration, hardened_malloc instead performs bitwise manipulations on *n* to find an appropriate
size class in constant time. To address this inefficiency, we leverage well-known compile-time
specialization techniques in F* [Ho et al. 2023], and allow the user to provide not only a choice of
size classes, but also a corresponding, provably correct size class selection function. In the version
of StarMalloc used in our evaluation, we pick both the size class configuration and the selection
function used by hardened_malloc.

4 Extending Steel for Verified Systems Programming

As part of this work, we had to adapt numerous parts of the Steel toolchain to support lower-
level idioms than what was previously possible. The difficulties all revolve around reconciling
existing, non-negotiable design choices from the world of low-level systems C programming with
the principled, clean, formal abstractions exposed by the Steel framework. We believe the solutions
we came up with are general, and could be adopted by any other verification framework that aims
to model similar low-level concepts.

4.1 Locks

The first difficulty concerns locks. In concurrent separation logic, locks are regular (freely duplicable)
values that protect access to a separation logic predicate [Gotsman et al. 2007; Hobor et al. 2008].
Concretely, Steel defines val lock (p:slprop) : Type, and a value of this type guards access to p. Locks
can be created via val new_lock (p:slprop) : Steel (lock p) p (λ_ → emp); the arguments of Steel indicate
that in order to obtain a value of type lock p, the caller has to relinquish p, and receives no predicate
after the call (the empty predicate). Acquiring a lock ensures the caller obtains p; releasing a lock
requires reliquinshing ownership of p.

We set out, in this work, to connect the Steel model and implementation to the real-world
environment of an OS and a typical userland stack. Specifically, this means we need to implement
the Steel model above using whatever facilities are provided in C by pthreads, an efficient, pervasive
library that leverages kernel-level abstractions (e.g., futexes) to implement efficient locking with
as little contention as possible. A custom implementation based on a userland primitive such as
compare-and-swap is thus out of the question.

In the pthread library, the type of locks is pthread_mutex_t. Unfortunately, locks are not iden-
tified with a unique identifier that would be contained within that value, but rather, by the ad-
dress of the value itself. This means that a simple let y = x in F* yields, once extracted to C, a
statement of the form pthread_mutex_t y = x; which effectively generates a new lock with a dif-
ferent identity from x. Worse, our model of locks in Steel generates prototypes in C, such as
void acquire_lock(pthread_mutex_t p), which we then need to implement by hand. Here, this simply
cannot be done, as calling pthread_mutex_lock(&p) would operate on a copy of the original lock passed by value via the function call. Fixing the Steel model is not possible; it would require materializing the lock itself as an slprop, preventing us from passing the lock around.

To fix this issue, we rely on an existing nanopass in the Steel-to-C KaRaMeL compiler, namely the struct-by-address pass, initially implemented to target the CompCert compiler, and covered by the original soundness result [Protzenko et al. 2017, Appendix E.6]. This pass ensures that function arguments of struct types are always passed by reference and never by copy, which in turn avoids relying on an unverified compilation pass in the CompCert frontend. We extended this pass to also operate on values of type lock, meaning the signature of acquire_lock in Steel now produces a C prototype of the form void acquire_lock(pthread_mutex_t *p), which avoids the earlier issue. We then added a translation validator that errors out if any subexpression ever materializes at type pthread_mutex_t. This means that once a lock is declared, it may only be passed around by address, and never by value. This reduces the soundness of the lock compilation scheme to that of the (trivial) validator. The validator then identified situations that did lead to locks being copied. Those essentially stemmed from F\* lifting effectful subexpressions into their own let-bindings, because of its monadic effects. We eliminate those via a series of one-liner cosmetic optimizations. For instance, in KaRaMeL's AST, we now rewrite let tmp; new_lock(&tmp); *p = {*p with lock = tmp} into new_lock(&p→lock).

## 4.2 Array Extensions and C Standard

The subset of Steel that compiles to C lacked several features needed to implement a memory allocator. Most of these relate to low-level concerns of the C model. As with the original F\*-to-C extraction work [Protzenko et al. 2017], we rely on a careful, in-depth review of the C standard to accurately and correctly model C semantics as a shallow embedding in F\*.

We first had to implement a Steel model of size_t, the type of object sizes, whose size is not defined by the C standard, but rather is determined by the C data model chosen by the compiler. All that is known statically (since C99) is that size_t is at least 16 bits; the same is known for the Steel type SizeT.t. However, we frequently need to assume larger sizes in our implementation. To that effect, we designed special functions to cast 32- and 64-bit Steel integers into SizeT.t; those functions require static preconditions (e.g., fits_u32), which can only be introduced by calling stateful functions (e.g., intro_fits_u32). The corresponding implementation in KaRaMeL adds support for SizeT.t across the various passes and ASTs, and compiles the intro_* functions to static asserts (e.g. _Static assert(sizeof size_t ≥ sizeof uint32_t)) in the final C.

Similarly, we had to introduce a new type for differences between addresses, which models ptrdiff_t, along with corresponding support in F\*, Steel and the KaRaMeL compiler. A Steel value of type PtrDiff.t can be obtained by subtracting two Steel pointers, as long as they belong to the same allocation unit [ISO 1999, §6.5.8] or, in Steel terminology, as long as they have the same array base. This is particularly useful to implement free in our allocator, where we need to locate a user-provided pointer within its slab in order to free the slot at the corresponding index. To do so, we simply compute the difference of the user-provided pointer with the base address of its corresponding slab, and obtain a positive PtrDiff.t. Values of PtrDiff.t that are known to be positive can be converted to SizeT.t: we thus obtain the index of the user-provided pointer into its slab, which in turn allows us to update the corresponding metadata to mark this slot as free.

Proving that two objects have the same array base can be delicate. Notably, in the case of free, it is not generally true that the user-provided pointer lies within our reserved virtual address space. Indeed, nothing prevents the user from giving us a pointer issued by another allocator, or any other value. This means that we need to perform a dynamic check in order to obtain a predicate, dubbed withinBounds p_l p_h p, that ascertains that the user-provided p is in the virtual address
space `[p_l, p_h]`. To the best of our knowledge, there is no way to implement this dynamic check without relying on what may be arguably labeled as undefined behavior in C. For that reason, we isolate this contentious part in a separate, hand-written C function, and leave the Steel model untouched.

To see why computing withinzarbs entails undefined behavior in C, recall that the C standard (§6.5.8) requires that pointer comparisons be done on objects that originate from the same allocation unit. But this is precisely what we are trying to determine here! We follow standard practice, and assume that as long as we prevent the C function from being inlined at call-site, the C compiler will be unable to conclude that the pointers do not belong to the same object, and thus will compile the function as expected. All other allocators adopt the same implementation. We reiterate that this does not affect the modeling of C in F\*, since the debatable function is hand-written in C.

A final feature we added to the Steel framework and toolchain concerns top-level immutable arrays; these are a common C feature that was until then missing from Steel. We added support for those, and they compile with the expected const qualifier. By virtue of being top-level, they can be trivially indexed by the (pure, proof-level) sequence they represent, a design which makes those top-level arrays easy and convenient to use within StarMalloc. By virtue of being immutable, one can retrieve the corresponding values, and show that they remain unaffected by (necessarily) disjoint updates, without any tedious memory reasoning. This mechanism relies on a custom slprop, which is duplicable and supports concurrent accesses. This novel Steel feature yields much better performance than, say, a global lock, which would further defeat our fine-grained concurrency.

# 5 Implementation

Our work was entirely performed in F\*, using the Steel framework. We now provide an overview of our implementation, and of the different functionalities of our allocator.

## 5.1 Proof Idioms and Datastructures

As part of the development of StarMalloc, we defined and implemented a range of generic libraries which we instantiated to fit our needs. We already presented several of them in the previous sections; they include datastructures (statically allocated doubly linked lists, efficient bitmaps, AVL trees, top-level const arrays, FIFO queues), proof idioms and generic separation logic combiners (starseq, extensions and helpers for slrefine and sldep), concurrency primitives (separation logic locks with native extraction to pthread mutexes), and modeling of the interaction with the OS (axiomatization of memory-related syscalls, e.g., mmap). These libraries required significant engineering and modeling effort, and represent a large part of our development, totalling more than 13,000 lines of F\* code. While crucial to the development of StarMalloc, they are a contribution of their own, which significantly decreases the effort required for future systems verification projects in F\*. We organized our codebase to ensure they are entirely separate from the code of StarMalloc, and hope to upstream them to the Steel standard library in the future to benefit to the community.

## 5.2 StarMalloc

We estimate that our implementation effort for StarMalloc took two and a half person-years. This includes building a substantial foundation that was missing from Steel, starting from arrays, and moving up to datastructures (AVL trees, bitmaps, arraylists, queues). A lot of work was foundational, and aimed at understanding how to successfully model, verify, and extract an extremely low-level view of memory within the framework. Thanks to the proof methodology presented in Section 3, which provides tight abstraction boundaries between the various components of StarMalloc, it- erations on the verified codebase are easier to perform. Case in point, we implemented a first batch of security mechanisms in less than a week, without affecting the rest of the code. The tight
abstractions have the added benefit of preserving a lot of intermediary verification files, meaning that one can efficiently rebuild and re-extract StarMalloc when iterating on one sub-component.

Table 1 provides figures about our implementation. StarMalloc currently consists of about 42,000 lines of F\* code, extracting to close to 6,000 lines of C code (excluding whitespace and comments); our reusable libraries form a large part of this. StarMalloc also contains a small amount of C glue code, needed, e.g., to match our axiomatization of OS syscalls with actual code calling mmap.

**Supported APIs.** In addition to the standard malloc and free used for allocating and deallocating, StarMalloc supports the other memory management specified by the C99 standard [ISO 1999, §7.20.3], namely, realloc and calloc. Unfortunately, real-world applications commonly rely on other extensions, e.g., from more recent C standards (e.g., aligned_alloc), or from the GNU C library (malloc_usable_size). The absence of these functions can lead to surprising runtime errors. For instance, if malloc_usable_size is not provided but called by an application, function symbols will typically resolve to the standard C library implementation, leading to incoherent results when allocations were performed through StarMalloc. Applications rarely specify the complete set of APIs they rely on; this led to issues when trying to experimentally compare

StarMalloc’s performance to other hardened state-of-the-art allocators (Section 6.1) such as FreeGuard [Silvestro et al. 2017] or Guarder [Silvestro et al. 2018] which do not expose all required APIs for our benchmarking suite. To circumvent this issue, we performed extensive debugging and sleuthing, to make sure StarMalloc provides all standard, widely used extensions such as malloc_usable_size, memalign, or aligned_alloc, hence offering a complete API sufficient for use with the Firefox browser (Section 6.2). For other functions that we identified but do not implement (yet), such as valloc or pvalloc, we provide C stubs that raise a fatal error when called, avoiding silent fallbacks to the C standard library. These functions seem obsolete, and none of the applications we tested StarMalloc with use them.

**Hardening Features.** As described in Section 2.2, StarMalloc provides several hardening mechanisms, such as segregated metadata, canaries, or the use of quarantine and guard pages. Formally establishing security guarantees about hardening mechanisms is an open question and out of scope for this work, we instead rely on the rich literature on allocator design to motivate their usefulness and efficiency. We however wish to prove their correctness, namely, their implementation matches their expected design, and preserves the allocator’s functionalities. We briefly show how zeroing and guard pages impact our specifications; following the methodology outlined in Section 3, required code changes are often localized and well-contained.

To specify that allocations must be zero-filled, we extend the specification of malloc presented in Section 3.1 as follows, adding an extra postcondition in the ensures clause. The postcondition ensures that the contents of the returned pointer r in the final state h1 only consists of zeros. As mentioned in Section 2.2, our free operation takes care of zeroing, and our malloc operation (and others) takes care of checking that memory is still zero. If the memory is corrupted, the allocator returns NULL, thus satisfying the postcondition.

val malloc (size: size_t) : Steel (array uint8) emp (λ r → null_or_slarray r) (requires λ_ → T)
(ensures λ_ r h1 → not (is_null r) = ⇒ (length r ≥ size ∧ (∀ (i:nat{i < size}). get (h1.[r]) i == 0)))

<table><caption>Table 1. Lines of F\* code for each component of StarMalloc, excluding whitespace and comments. Misc includes starseq, other helpers related to sldep and slrefine, plus various library functions not found in F\*'s standard library.</caption><thead><tr><th>Component</th><th>LoC</th></tr></thead><tbody><tr><td><strong>Reusable Libraries</strong></td><td></td></tr><tr><td>Bitmaps</td><td>1,520</td></tr><tr><td>Arraylist</td><td>3,785</td></tr><tr><td>AVL</td><td>4,332</td></tr><tr><td>Misc</td><td>4,022</td></tr><tr><td><strong>StarMalloc</strong></td><td>28,059</td></tr><tr><td><strong>C glue</strong></td><td>330</td></tr><tr><td><strong>Total</strong></td><td>41,716</td></tr></tbody></table>
We previously showed (Section 3.3) how to extend the arraylist datastructure to support additional slab lists, including one for keeping track of guard pages. All that is left is to model guard pages using separation logic: we want to design an slprop slab-guard slab capturing that slab corresponds to a guard page; this will be the predicate associated to a Guard status by the dispatch function.

Importantly, the slab guard predicate is abstract, and we only provide an introduction rule, as shown below. This induces a form of monotonicity: once a slab is marked as slab guard, by virtue of abstraction, it can never be eliminated to retrieve a separation logic predicate on which the allocator could operate, or that it could transform to an slarray to pass to the client. Under the hood, the introduction rule is implemented as a call to mmap with the PROT_NONE flag; this ensures that any access to a guard page will result in a SIGSEGV returned by the OS.

let dispatch stat slab = match stat with ... | Guard → slab guard slab
val slab guard slab : slprop val slab guard intro slab : Steel unit (slarray slab) (λ_ → slab guard slab)

Additionally, guard pages must appear following a specified pattern; typically, every guard_int pages, where guard_int is a statically fixed, user-defined constant. To specify this, we extend the slabs_sl_aux predicate, which iterates over all slabs using starseq. guard_int and guard_start are two global Steel constants that can be easily changed without modifying other parts of the code, thus making experimenting with different guard pages patterns trivial.

let slabs_sl_aux ... = ... starseq (λ stat i → dispatch ... ∧ (i % guard_int = guard_start) = ⇒ stat = Guard) ...

**Syscall Modeling.** Memory allocators provide a layer on top of operating systems: they manage memory obtained through syscalls such as mmap. To implement and verify an allocator, it is thus necessary to model mmap's behavior. In this work, we rely on the axiomatization shown below.

val mmap (size: size_t) : Steel (array uint8) emp (λ r → slarray r) (requires λ_ → size > 0)
(ensures λ_ r h1 → length r ≥ size ∧ ∀(i:nat{i < length r}). get (h1.[r]) i = 0 ∧ aligned r page_size)

This model assumes that mmap always returns a valid array of bytes, of size at least greater than the length requested. To do this, it statically requires size to be greater than zero; indeed, according to its specification, mmap fails when called with size=0. Additionally, this signature does not model resource exhaustion at the OS level: in practice, if mmap returns NULL at runtime because the OS could not provide further memory, we raise an uncatchable fatal error and interrupt the execution of the allocator. Our axiomatization also states that the returned memory is zero-initialized; to guarantee this, our implementation calls mmap with the MAP_ANONYMOUS flag.

One last point of interest relates to our handling of alignment, captured by the predicate aligned r page_size. The C standard dictates that values returned by malloc must be suitably aligned for "any object with a fundamental alignment requirement". In practice, this means that malloc satisfies the alignment requirements of the largest scalar type, typically long double, which is either 8 or 16 depending on the ABI. Naturally, larger alignments are oftentimes needed, for instance when using vector types (SSE, SSE2). To that end, C11 and later define aligned_alloc, which supersedes previous extensions such as memalign and posix_memalign. All the standard specifies is that aligned_alloc may fail if the alignment is invalid or greater than that supported by the platform.

To formally capture alignment constraints, we rely on the predicate aligned ptr n, which represents that ptr is aligned on a n-bytes boundary; the postcondition of mmap captures our assumption that calls to mmap always return a page-aligned memory. This predicate is propagated throughout our code, and is eventually provided to the client as a post-condition of aligned_alloc (aligned ptr n) or malloc (aligned ptr 16). Our malloc returns values that are always aligned on a 16-bytes boundary, a stricter version of what some older ABIs (e.g., Linux x86) permit. To facilitate reasoning within StarMalloc, we mostly keep the aligned predicate abstract. Non-linear arithmetic is circumscribed
to one-controlled lemma that goes from aligned ptr page_size to smaller alignment constraints, thus limiting issues with SMT solvers that are notoriously unstable when non-linear arithmetic is involved [Bosamiya et al. 2022; Zhou et al. 2023].

**Differences with hardened_malloc.** While StarMalloc inherits hardened_malloc's design, our implementation exhibits small differences. The most impactful, which we previously described in Section 3.5, is our unoptimized default implementation of size class selection during allocation. In exchange, clients can easily change the size class configuration of StarMalloc. Other notable changes relate to different choices of datastructures for several components.

First, while StarMalloc uses AVL trees to store metadata for large allocations, hardened_malloc relies on more efficient hashtables. Several projects showed how to formally verify hashtable implementations [De Boer et al. 2023; Pottier 2017]; using AVL trees instead allowed us to avoid tedious reasoning about collision strategies. In practice, our different choice of datastructure only induces a small overhead: in our implementation, operations on AVL trees are always performed in conjunction with expensive mmap or munmap syscalls.

Second, to simplify separation logic reasoning, StarMalloc uses separate arrays for storing slab and slot metadata, which allows us to use the simple slarray predicate to reason about metadata. In contrast, hardened_malloc merges information about slab and slot metadata into a unique array. There is no technical limitation preventing us from adopting a similar approach in Steel, for instance, separation logic predicates in the style of fictional separation logic [Jensen and Birkedal 2012] would allow us to split the view of a unique array into slot and slab metadata.

## 5.3 Trusted Computing Base (TCB)

Similarly to other verification projects, our TCB includes our verification toolchain, which consists of the F\* proof assistant [Swamy et al. 2016] and the underlying Z3 SMT solver [de Moura and Bjørner 2008], as well as the KaRaMeL compiler [Protzenko et al. 2017] that extracts F\* code to C. To obtain executable code, we thus also need to assume the correctness of a C compiler.

The safety and correctness of StarMalloc are captured through the concise Steel signatures of the API functions exposed to client programs, e.g., malloc or free. They often have trivial preconditions, when this is not the case, we attempt to apply defensive programming. For instance, the colloc function aims to allocate an array of n objects of a given size; its correctness requires that the multiplication n \* size does not overflow. To avoid API misuses, we define a wrapper that checks this at runtime, thus exposing a clean API with trivial preconditions to the user.

The last part of our TCB is our axiomatization of the interaction of the OS, i.e., our model of mmap and munmap. While the corresponding Steel signatures are designed to be simple and easy to review, the underlying C implementation, calling the syscalls with specific arguments, needs to be carefully audited. Doing so, we found a mismatch with our assumptions at the Steel level (a missing flag in mmap), which we fixed.

## 6 Evaluation

We now compare StarMalloc with other state-of-the-art memory allocators, including security-oriented allocators, e.g., DieHarder [Novark and Berger 2010] and hardened_malloc [GrapheneOS Development Team 2021], and regular allocators, such as the glibc and the next-gen musl allocators.

Doing so, we aim to answer the following two questions: i) is our verification methodology effective enough to retrieve the performance of our initial target, hardened_malloc, and ii) is StarMalloc usable as a drop-in replacement in existing, widely used applications.

Our evaluation relies on two sets of benchmarks. First, to provide a fine-grained performance comparison with other allocators, we reuse mimalloc-bench [Leijen et al. 2018], a comprehensive
and popular suite which contains both allocator stress-tests and real-world applications. To evaluate
the real-world readiness of our allocator, we then describe our integration of StarMalloc within the
Firefox browser, which required an extensive set of allocator features.

**Experimental Setup.** We run experiments on a 12-core (4 performance cores, 8 efficient cores), 16-thread machine with an Intel(R) Core(TM) i5-13600H @ 4,80GHz processor and 32GB memory, using Linux 6.6 and glibc 2.40. To ensure reproducible results, we use the “performance” scaling governor (meaning all cores pegged at maximum speed without dynamic CPU scaling), and increase `vm.max_map_count` from 65,530 to 1,048,576 to ensure allocators using a large number of memory mappings, such as `hardened_malloc` and `StarMalloc` for guard pages, work properly. Geometrical mean of 5 runs is used. Aiming for an apples-to-apples comparison, we use the same configuration as `hardened_malloc`, namely, the guard page interval set to 2 and the number of arenas set to 4, with quarantine and zeroing enabled.

## 6.1 Performance Evaluation

**mimalloc-bench.** Our performance evaluation relies on the mimalloc-bench testsuite, also used by recent works on allocators [Bramley et al. 2023; Erdős et al. 2022; Leijen et al. 2019; Li et al. 2023; Lin et al. 2024]. It consists of two categories of benchmarks. The first series are real-world applications, such as the Lean compiler, the Z3 SMT solver, or the redis key-value database. The second series of benchmarks stress-tests allocators via specific allocation patterns which are not representative of real-world applications, but that allow to pinpoint inefficiencies in allocator designs or implementations. As part of this work, we improved mimalloc-bench by allowing the use of the testsuite with recent compiler toolchains, and fixed several compilation issues and bugs in benchmarking scripts; we contributed several patches that were merged upstream.

The most meaningful comparison is between `StarMalloc` and `hardened_malloc`. Figures about other allocators help to situate `hardened_malloc` and `StarMalloc` in the allocator landscape, compared to both widely used but not necessarily security-oriented allocators (glibc and the nextgen implementation for musl libc [Felker 2020]), and to security-oriented allocators from the academic literature (DieHarder [Novark and Berger 2010]). We present experimental results in Table 2 and Table 3. We attempted to include `Guarder` [Silvestro et al. 2018] or `FreeGuard` [Silvestro et al. 2017] in our evaluation, but did not manage to make them work with our benchmarks. Upon inspection of the code, this seems due to publicly available versions lacking support for several widely used functions, such as `aligned_alloc` or `malloc_usable_size`.

**Total Execution Time.** A meaningful way to measure an allocator's performance is to measure the client program's total execution time. On the first series of benchmarks (real-world applications), the performance overhead compared to `hardened_malloc` is within 0.79x to 1.29x. For the second series (stress-tests), we observe that `StarMalloc` performs within 0.69x to 1.12x of `hardened_malloc` on all tests, except for one outlier at 1.36x (rptestN).

Broadening our scope to look at other allocators, we remark that our performance and hardened_malloc's is further apart from non-security-oriented allocators like glibc. This is the cost of defensive security measures; ultimately, application developers will have to pick their balance between security and performance. Nevertheless, `StarMalloc` outperforms `mng` and `scudo` for some benchmarks. More broadly, we observe a greater variety of performance profile across allocators, with greater variation on micro-benchmarks than on realistic workloads. These results suggest that no single choice of optimizations is the “right” one for every workload. Additional benchmarks (not listed here) on different processors show that microarchitecture revisions can also significantly influence the final results.
<table><caption>Table 2. Execution time of various programs, measured against the following allocators: dieharder ("dh", [Novark and Berger 2010], revision 640949f), FFmalloc ("ff", [Wickman et al. 2021], revision 2f24ecf), hardened_malloc default version ("hm", [GrapheneOS Development Team 2021], revision 995ce07), isoalloc ("iso", [Rohlf 2020], revision 2670d5f), mimalloc-secure ("mi-sec", [Leijen et al. 2019], revision b66e321), nextgen malloc implementation for musl libc ("mng", [Felker 2020], revision 2ed5881), scudo ("scudo", [LLVM Project 2023], revision 1654d7d), slimguard ("sg", [Liu et al. 2019], revision 7d9139a), snmalloc-secure ("sn-sec", [Liétar et al. 2019], revision dc12688), StarMalloc ("st", this work), and the glibc allocator ("glibc", version 2.40). All times are normalized and presented relative to hardened_malloc. ERR corresponds to crashes during benchmarking.</caption><thead><tr><th>Benchmark</th><th>st</th><th>hm</th><th>dh</th><th>ff</th><th>iso</th><th>mi-sec</th><th>mng</th><th>scudo</th><th>sg</th><th>sn-sec</th><th>glibc</th></tr></thead><tbody><tr><td>barnes</td><td><strong>1.00</strong></td><td>1.00</td><td>1.05</td><td>1.01</td><td>1.02</td><td>1.00</td><td>1.02</td><td>1.00</td><td>1.00</td><td>1.00</td><td>1.00</td></tr><tr><td>cffrac</td><td><strong>0.86</strong></td><td>1.00</td><td>1.79</td><td>0.70</td><td>1.04</td><td>0.59</td><td>0.71</td><td>0.63</td><td>0.49</td><td>0.48</td><td>0.49</td></tr><tr><td>espresso</td><td><strong>1.10</strong></td><td>1.00</td><td>1.35</td><td>0.92</td><td>1.05</td><td>0.77</td><td>1.17</td><td>0.80</td><td>0.78</td><td>0.70</td><td>0.78</td></tr><tr><td>gs</td><td><strong>1.20</strong></td><td>1.00</td><td>0.99</td><td>1.71</td><td>0.64</td><td>0.47</td><td>0.78</td><td>0.51</td><td>0.44</td><td>0.51</td><td>0.44</td></tr><tr><td>larsonN</td><td><strong>0.81</strong></td><td>1.00</td><td>58.11</td><td>3.27</td><td>41.76</td><td>0.13</td><td>6.45</td><td>0.74</td><td>0.06</td><td>0.05</td><td>0.06</td></tr><tr><td>larsonN-sized</td><td><strong>0.79</strong></td><td>1.00</td><td>55.74</td><td>3.22</td><td>40.79</td><td>0.13</td><td>6.34</td><td>0.73</td><td>0.06</td><td>0.05</td><td>0.06</td></tr><tr><td>leanN</td><td><strong>0.93</strong></td><td>1.00</td><td>7.00</td><td>0.72</td><td>8.39</td><td>0.59</td><td>2.02</td><td>0.70</td><td>0.64</td><td>0.55</td><td>0.63</td></tr><tr><td>lua</td><td><strong>1.26</strong></td><td>1.00</td><td>ERR</td><td>1.07</td><td>1.00</td><td>0.81</td><td>1.03</td><td>0.82</td><td>0.79</td><td>0.80</td><td>0.79</td></tr><tr><td>mathlib</td><td><strong>0.99</strong></td><td>1.00</td><td>ERR</td><td>0.79</td><td>1.66</td><td>0.68</td><td>0.86</td><td>0.71</td><td>0.70</td><td>0.65</td><td>0.70</td></tr><tr><td>redis</td><td><strong>0.93</strong></td><td>1.00</td><td>3.09</td><td>0.68</td><td>1.53</td><td>0.80</td><td>0.76</td><td>0.62</td><td>0.58</td><td>0.52</td><td>0.57</td></tr><tr><td>rocksdb</td><td><strong>0.92</strong></td><td>1.00</td><td>ERR</td><td>0.93</td><td>ERR</td><td>0.84</td><td>ERR</td><td>0.86</td><td>0.80</td><td>ERR</td><td>0.80</td></tr><tr><td>z3</td><td><strong>1.29</strong></td><td>1.00</td><td>1.91</td><td>1.07</td><td>1.40</td><td>0.77</td><td>1.03</td><td>0.77</td><td>0.74</td><td>0.74</td><td>0.71</td></tr><tr><td>alloc-test1</td><td><strong>1.07</strong></td><td>1.00</td><td>2.18</td><td>0.81</td><td>1.12</td><td>0.68</td><td>0.91</td><td>0.62</td><td>0.60</td><td>0.52</td><td>0.60</td></tr><tr><td>alloc-testN</td><td><strong>1.05</strong></td><td>1.00</td><td>10.52</td><td>0.15</td><td>6.29</td><td>0.06</td><td>4.40</td><td>0.07</td><td>0.06</td><td>0.05</td><td>0.06</td></tr><tr><td>cache-scratch1</td><td><strong>0.98</strong></td><td>1.00</td><td>1.02</td><td>1.02</td><td>1.02</td><td>0.99</td><td>1.01</td><td>0.99</td><td>0.99</td><td>0.98</td><td>0.98</td></tr><tr><td>cache-scratchN</td><td><strong>1.00</strong></td><td>1.00</td><td>1.11</td><td>1.11</td><td>1.13</td><td>1.02</td><td>1.08</td><td>1.02</td><td>0.96</td><td>0.96</td><td>0.96</td></tr><tr><td>cache-thrash1</td><td><strong>1.00</strong></td><td>1.00</td><td>1.01</td><td>1.01</td><td>1.01</td><td>1.00</td><td>1.01</td><td>0.99</td><td>0.99</td><td>0.99</td><td>0.99</td></tr><tr><td>cache-thrashN</td><td><strong>1.04</strong></td><td>1.00</td><td>1.08</td><td>1.13</td><td>1.13</td><td>1.04</td><td>1.04</td><td>1.00</td><td>1.02</td><td>1.04</td><td>1.04</td></tr><tr><td>glibc-simple</td><td><strong>0.92</strong></td><td>1.00</td><td>1.71</td><td>0.59</td><td>1.03</td><td>0.39</td><td>1.07</td><td>0.54</td><td>0.51</td><td>0.29</td><td>0.50</td></tr><tr><td>glibc-thread</td><td><strong>1.12</strong></td><td>1.00</td><td>12.26</td><td>0.24</td><td>7.80</td><td>0.05</td><td>5.68</td><td>0.06</td><td>0.04</td><td>0.03</td><td>0.04</td></tr><tr><td>malloc-large</td><td><strong>1.00</strong></td><td>1.00</td><td>1.76</td><td>1.00</td><td>0.30</td><td>0.10</td><td>1.00</td><td>1.00</td><td>0.14</td><td>0.29</td><td>0.14</td></tr><tr><td>mleak10</td><td><strong>0.96</strong></td><td>1.00</td><td>1.51</td><td>11.19</td><td>1.44</td><td>0.96</td><td>1.33</td><td>1.15</td><td>0.93</td><td>1.12</td><td>0.96</td></tr><tr><td>mleak100</td><td><strong>1.02</strong></td><td>1.00</td><td>1.14</td><td>11.41</td><td>1.13</td><td>1.06</td><td>1.09</td><td>1.16</td><td>0.98</td><td>1.16</td><td>0.98</td></tr><tr><td>mstressN</td><td><strong>0.80</strong></td><td>1.00</td><td>9.82</td><td>1.43</td><td>7.72</td><td>0.45</td><td>4.47</td><td>0.71</td><td>0.44</td><td>0.37</td><td>0.44</td></tr><tr><td>rbstress1</td><td><strong>0.87</strong></td><td>1.00</td><td>3.10</td><td>ERR</td><td>ERR</td><td>0.77</td><td>0.83</td><td>0.82</td><td>0.81</td><td>0.75</td><td>0.80</td></tr><tr><td>rbstressN</td><td><strong>0.96</strong></td><td>1.00</td><td>1.43</td><td>ERR</td><td>ERR</td><td>0.84</td><td>0.90</td><td>0.83</td><td>0.83</td><td>0.78</td><td>0.83</td></tr><tr><td>rptestN</td><td><strong>1.36</strong></td><td>1.00</td><td>37.4</td><td>5.30</td><td>7.82</td><td>0.40</td><td>4.01</td><td>1.14</td><td>0.29</td><td>0.44</td><td>0.29</td></tr><tr><td>sh6benchN</td><td><strong>0.69</strong></td><td>1.00</td><td>22.12</td><td>0.18</td><td>10.86</td><td>0.03</td><td>4.99</td><td>1.06</td><td>0.05</td><td>0.02</td><td>0.05</td></tr><tr><td>sh8benchN</td><td><strong>0.76</strong></td><td>1.00</td><td>14.93</td><td>0.21</td><td>9.03</td><td>0.04</td><td>2.84</td><td>1.40</td><td>0.05</td><td>0.02</td><td>0.05</td></tr><tr><td>xmalloc-testN</td><td><strong>0.85</strong></td><td>1.00</td><td>10.32</td><td>0.24</td><td>5.44</td><td>0.06</td><td>2.32</td><td>3.79</td><td>0.12</td><td>0.04</td><td>0.12</td></tr><tr><td>gmean</td><td><strong>0.97</strong></td><td>1.00</td><td>3.76</td><td>1.00</td><td>2.47</td><td>0.39</td><td>1.59</td><td>0.74</td><td>0.37</td><td>0.32</td><td>0.37</td></tr><tr><td>min</td><td><strong>0.69</strong></td><td>1.00</td><td>0.99</td><td>0.15</td><td>0.30</td><td>0.03</td><td>0.71</td><td>0.06</td><td>0.04</td><td>0.02</td><td>0.04</td></tr><tr><td>max</td><td><strong>1.36</strong></td><td>1.00</td><td>58.11</td><td>11.41</td><td>41.76</td><td>1.06</td><td>6.45</td><td>3.79</td><td>1.02</td><td>1.16</td><td>1.04</td></tr></tbody></table>

**Memory Usage.** We measure the Resident Set Size (RSS), with swap disabled to get an accurate reading of the memory footprint of a running program. RSS only counts pages that are actually used, as opposed to the *virtual* memory usage that also contains reserved pages; this is what we want. We observe a wide variety of behaviors; in several cases, StarMalloc outperforms hardened_malloc, while in others, its memory footprint is larger. We posit that this variance is due to minor implementation differences. We remark that glibc's allocator, too, exhibits suboptimal behavior compared
<table><caption>Table 3. Resident Set Size (RSS) memory usage for various programs, measured against the same set of allocators as Table 2. Numbers are, as before, normalized and presented relative to `hardened_malloc`.</caption><thead><tr><th>Benchmark</th><th>st</th><th>hm</th><th>dh</th><th>ff</th><th>iso</th><th>mi-sec</th><th>mng</th><th>scudo</th><th>sg</th><th>sn-sec</th><th>glibc</th></tr></thead><tbody><tr><td>barnes</td><td><strong>0.97</strong></td><td>1.00</td><td>1.07</td><td>1.56</td><td>1.08</td><td>0.96</td><td>0.96</td><td>0.99</td><td>0.96</td><td>0.97</td><td>0.95</td></tr><tr><td>cfrac</td><td><strong>1.01</strong></td><td>1.00</td><td>1.06</td><td>35.51</td><td>2.37</td><td>0.49</td><td>0.36</td><td>0.71</td><td>0.41</td><td>0.47</td><td>0.40</td></tr><tr><td>espresso</td><td><strong>2.13</strong></td><td>1.00</td><td>0.37</td><td>1.85</td><td>2.38</td><td>0.26</td><td>0.13</td><td>0.24</td><td>0.13</td><td>0.55</td><td>0.12</td></tr><tr><td>gs</td><td><strong>1.69</strong></td><td>1.00</td><td>1.29</td><td>2.98</td><td>1.59</td><td>0.96</td><td>0.82</td><td>0.87</td><td>0.81</td><td>0.95</td><td>0.81</td></tr><tr><td>larsonN</td><td><strong>1.55</strong></td><td>1.00</td><td>1.03</td><td>2.83</td><td>1.11</td><td>1.35</td><td>0.50</td><td>0.54</td><td>1.18</td><td>2.24</td><td>1.16</td></tr><tr><td>larsonN-sized</td><td><strong>1.55</strong></td><td>1.00</td><td>1.03</td><td>2.83</td><td>1.10</td><td>1.35</td><td>0.50</td><td>0.54</td><td>1.16</td><td>2.25</td><td>1.17</td></tr><tr><td>leanN</td><td><strong>1.95</strong></td><td>1.00</td><td>1.50</td><td>8.39</td><td>2.65</td><td>1.05</td><td>0.73</td><td>0.90</td><td>0.82</td><td>1.16</td><td>0.82</td></tr><tr><td>lua</td><td><strong>1.81</strong></td><td>1.00</td><td>ERR</td><td>1.26</td><td>1.55</td><td>0.96</td><td>0.75</td><td>0.90</td><td>0.78</td><td>0.91</td><td>0.78</td></tr><tr><td>mathlib</td><td><strong>1.42</strong></td><td>1.00</td><td>ERR</td><td>2.47</td><td>4.03</td><td>0.95</td><td>0.68</td><td>0.80</td><td>0.77</td><td>0.87</td><td>0.75</td></tr><tr><td>redis</td><td><strong>0.45</strong></td><td>1.00</td><td>1.00</td><td>2.54</td><td>2.03</td><td>0.55</td><td>0.42</td><td>0.50</td><td>0.39</td><td>0.50</td><td>0.40</td></tr><tr><td>rocksdb</td><td><strong>1.60</strong></td><td>1.00</td><td>ERR</td><td>2.27</td><td>ERR</td><td>0.99</td><td>ERR</td><td>0.94</td><td>0.95</td><td>ERR</td><td>0.95</td></tr><tr><td>z3</td><td><strong>1.18</strong></td><td>1.00</td><td>0.95</td><td>2.46</td><td>1.92</td><td>0.78</td><td>0.65</td><td>0.71</td><td>0.63</td><td>0.80</td><td>0.63</td></tr><tr><td>alloc-test1</td><td><strong>0.89</strong></td><td>1.00</td><td>0.91</td><td>33.28</td><td>4.16</td><td>0.65</td><td>0.59</td><td>0.72</td><td>0.63</td><td>0.65</td><td>0.63</td></tr><tr><td>alloc-testN</td><td><strong>1.55</strong></td><td>1.00</td><td>0.42</td><td>33.16</td><td>1.10</td><td>0.65</td><td>0.30</td><td>0.36</td><td>0.35</td><td>0.45</td><td>0.35</td></tr><tr><td>cache-scratch1</td><td><strong>1.05</strong></td><td>1.00</td><td>1.23</td><td>16.26</td><td>2.31</td><td>0.85</td><td>0.81</td><td>0.86</td><td>0.81</td><td>0.85</td><td>0.78</td></tr><tr><td>cache-scratchN</td><td><strong>0.99</strong></td><td>1.00</td><td>1.22</td><td>15.83</td><td>2.27</td><td>0.86</td><td>0.77</td><td>0.85</td><td>0.82</td><td>0.84</td><td>0.79</td></tr><tr><td>cache-thrash1</td><td><strong>1.03</strong></td><td>1.00</td><td>1.20</td><td>16.08</td><td>2.31</td><td>0.85</td><td>0.80</td><td>0.84</td><td>0.80</td><td>0.84</td><td>0.78</td></tr><tr><td>cache-thrashN</td><td><strong>0.99</strong></td><td>1.00</td><td>1.21</td><td>15.92</td><td>2.30</td><td>0.84</td><td>0.83</td><td>0.84</td><td>0.83</td><td>0.85</td><td>0.78</td></tr><tr><td>glibc-simple</td><td><strong>1.26</strong></td><td>1.00</td><td>0.82</td><td>5.43</td><td>2.44</td><td>0.25</td><td>0.22</td><td>0.58</td><td>0.22</td><td>0.31</td><td>0.22</td></tr><tr><td>glibc-thread</td><td><strong>2.38</strong></td><td>1.00</td><td>0.17</td><td>0.84</td><td>0.80</td><td>0.69</td><td>0.06</td><td>0.11</td><td>0.07</td><td>1.12</td><td>0.07</td></tr><tr><td>malloc-large</td><td><strong>1.00</strong></td><td>1.00</td><td>1.01</td><td>1.18</td><td>4.63</td><td>1.39</td><td>1.00</td><td>1.00</td><td>1.30</td><td>1.64</td><td>1.30</td></tr><tr><td>mleak10</td><td><strong>0.72</strong></td><td>1.00</td><td>1.07</td><td>13.04</td><td>2.36</td><td>0.40</td><td>0.32</td><td>0.69</td><td>0.34</td><td>0.44</td><td>0.34</td></tr><tr><td>mleak100</td><td><strong>0.61</strong></td><td>1.00</td><td>0.89</td><td>55.73</td><td>2.26</td><td>0.39</td><td>0.27</td><td>0.57</td><td>0.31</td><td>0.39</td><td>0.30</td></tr><tr><td>mstressN</td><td><strong>2.04</strong></td><td>1.00</td><td>1.02</td><td>1.21</td><td>2.48</td><td>2.32</td><td>0.84</td><td>0.92</td><td>1.60</td><td>1.61</td><td>1.58</td></tr><tr><td>rbstress1</td><td><strong>0.96</strong></td><td>1.00</td><td>2.38</td><td>ERR</td><td>ERR</td><td>1.52</td><td>1.22</td><td>1.16</td><td>0.97</td><td>1.00</td><td>0.98</td></tr><tr><td>rbstressN</td><td><strong>0.80</strong></td><td>1.00</td><td>1.93</td><td>ERR</td><td>ERR</td><td>2.00</td><td>1.00</td><td>0.94</td><td>1.31</td><td>1.76</td><td>1.38</td></tr><tr><td>rptestN</td><td><strong>1.46</strong></td><td>1.00</td><td>0.95</td><td>1.17</td><td>1.18</td><td>0.95</td><td>0.41</td><td>0.44</td><td>0.47</td><td>1.21</td><td>0.52</td></tr><tr><td>sh6benchN</td><td><strong>1.05</strong></td><td>1.00</td><td>1.53</td><td>7.38</td><td>5.09</td><td>0.91</td><td>0.90</td><td>1.23</td><td>1.10</td><td>1.03</td><td>1.09</td></tr><tr><td>sh8benchN</td><td><strong>1.79</strong></td><td>1.00</td><td>1.17</td><td>1.18</td><td>2.23</td><td>1.21</td><td>0.92</td><td>0.89</td><td>1.61</td><td>1.18</td><td>1.61</td></tr><tr><td>xmalloc-testN</td><td><strong>1.98</strong></td><td>1.00</td><td>0.33</td><td>1.33</td><td>0.31</td><td>1.09</td><td>0.14</td><td>1.04</td><td>1.24</td><td>1.92</td><td>1.26</td></tr><tr><td>gmean</td><td><strong>1.24</strong></td><td>1.00</td><td>0.95</td><td>4.63</td><td>1.93</td><td>0.84</td><td>0.51</td><td>0.69</td><td>0.65</td><td>0.90</td><td>0.65</td></tr><tr><td>min</td><td><strong>0.45</strong></td><td>1.00</td><td>0.17</td><td>0.84</td><td>0.31</td><td>0.25</td><td>0.06</td><td>0.11</td><td>0.07</td><td>0.31</td><td>0.07</td></tr><tr><td>max</td><td><strong>2.38</strong></td><td>1.00</td><td>2.38</td><td>55.73</td><td>5.09</td><td>2.32</td><td>1.22</td><td>1.23</td><td>1.61</td><td>2.25</td><td>1.61</td></tr></tbody></table>

to `hardened_malloc` on several test cases, despite the absence of a quarantine mechanism, which greatly increases the memory usage; this again suggests that no design is ideal for all applications.

## 6.2 Integration into Firefox

To assess whether `StarMalloc` can be deployed as a drop-in replacement into real-world projects, we integrated it into Mozilla Firefox, raising interesting challenges: first, the replacement allocator must provide non-standard extensions of `malloc` and free [Hommey 2012]; second Firefox, and hence the underlying allocator, must work in a highly concurrent setting, supporting many threads and processes in parallel. To evaluate the user-facing impact of using `StarMalloc`, we used `JetStream2` [2022], a “benchmark suite focused on the most advanced web applications”. We integrated `Star-Malloc` with Firefox 129.0.2 and successfully ran the entire benchmark suite, demonstrating a score
overhead of 0.98x and 1.05x compared to a version compiled with `hardened_malloc` and `glibc` respectively.

We emphasize that JetStream2 does not specifically test the allocator's performance, but rather a comprehensive set of features that must be provided by modern web browsers. The successful execution of these benchmarks therefore indicates that `StarMemloc` indeed provides all the features required by the Firefox browser, while the score differences, despite not being equivalent to a performance overhead, suggest its applicability to real-world usecases.

# 7 Related Work

Verification methodologies abound for low-level programming, and given their critical aspect, memory allocators have long been considered an interesting target for low-level formal verification. We now focus on those low-level verification methodologies that have been specifically applied to allocators. Whenever possible, we highlight differences both in methodology and in verification artifact. We recall that our mixture of dependent types, separation logic, and semi-automated SMT-based verification in Steel allows us to meta-program and verify an allocator that extracts to 6.0kLoC, and features the wide array of defensive measures expect of a modern, secure allocator.

Wickerson et al. [2010] use rely-guarantee [Jones 1983], in combination with separation logic, to verify the Unix Version 7 (1979) memory manager, while reasoning about concurrency. This early memory manager consists of a linked list of *all* the blocks. Finding a free block requires linearly traversing all the blocks; block headers consists of a single memory word pointing to the next block, with the low bit encoding whether the current block is available. The verification is pen-and-paper, and as such relies on a manual encoding of that allocator into the framework.

Using the Isabelle/HOL [Nipkow et al. 2002] proof assistant, Sahebolamri et al. [2018] verify a simple sequential memory allocator where a linked list intertwined with data keeps track of allocation units. The methodology relies on AutoCorres [Greenaway et al. 2012], which takes C code and produces a higher-level monadic specification, along with a proof of correctness of the translation. Owing to the (deliberately) simplistic design, it suffices to directly establish invariants over the result of the translation, without any particular framework or proof style.

Appel and Naumann [2020] verify an array-of-bins `malloc/free` system using the Verified Software Toolchain [Appel 2011]. VST allows reasoning over a deep embedding of C in Coq, via the CompCert semantics. This allows for precise modeling of C, at the price of possibly more involved proofs. VST relies on a concurrent separation logic, but unlike Steel, does not use an SMT solver and thus relies entirely on tactics for automation. This allocator fits in 108 lines of C, is only proven correct in the sequential setting, and is intended for use with verified clients, meaning it has no defensive security mechanisms. They do, however, model resource awareness and exhaustion.

Sammler et al. [2021] verify C code using the Iris framework [Jung et al. 2018, 2015; Krebbers et al. 2017], a recent higher-order concurrent separation logic framework in Coq. An ownership discipline, applied on top of C code, allows translating C programs into Iris, and thus proving their correctness against user-provided annotations. Further properties can be derived in Coq by building upon this first layer. The authors verify a thread-safe allocator (68 C LoC), and a page allocator from a hypervisor (191 LoC). The latter is their largest case-study.

Pulte et al. [2023] propose CN, a new separation logic and refinement type system that captures almost the entire ISO C standard; the authors claim it allows reasoning about code as written by the programmer. Like us, the system mixes manual proofs with automated SMT-based reasoning. Source C code is translated into a core language, and the specification language is designed so as to make sure user-provided refinements remain in a logical fragment that can be decided via SMT. Anything outside of this fragment (including non-linear arithmetic) needs to be isolated in noninterpreted functions and reasoned about manually in Coq. Unlike us, the system does not support concurrency.
Furthermore, we leverage meta-programming to generate different variants of our implementation; it is unclear if CN would support an equivalent, C-native implementation based on macros. Their flagship example is a buddy allocator from Android's pKVM, which comprises 364 lines of C code, excluding comments; its verification required several modification to its C code.

Other works [Fang et al. 2018; Yu et al. 2003] verify *simplistic* memory allocators, but to the best of our knowledge, none verify a state-of-the-art, competitive, real-world allocator. [Zhang et al. 2019] verifies a non-trivial allocator design, but only a *specification*, not an actual implementation.

Replacing the system allocator is a challenge, and requires implementing a wide API surface (both POSIX *and* non-standard but widely used APIs) along with several advanced mechanisms for performance. Furthermore, having a security-oriented allocator requires implementing a vast amount of features, which increases the verification burden. This explains why none of the allocators we reviewed claim to act as a *drop-in* replacement for the system allocator, and study implementations that are at best an order of magnitude smaller than the code we verify.

Beyond userspace allocators, previous verification projects tackled verified operating systems and microkernels, and thus kernel space memory management [Gu et al. 2016; Mangano et al. 2016; Marti et al. 2006; Tuch et al. 2007]. Being in-kernel, these allocators have different constraints. First, kernels have many static data structures so these allocators do not hit many small heap-based allocations; second, kernels oftentimes have global locks for data structures [Peters et al. 2015], meaning concurrency isn't as much of a concern for the allocator. Furthermore, in the context of verified OS kernels like above, additional proofs ensure that the in-kernel allocator does not need to be defensive against other parts of the kernel, which means even in this context, a full-fledged defensive general-purpose security-oriented allocator was not typically the object being studied.

One last area of related work is garbage collectors (GCs). Numerous runtime systems and GCs have been studied and verified, starting with Doligez and Gonthier [1994]; Doligez and Leroy [1993], all the way to CakeML [Sandberg Ericsson et al. 2019]. While verifying a GC involves similar data structures as those of an allocator like StarMalloc, the verification challenge is different.

Zakowski et al. [2019] focus on verifying the mutator in conjunction with the allocator, and showing that the operation of the two maintains the proper invariants in a concurrent setting. The authors adopt a modular verification methodology too, but that is specifically tailored to their implementation of rely-guarantee reasoning in Coq. Like us, they proceed incrementally with multiple layers of abstraction to make verification tractable. The description of the algorithm focuses on the mark-and-sweep phases, and the only data structure mentioned in the paper is a free list for the pool of unused references. Finally, we remark that this is a non-executable specification, which does not yield or is formally linked against executable code.

Sandberg Ericsson et al. [2019] operate within CakeML, meaning that their proofs are carried in HOL4 over actual SML code. The GC of CakeML relies on a moving approach where fresh allocations within a heap rely on a bump-pointer allocator, and where compaction happens when the old heap is copied into the new heap. As such, the challenge lies more in the correctness of the traversal and reachability analysis, rather than the allocation primitive itself.

Cronburg and Guyer [2019] describe FloorPlan, a domain-specific language for describing the layout of memory management structures. FloorPlan accounts for blocks, bitmaps, linked lists, and aims to automate the generation of these memory management systems rather than having programmers write error-prone code by hand. The chief use-case is runtime systems for managed languages, but this could be repurposed for StarMalloc. FloorPlan, however, produces *unverified* Rust code, meaning it is not directly applicable. One could conceivably add a verified Steel backend for FloorPlan, or conversely, switch the verification technology to, e.g., use Aeneas [Ho and Protzenko 2022] or Verus [Lattuada et al. 2023] and directly verify the Rust code. Both remain future work.
# Data Availability

The artifact to reproduce results in this paper, including the F\* sources and generated C code as well as an experimental setup to rerun our evaluation, is available on Zenodo [Reitz et al. 2024].

# Acknowledgments

We would like to thank Daan Leiijen for clarifications about many parts of mimalloc and mimalloc-bench, Matthew Parkinson for discussions about allocators security mechanisms, and Tim Bourke for valuable feedback about earlier versions of this paper.

# References

* Andrew W. Appel. 2011. Verified Software Toolchain. In *Proceedings of the European Conference on Programming Languages and Systems (ESOP)*. https://doi.org/10.1007/978-3-642-19718-5_1

* Andrew W Appel and David A Naumann. 2020. Verified sequential malloc/free. In *Proceedings of the International Symposium on Memory Management (ISMM)*. https://doi.org/10.1145/3381898.3397211

* Apple Security Research. 2022. Towards the next generation of XNU memory safety: kalloc_type. https://security.apple.com/blog/towards-the-next-generation-of-xnu-memory-safety/.

* Emery D. Berger. 2012. Software Needs Seatbelts and Airbags: Finding and Fixing Bugs in Deployed Software is Difficult and Time-Consuming. Here Are Some Alternatives. *Commun. ACM* (2012). https://doi.org/10.1145/2330667.2330683

* Emery D. Berger and Benjamin G. Zorn. 2006. DieHard: Probabilistic Memory Safety for Unsafe Languages. In *Proceedings of the Conference on Programming Language Design and Implementation (PLDI)*. https://doi.org/10.1145/1133255.1134000

* Jay Bosamiya, Wen Shih Lim, and Bryan Parno. 2022. Provably-Safe Multilingual Software Sandboxing using WebAssembly. In *Proceedings of the USENIX Security Symposium*.

* Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. *Journal of Functional Programming* 23 (9 2013), 552–593. Issue 05. https://doi.org/10.1017/S095679681300018X

* Jacob Bramley, Dejice Jacob, Andrei Lascu, Jeremy Singer, and Laurence Tratt. 2023. Picking a CHERI Allocator: Security and Performance Considerations. In *Proceedings of the International Symposium on Memory Management (ISMM)*. https://doi.org/10.1145/3591195.3595278

* Stephen Brookes. 2007. A Semantics for Concurrent Separation Logic. In *Theoretical Computer Science (TCS)*. https://doi.org/10.1016/j.tcs.2006.12.034

* The Chromium Project. 2020. Memory Safety. https://www.chromium.org/Home/chromium-security/memory-safety/.

* Karl Cronburg and Samuel Z Guyer. 2019. Floorplan: spatial layout in memory management systems. In *Proceedings of the 18th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences*. 81–93. https://doi.org/10.1145/3357765.3359519

* Martin De Boer, Stijn De Gouw, Jonas Klamroth, Christian Jung, Mattias Ulbrich, and Alexander Weigl. 2023. Formal Specification and Verification of JDK’s Identity Hash Map Implementation. *Formal Aspects of Computing* 35, 3 (2023). https://doi.org/10.1145/3594729

* Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In *Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)*. https://doi.org/10.1007/978-3-540-78800-3_24

* Damien Doligez and Georges Gonthier. 1994. Portable, unobtrusive garbage collection for multiprocessor systems. In *Proceedings of the ACM Symposium on Principles of Programming Languages (POPL)*. https://doi.org/10.1145/174675.174673

* Damien Doligez and Xavier Leroy. 1993. A concurrent, generational garbage collector for a multithreaded implementation of ML. In *Proceedings of the ACM Symposium on Principles of Programming Languages (POPL)*. https://doi.org/10.1145/158511.158611

* Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. 2017. A Metaprogramming Framework for Formal Verification. In *Proceedings of the International Conference on Functional Programming (ICFP)*. https://doi.org/10.1145/3110278

* Márton Erdős, Sam Ainsworth, and Timothy M Jones. 2022. MineSweeper: a “clean sweep” for drop-in use-after-free prevention. In *Proceedings of the International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)*. https://doi.org/10.1145/3503222.3507712

* Bin Fang, Mihaela Sighireanu, Geguang Pu, Wen Su, Jean-Raymond Abrial, Mengfei Yang, and Lei Qiao. 2018. Formal modelling of list based dynamic memory allocators. *Science China Information Sciences* 61 (2018), 1–16. https://doi.org/10.1007/s11432-017-9280-9

* Rich Felker. 2020. Comparison between hardened_malloc and musl mallocs. https://www.openwall.com/lists/musl/2020/05/13/1.
Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux, and Tahina Ramananandro. 2021. Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic. In *Proceedings of the International Conference on Functional Programming (ICFP)*. https://doi.org/10.1145/3473590

GitHub Team. 2023. The top programming languages. https://octoverse.github.com/2022/top-programming-languages
glibc. 2017a. Bug 22343 (CVE-2018-6485) - Integer overflow in posix_memalign (CVE-2018-6485). https://sourceware.org/bugzilla/show_bug.cgi?id=22343.

glibc. 2017b. Bug 22375 (CVE-2017-17426) - malloc returns pointer from tcache_get when should return NULL (CVE-2017-17426). https://sourceware.org/bugzilla/show_bug.cgi?id=22375.

glibc. 2020. Bug 26306 - Confusion in malloc.c about the fastbins size check. https://sourceware.org/bugzilla/show_bug.cgi?id=26306.

Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey. 2023. Mostly Automated Proof Repair for Verified Libraries. In *Proceedings of the Conference on Programming Language Design and Implementation (PLDI)*. https://doi.org/10.1145/3591221

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv. 2007. Local Reasoning for Storable Locks and Threads. In *Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS)*. https://doi.org/10.1007/978-3-540-76637-7_3

GrapheneOS Development Team. 2021. hardened_malloc - GrapheneOS's hardened memory allocator. https://github.com/GrapheneOS/hardened_malloc/blob/main/README.md#security-properties.

David Greenaway, June Andronick, and Gerwin Klein. 2012. Bridging the gap: Automatic verified abstraction of C. In *Proceedings of the International Conference on Interactive Theorem Proving (ITP)*. Springer, 99–115. https://doi.org/10.1007/978-3-642-32347-8_8

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In *Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI)*.

The HFT guy. 2020. Major Bug in glibc is Killing Applications With a Memory Limit. https://thehftguy.com/2020/05/21/major-bug-in-glibc-is-killing-applications-with-a-memory-limit/.

Son Ho, Aymeric Fromherz, and Jonathan Protzenko. 2023. Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification. In *Proceedings of the International Conference on Functional Programming (ICFP)*. https://doi.org/10.1145/3607844

Son Ho and Jonathan Protzenko. 2022. Aeneas: Rust verification by functional translation. *Proceedings of the ACM on Programming Languages* 6, ICFP (2022), 711–741. https://doi.org/10.1145/3547647

Son Ho, Jonathan Protzenko, Abhishek Bichhawat, and Karthikeyan Bhargavan. 2022. Noise*: A library of verified high-performance secure channel protocol implementations. In *Proceedings of the IEEE Symposium on Security and Privacy (S&P)*. https://doi.org/10.1109/SP46214.2022.9833621

Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. 2008. Oracle Semantics for Concurrent Separation Logic. In *Proceedings of the European Conference on Programming Languages and Systems (ESOP)*. https://doi.org/10.1007/978-3-540-78739-6_27

Mike Hommey. 2012. Hooking the memory allocator in Firefox. https://glandium.org/blog/?p=2848.

Samin S. Ishtiaq and Peter W. O'Hearn. 2001. BI as an Assertion Language for Mutable Data Structures. In *Proceedings of the ACM Symposium on Principles of Programming Languages (POPL)*. https://doi.org/10.1145/360204.375719

ISO. 1999. ISO/IEC 9899:1999 C standard. https://www.openstd.org/jtc1/sc22/wg14/www/docs/n1256.pdf.

Jonas Braband Jensen and Lars Birkedal. 2012. Fictional separation logic. In *Proceedings of the European Conference on Programming Languages and Systems (ESOP)*. https://doi.org/10.1007/978-3-642-28869-2_19

JetStream2. 2022. JetStream 2.1 In-Depth Analysis. https://browserbench.org/JetStream/in-depth.html.

Cliff B. Jones. 1983. Tentative steps toward a development method for interfering programs. In *ACM Transactions on Programming Languages and Systems (TOPLAS)*. https://doi.org/10.1145/69575.69577

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. *Journal of Functional Programming* 28 (2018). https://doi.org/10.1017/S0956796818000151

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In *Proceedings of the ACM Symposium on Principles of Programming Languages (POPL)*. https://doi.org/10.1145/2775051.2676980

Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In *Proceedings of the European Conference on Programming Languages and Systems (ESOP)*. https://doi.org/10.1007/978-3-662-54434-1_26

Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types. In *Proceedings of the ACM SIGPLAN Conference*
on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). https://doi.org/10.1145/3586037

Daan Leijen, Julien Voisin, and Matthew Parkinson. 2018. mimalloc-bench – Suite for benchmarking malloc implementation. https://github.com/daanx/mimalloc-bench.

Daan Leijen, Benjamin Zorn, and Leonardo de Moura. 2019. Mimalloc: Free list sharding in action. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS). https://doi.org/10.1007/978-3-030-34175-6_13

K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). https://doi.org/10.1007/978-3-642-17511-4_20

Ruihao Li, Qinzhe Wu, Krishna Kavi, Gayatri Mehta, Neeraja J Yadwadkar, and Lizy K John. 2023. NextGen-Malloc: Giving Memory Allocator Its Own Room in the House. In Proceedings of the USENIX Workshop on Hot Topics in Operating Systems (HotOS). https://doi.org/10.1145/3593856.3595911

Paul Liétar, Theodore Butler, Sylvan Clebsch, Sophia Drossopoulou, Juliana Franco, Matthew J. Parkinson, Alex Shamis, Christoph M. Wintersteiger, and David Chisnall. 2019. Smalloc: A Message Passing LOCATOR. In Proceedings of the 2019 ACM SIGPLAN International Symposium on Memory Management (Phoenix, AZ, USA) (ISMM 2019). Association for Computing Machinery, New York, NY, USA, 122–135. https://doi.org/10.1145/3315573.3329980

Zhenpeng Lin, Zheng Yu, Ziyi Guo, Simone Campanoni, Peter Dinda, and Xinyu Xing. 2024. CAMP: Compiler and Allocator-based Heap Memory Protection. In Proceedings of the USENIX Security Symposium.

Beichen Liu, Pierre Olivier, and Binoy Ravindran. 2019. Slimguard: A secure and memory-efficient heap allocator. In Proceedings of the ACM/IFIP/USENIX International Middleware Conference. https://doi.org/10.1145/3361525.3361532

LLVM Project. 2023. Scudo Hardened Allocator. https://llvm.org/docs/ScudoHardened Allocator.html.

Frédéric Mangano, Simon Duquennoy, and Nikolai Kosmatov. 2016. Formal verification of a memory allocation module of Contiki with Frama-C: a case study. In Proceedings of the International Conference on Risks and Security of Internet and Systems (CRIIS). https://doi.org/10.1007/978-3-319-54876-0_9

Nicolas Marti, Reynald Affeldt, Akinori Yonezawa, and Department Of Computer Science. 2006. Formal Verification of the Heap Manager of an Operating System using Separation Logic. In Proceedings of the International Conference on Formal Engineering Methods (ICFEM). https://doi.org/10.1007/11901433_22

Guido Martinez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy. 2019. Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms. In Proceedings of the European Conference on Programming Languages and Systems (ESOP). https://doi.org/10.1007/978-3-030-17184-1_2

MSRC Team. 2021. BadAlloc – Memory allocation vulnerabilities could affect wide range of IoT and OT devices in industrial, medical, and enterprise networks. https://msrc-blog.microsoft.com/2021/04/29/badalloc-memory-allocation-vulnerabilities-could-affect-wide-range-of-iot-and-ot-devices-in-industrial-medical-and-enterprise-networks/.

The MSRC Team. 2019. A Proactive Approach to More Secure Code. https://msrc.microsoft.com/blog/2019/07/a-proactive-approach-to-more-secure-code/.

Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2016. Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. In Proceedings of the International Conference on Computer Aided Verification (CAV). https://doi.org/10.1007/978-3-319-41528-4_22

MySQL. 2019. Bug #94647 - Memory leak in MEMORY table by glibc. https://bugs.mysql.com/bug.php?id=94647.

Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer. https://doi.org/10.1007/3-540-45949-9

Gene Novark and Emery D Berger. 2010. DieHarder: securing the heap. In Proceedings of the ACM Conference on Computer and Communications Security (CCS). https://doi.org/10.1145/1866307.1866371

Peter W. O'Hearn. 2007. Resources, Concurrency, and Local Reasoning. In Theoretical Computer Science (TCS). https://doi.org/10.1016/j.tcs.2006.12.035

Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs That Alter Data Structures. In Proceedings of the International Workshop on Computer Science Logic (CSL). https://doi.org/10.1007/3-540-44802-0_1

Matthew J. Parkinson and Alexander J. Summers. 2012. The Relationship Between Separation Logic and Implicit Dynamic Frames. Logical Methods in Computer Science (2012). https://doi.org/10.2168/LMCS-8(3:1)2012

Sean Peters, Adrian Danis, Kevin Elphinstone, and Gernot Heiser. 2015. For a microkernel, a big lock is fine. In Proceedings of the Asia-Pacific Workshop on Systems (APSys). https://doi.org/10.1145/2797022.2797042

Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, and Santiago Zanella-Béguelin. 2020. HACLxN: Verified Generic SIMD Crypto (for All Your Favourite Platforms). In Proceedings of the ACM Conference on Computer and Communications Security (CCS). https://doi.org/10.145/3372297.3423352

Red Hat Customer Portal. 2013. CVE-2013-4332. https://access.redhat.com/security/cve/cve-2013-4332.

François Pottier. 2017. Verifying a Hash Table and Its Iterators in Higher-Order Separation Logic. In Proceedings of the International Conference on Certified Programs and Proofs (CPP). https://doi.org/10.1145/3018610.3018624
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, and Santiago Zanella-Béguelin. 2020. EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. In Proceedings of the IEEE Symposium on Security and Privacy (S&P). https://doi.org/10.1109/SP40000.2020.00114

Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. 2017. Verified Low-Level Programming Embedded in F*. In Proceedings of the International Conference on Functional Programming (ICFP). https://doi.org/10.1145/3110261

Christopher Pulte, Dhruv C Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami. 2023. CN: Verifying Systems C Code with Separation-Logic Refinement Types. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL). https://doi.org/10.1145/3571194

Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In Proceedings of the USENIX Security Symposium.

Aseem Rastogi, Guido Martínez, Aymeric Fromherz, Tahina Ramananandro, and Nikhil Swamy. 2021. Programming and Proving with Indexed Effects. Technical Report. https://www.fstar-lang.org/papers/indexedeffects/.

Antonin Reitz, Aymeric Fromherz, and Jonathan Protzenko. 2024. Artifact for OOPSLA 2024 paper: StarMalloc: Verifying a Modern, Hardened Memory Allocator. https://doi.org/10.5281/zenodo.12670476

John Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Proceedings of the IEEE Symposium on Logic in Computer Science (LICS). https://doi.org/10.1109/LICS.2002.1029817

Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock, et al. 2019. QED at large: A survey of engineering of formally verified software. Foundations and Trends® in Programming Languages 5, 2-3 (2019), 102–281. https://doi.org/10.1561/2500000045

Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. 2018. Adapting proof automation to adapt proofs. In Proceedings of the International Conference on Certified Programs and Proofs (CPP). https://doi.org/10.1145/3167094

Chris Rohlf. 2020. Isolation Alloc. https://struct.github.io/iso_alloc.html.

Arash Sahebolamri, Scott D Constable, and Steve J Chapin. 2018. A Formally Verified Heap Locator. Electrical Engineering and Computer Science - Technical Reports (2018). https://surface.syr.edu/eecs_techreports/182.

Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. 2021. RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI). https://doi.org/10.1145/3453483.3454036

Adam Sandberg Ericsson, Magnus O Myreen, and Johannes Åman Pohjola. 2019. A verified generational garbage collector for CakeML. Journal of Automated Reasoning 63 (2019), 463–488. https://doi.org/10.1007/s10817-018-9487-z

Thibaut Sautereau. 2021. Undefined behavior in get_large_size_class(). https://github.com/GrapheneOS/hardened_malloc/isues/133.

Sam Silvestro, Hongyu Liu, Corey Crosser, Zhiqiang Lin, and Tongping Liu. 2017. FreeGuard: A Faster Secure Heap Locater. In Proceedings of the ACM Conference on Computer and Communications Security (CCS). https://doi.org/10.1145/3133956.3133957

Sam Silvestro, Hongyu Liu, Tianyi Liu, Zhiqiang Lin, and Tongping Liu. 2018. Guarder: A Tunable Secure Locater. In Proceedings of the USENIX Security Symposium.

Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL). https://doi.org/10.1145/2837614.2837655

Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, and Arti Gupta. 2022. Hardening attack surfaces with formally proven binary format parsers. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI). https://doi.org/10.1145/3519939.3523708

Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and Guido Martínez. 2020. SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs. In Proceedings of the International Conference on Functional Programming (ICFP). https://doi.org/10.1145/3409003

Laszlo Szekeres, Mathias Payer, Tao Wei, and Dawn Song. 2013. SoK: Eternal War in Memory. In Proceedings of the IEEE Symposium on Security and Privacy (S&P). https://doi.org/10.1109/SP.2013.13

Harvey Tuch, Gerwin Klein, and Michael Norrish. 2007. Types, Bytes, and Separation Logic. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL). https://doi.org/10.1145/1190215.1190234
John Wickerson, Mike Dodds, and Matthew Parkinson. 2010. Explicit stabilisation for modular rely-guarantee reasoning. In *Proceedings of the European Conference on Programming Languages and Systems (ESOP)*. https://doi.org/10.1007/978-3-642-11957-6_32

Brian Wickman, Hong Hu, Insu Yun, DaeHee Jang, JungWon Lim, Sanidhya Kashyap, and Taesoo Kim. 2021. Preventing Use-After-Free Attacks with Fast Forward Allocation. In *Proceedings of the USENIX Security Symposium*.

Paul R. Wilson, Mark S. Johnstone, Michael Neely, and David Boles. 1995. Dynamic storage allocation: A survey and critical review. In *Proceedings of the International Workshop on Memory Management (IWMM)*. https://doi.org/10.1007/3-540-60368-9_19

Dachuan Yu, Nadeem A Hamid, and Zhong Shao. 2003. Building certified libraries for PCC: Dynamic storage allocation. In *Proceedings of the European Conference on Programming Languages and Systems (ESOP)*. https://doi.org/10.1007/3-540-36575-3_25

Insu Yun, Woosun Song, Seunggi Min, and Taesoo Kim. 2021. HardsHeap: a universal and extensible framework for evaluating secure allocators. In *Proceedings of the ACM Conference on Computer and Communications Security (CCS)*. https://doi.org/10.1145/3460120.3484740

Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, and Jan Vitek. 2019. Verifying a concurrent garbage collector with a rely-guarantee methodology. *Journal of Automated Reasoning* 63 (2019), 489–515. https://doi.org/10.1007/s10817-018-9489-x

Yu Zhang, Yongwang Zhao, David Sanan, Lei Qiao, and Jinkun Zhang. 2019. A verified specification of TLSF memory management allocator using state monads. In *Proceedings of the International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA)*. https://doi.org/10.1007/978-3-030-35540-1_8

Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn Heule, and Bryan Parno. 2023. Mariposa: Measuring SMT Instability in Automated Program Verification. In *Proceedings of the Conference on Formal Methods in Computer-Aided Design (FMCAD)*. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_26

Received 2024-04-06; accepted 2024-08-18