Verifying a Memory Allocator for Rust

Abstract

Rust is used in systems software for its type-based memory-safety guarantees. With dynamic allocation, however, these guarantees also depend on the correctness of the underlying allocator. This paper focuses on rlsf, an existing Rust allocator based on the Two-Level Segregated Fit (TLSF) algorithm. rlsf provides predictable allocation and deallocation time through the algorithmic design of TLSF and low-level implementation optimizations. We verify the existing rlsf implementation in Verus, a verifier for Rust, against the allocator-level behavior required by Rust’s allocation interface. Rather than redesigning the allocator for verification, we structure the proof around the existing TLSF-based implementation. First, we formalize the algorithm-level invariants governing how TLSF organizes free blocks. Second, we verify the implementation against these invariants, using bit-level reasoning for computing free-list indices and bitmap bookkeeping, as well as permission-based reasoning for free-list pointer operations. Through this proof, we obtain a verified implementation while preserving the original design of rlsf.