Proof Target: bitmap-allocator, which is a Bitmap-based allocator employs a multi-level bitmap structure to achieve efficient management of large-scale memory space.
In a Type-I Hypervisor, the memory allocator is responsible for assigning non-overlapping physical page ranges to different VMs. It collaborates with the page table to achieve strong isolation and verifiable security:
- Disjointness: At any time, allocated intervals must be non-overlapping.
- Availability: If there exists a sufficiently large contiguous free region, the allocator must be able to locate and return it.
- Reclaimability: Once released, an interval must return to the free set.
- Hierarchy Consistency: The parent-level bitmap must correspond exactly to the views of its child allocators.
The page table enforces access control, while the allocator ensures non-overlapping intervals and resource scheduling. Together, they form the foundation of memory isolation in virtual machines, as shown in the following figure.
The following figure illustrates the tree-like structure of bitmap-allocator. It's each layer manages an address space 16 times larger than the next layer below it.
We divide the verification into three layers:
- The first layer includes several non-standard library functions that are invoked.
- The second layer is BitAlloc16, which serves as the leaf-node layer.
- The third layer is BitAllocCascade16, forming a complete 16-ary tree.