Formal Verification of Asterinas OSTD with Verus

The vostd project provides a formally-verified version of OSTD, the (unofficial) standard library for OS development in safe Rust. OSTD encapsulates low-level hardware interactions—which requires using unsafe Rust—into a small yet powerful set of high-level, safe abstractions. These abstractions enable the creation of complex, general-purpose OSes like Asterinas entirely in safe Rust.

By design, OSTD guarantees soundness: no undefined behavior is possible, regardless of how its API is used in safe Rust. The goal of the vostd project is to bolster confidence in this soundness through formal verification, leveraging the Verus verification tool.

This work is ongoing. Our current focus is on verifying OSTD’s memory management subsystem, a core component that is directly related to kernel memory safety. As we continue, we aim to extend formal verification to additional parts of OSTD to further ensure its reliability and correctness.

Project Structure

Implementation code from the OSTD mainline, together with its accompanying proofs, resides in the ostd/src directory, while specifications are located under ostd/specs.

This repository currently contains verification code for ostd/src/mm and ostd/src/sync. It is independent of the concurrency proofs presented in our SOSP paper — “CortenMM: Efficient Memory Management with Strong Correctness Guarantees.” For the SOSP artifact, please refer to the func-correct branch for verification code, and to this repo for the complete artifact.

A merge of these efforts is planned, but has not yet begun.

Building the Proof Development

Install Rust

If you have not installed Rust yet, follow the official instructions.

Clone Submodule

vostd relies on our custom build tool. Please run:

git submodule update --init --recursive

Build Verus

The recommended way to build Verus is by running the following command:

make verus

or

cargo dv bootstrap

Verus should be automatically cloned and built in the tools directory. If download fails, please clone the repo manually into tools/verus , then run cargo dv bootstrap again.

Note

We use our own fork of Verus, which we continuously synchronize with the upstream repository. You may choose to install the upstream Verus source via cargo dv bootstrap --upstream-verus, however, we cannot guarantee that it will always verify successfully with our project. That said, our CI continuously tests against upstream, and we typically resolve any breaking changes within about a week.

If you have already installed Verus elsewhere and just want to reproduce the verification result, a quick alternative is to set CARGO_VERUS_PATH to the directory containing the cargo-verus binary, or add it to your PATH. Then run cargo verus verify.

Build Verification Targets

To verify the entire project, simply run:

make

or

cargo dv verify

To verify only ostd and skip its dependencies, run:

cargo dv verify -f --targets ostd

The ostd crate relies on a verified crate: vstd_extra. To verify it independently, run:

cargo dv verify --targets vstd_extra

Clean Build Artifacts

Recompilation and reverification are automatically skipped for crates that have not changed since the last build. To remove the build artifact for a fresh build, run:

make clean

or

cargo dv clean

Documentation

We provide comprehensive API-level documentation that describes the verified APIs along with their specifications. To generate the documentation, run:

make doc

or

cargo dv build
cargo dv doc --target ostd

The generated documentation can be found at doc/index.html. An online version is also available.

IDE Support

For VSCode users, the verus-analyzer extension is available in the Marketplace.

For Emacs users, please refer to the verus-mode.

Contributing to VOSTD

We welcome your contributions!

Common Conventions

• We add an axiom_ prefix to the name of each axiom fn and a lemma_ prefix to each proof fn.
• We prefer associated functions to isolated lemmas.
• Specifications and lemmas are preferred to be add to ostd/specs.
• General definitions and lemmas should be add to verified_libs/vstd_extra.

Tips

• During your development process, please frequently run make verus-upgrade or cargo dv bootstrap --upgrade to stay up-to-date with the latest supported version of Verus.
• Format checking is enforced, please format your code with cargo dv fmt before submission.
• If you are contributing to Verus, we recommend submitting pull requests to the upstream repo rather than our fork, since we aim to minimize differences between them.