Formal Verification of a Memory Allocator for Rust Hypervisors: From Verified to Deployable Code with Functional Equivalence Guarantees

Abstract

Bugs in hypervisor memory management may lead to double allocation, physical aliasing, or violations of inter-VM isolation. This paper studies BitAllocCascade16, a bitmap-based frame allocator used on real hypervisors implemented in Rust. We use Verus to formally verify the allocator, proving its structural invariants and functional correctness. In the process, we uncover and fix a shift-operation overflow bug in the original implementation. Source-level verification often requires proof-oriented refactoring, which may cause the verified implementation to diverge from the original deployable code in structure, interface, and performance characteristics. To address this integration gap, we formulate the relation between the verified and original programs as a functional equivalence problem, and introduce Veri-easy, a lightweight and automated framework for establishing such equivalence. Guided by performance analysis, we further derive a final implementation and qualify it against the verified version. Our results show that the verified allocator faithfully matches the behavior of the original, and that the final implementation can be integrated into hvisor and HyperEnclave without compromising correctness or performance.