svsm: Instructions file for Codex

Introduction

SVSM is an in-guest paravisor written in Rust and designed for secure virtualization environments, primarily AMD SEV-SNP and Intel TDX. It operates at the highest privilege level within the Confidential Virtual Machine (VMPL0 on SEV-SNP).

Directory structure

The SVSM runs on bare metal as a ring-0 kernel, with optional userspace components. Important directories:

• kernel/: main SVSM kernel
• boot/: kernel bootloader and definitions
• syscall/: SVSM kernel/userspace system call definitions
• user/: SVSM userspace library and example init process
• tools/: general tools

Building and testing

The SVSM project is organized as a cargo workspace. Some workspace members are built with the host toolchain and others are built for bare metal. Running cargo build or cargo test will not necessarily work.

• Build: use make.
• Test: use make test for unit tests. Read Documentation/docs/developer/TESTING.md.
• Linter: run make clippy.
• Format checks: cargo fmt --check works as usual.

All of the above must run cleanly after making a set of changes. Additionally, all unsafe blocks must have a SAFETY comment detailing why the code is safe and/or what invariants are assumed.

Additional code documentation guidelines can be found at Documentation/docs/developer/RUSTDOC-GUIDELINES.md.

Build recipes

The project uses custom build tools to generate an image that may be loaded by the hypervisor. The top-level orchestrator is the xbuild tool, which is called from the Makefile. The recipes are located in configs/. Information about the build recipe format can be found in Documentation/docs/installation/BUILD_RECIPES.md.

IGVM

IGVM is the image format that the build system generates and that the host VMM accepts. It describes the memory contents of the guest at startup. The SVSM generates the IGVM image via tools/igvmbuilder, which is orchestrated by xbuild.

Formal verification with Verus

This repository integrates formal verification using Verus.

• Verified source files end with *.verus.rs or *.proof.verus.rs (e.g., address.verus.rs, alloc_perms.verus.rs).
• Verification Invariants: Never bypass, alter, or strip #![cfg_attr(verus_keep_ghost, ...)] blocks or Verus ghost specifications unless specifically instructed. Any structural change to a verified module requires re-verification by executing the Verus toolchain.
• If a compiler flag or configuration change is made, ensure the verus or verus_all feature configurations in Cargo.toml remain valid.
• Do not run any verification checks unless specifically asked OR if related code was updated.
• Usage documentation is found in Documentation/docs/developer/VERIFICATION.md.