RayNu-V: A Formally Verified Bare-Metal Hypervisor

Abstract

[To be written at M3/M4 checkpoint. Placeholder only.]

RayNu-V is a clean-slate Type-1 bare-metal hypervisor written in Rust and optimized for Dell PowerEdge servers. Its security-critical path (VMX, EPT, physical frame allocator, and related control planes) is designed for formal verification with Verus and Kani. This paper reports the progressive verification of the Proven Core, culminating in a machine-checked proof of the EPT Isolation Theorem: every valid guest-physical to host-physical mapping is exclusively owned by a single guest and belongs to neither the hypervisor nor any other guest.

Keywords: formal verification, Type-1 hypervisor, EPT, Verus, Kani, bare-metal, Dell PowerEdge

1. Introduction

[Static until early content is ready.]

Motivation, problem statement, the four pillars ([V], [Z], [D], [A]), and the decision to treat formal verification as an architectural north star rather than a post-hoc exercise.

2. Background and Threat Model

• Existing Type-1 hypervisors and their verification status (or lack thereof).
• Why memory isolation is the headline property.
• Threat model: malicious or compromised guest, buggy device emulation outside the Proven Core, operator error.
• Assumptions that the proofs rely on (and that are therefore out of scope).

3. System Architecture

3.1 Proven Core Boundary (ADR-002)

Only the following modules receive Verus specifications and progressive proofs. Everything else is verified by Rust’s type system, testing, and code review only.

Hard limit: 15,000 LOC including ~1,600 LOC of proof scaffolding.

3.2 Single-Binary Strategy (ADR-003)

One .efi binary. All assets (kernel, initrd, Web UI, schemas) embedded and zstd-compressed. Target size 15 MB, hard limit 20 MB. Non-critical assets are lazy-decompressed.

3.3 Hardware Focus

Dell PowerEdge R640 / R650 / R660. Tier-1 iDRAC/Redfish integration is in scope; Tier-2 (PERC deep health, predictive failure) is best-effort and requires partnership.

4. Formal Verification Approach

4.1 Toolchain (ADR-001, ADR-008)

• Verus — primary tool for functional correctness (SMT).
• Kani — bounded model checking of every unsafe block.
• Fallback chain: Verus → Kani → runtime assertions + fuzzing. The architecture is always designed for Level 3 even when tooling is not yet ready.

4.2 Verification Maturity Model (ADR-006)

Runtime assertions are retained even at L3 (defense-in-depth).

4.3 File Convention for Proven Core Modules

module/
├── module.rs           # executable code
├── module_spec.rs      # Verus specifications
├── module_proof.rs     # Verus proofs (gaps marked TODO)
└── module_test.rs      # Kani + unit + fuzz

5. The EPT Isolation Theorem (ADR-004)

For every valid EPT mapping from a guest-physical address to a host-physical frame, that frame is exclusively owned by the mapping guest and belongs to neither the hypervisor nor any other guest.

“Exclusively owned” = exactly one guest holds a mapping to that frame at any moment. “Belongs to neither” = the frame is absent from the hypervisor’s page tables and from every other guest’s EPT.

The theorem must hold across map, unmap, EPT-violation handling, and (later) live-migration page transfer.

5.1 Proof Progression (living)

6. Progressive Evaluation — Milestone Log

This section is filled only with contemporaneous evidence from real runs.

6.1 Milestone 0 — “It Boots”

Status: Not yet started on this living page
Target gate: Boots on R640 (or QEMU+OVMF), serial console works, Verus CI pipeline green.

6.2 Milestone 1 — “VMX Works”

Status: Not yet started on this living page
Target gate: VMLAUNCH / VMEXIT cycle, VMCS host/guest state configured, first L3 proofs on VMCS legality.

6.3 Milestone 2 — “Guest Executes Real Code”

Status: Not yet started on this living page
Target gate: EPT spec (L2), physical allocator at L3, guest code runs under EPT.

6.4 Milestone 3 — “Linux Boots”

Status: Not yet started on this living page
Target gate: Unmodified Linux 6.x reaches a shell. Verification checkpoint report published.

6.5 Milestone 4 — “Usable VM Platform”

Status: Not yet started on this living page
Target gate: ≥4 Linux VMs with SMP, storage, networking. EPT Isolation Theorem at L3 for 4K pages across N guests.

6.6 Milestone 5 / 5.5 / 6

(Sections reserved; content added only when the corresponding gates are passed.)

7. Related Work

[To be filled later with precise citations.]

Existing formally verified or heavily verified hypervisors / kernels (seL4, CertiKOS, Komodo, Firecracker verification efforts, etc.). Differences in scope, threat model, and hardware target.

8. Limitations and Open Proofs

• Large-page EPT and NUMA-aware allocation may remain at L2 for the initial public release.
• Live-migration path is a late L3 target (M6).
• Device emulation, scheduler algorithms, and the VMware migration engine are deliberately outside the Proven Core and are not claimed to be formally verified.
• Verus / Rust toolchain evolution can break existing proofs (see ADR-008); a quarterly maintenance budget is allocated.

Any L2-only modules at the time of a public snapshot will be listed here with an explicit statement of the residual risk and the runtime-enforcement measures that remain in place.

9. Conclusion

[Written only when the work has reached a stable, externally reviewable state.]