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: Closed on Latitude/QEMU; closed on real PowerEdge R640 (2026-08-15).
Target gate: Boots on R640 (or QEMU+OVMF), serial console works, Verus CI pipeline green.

6.2 Milestone 1 — “VMX Works”

Status: Closed on Latitude; reproduced on R640 iron.
Target gate: VMLAUNCH / VMEXIT cycle, VMCS host/guest state configured.

6.3 Milestone 2 — “Guest Executes Real Code”

Status: Closed on Latitude; reproduced on R640 iron.
Target gate: Guest code runs under EPT; timer/IRQ inject path.

6.4 Milestone 3 — “Linux Boots”

Status: Closed on Latitude; closed on R640 iron (RAYNU-V-M3-SHELL-OK).
Target gate: Unmodified Linux 6.x reaches a shell (init SHELL hypercall).

6.5 Milestone 4 — “Usable VM Platform”

Status: Closed on Latitude (M4.0–M4.9); M4.0–M4.5 probe chain on R640 iron.
Target gate: ≥4 concurrent guests under credit scheduler; virtio-blk/net + SMP probes.

6.6 Milestone 5 / 5.5 / 6

Status (Latitude/CI): M5–M6.9 closed (RAYNU-V-M6-EXT-OK; 80 verified, 0 errors). Iron: E2 BOOT-OK, E3 UEFI-HTTP-OK, E5 stamp persist (RAYNU-V-M7-ISO-BOOTED-FROM-DISK, 2026-08-16). Residual after Everest: TLS/console + leftover persist are M8 (E3b + Phase F closed 2026-08-20; E4 SPA VMLAUNCH closed 2026-08-21; E5 + Phase B closed 2026-09-10/11) — see HDA.

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 / NUMA: Latitude closed L3 gates (M5.7 / M6.2); iron path not re-proven beyond M4.5 probes.
• Live-migration page-transfer L3 closed on Latitude (M6.3); live vCenter product migrate remains polish.
• 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.
• Mount Everest: CLOSED on iron 2026-09-11 (f72b4276 / 34552377351) — SPA Start of RayNu-F → RAYNU-V-M7-ISO-INSTALL-OK → RAYNU-V-RAYNU-F-DISK-BOOT-OK → root=UUID= → login. Rollback kit: GitHub Latest v0.1.0-everest-closed (EFI SHA256 e74460ff0e248a06d2e4ab546684d1006edd25855f50c8dc27dc202facab9cbc). LBA stamps ≠ this close. Firmware SNP/Tcp4 stay dead after EBS. TLS / leftover persist / console UI are M8 (ADR-018), not a reopened Everest. Cluster is M9.

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.]