Formal Verification of Systems Software

Setting up Verus

Verus is under active development, with rolling releases. To ensure that all students get a consistent experience we will be using a separate release for the course, with associated documentation.
There are two options, listed below: setting up Verus natively (which requires installing rust on your system) or running Verus in an `x86_64` Docker container.

Option A: Download Verus release and install rust toolchain (if necessary)

To get Verus, download the relevant package from this release page: https://github.com/principled-systems/verus/releases/tag/release%2Frolling%2F0.2024.10.25.2362f8a

If you're on MacOS the binaries and libraries will be quarantined by Gatekeeper, which will pop up a number of messages about running software downloaded from the internet. To avoid this issue, once you have unpacked the `zip` file, open a shell in the newly unzipped directory and run `bash macos_allow_gatekeeper.sh`, which will remove the Gatekeeper quarantine flag from all the relevant files (you can inspect the file first, if you'd like, it only makes changes inside the directory you just unpacked).

You can then run Verus with ./verus (or .\verus.exe on Windows). If you already have `rustup` installed, `verus` will instruct you on how to install the necessary rust toolchain (1.76.0). If you don't have `rustup` installed, `verus` will instruct you on how to install it, and the necessary rust toolchain (1.76.0). `rustup` is Rust's installer.

Option B: Use Verus via Docker

If you have a machine that can run Linux `x86_64` docker containers, you can also use a docker image we've prepared for the course to run `verus` without having to install any dependencies separately.

From the directory that contains the files you want to verify (e.g. a file named `fibo.rs`), run:

docker run -it --rm -v .:/root/cwd ghcr.io/principled-systems/verus verus fibo.rs

This will download the Verus container and mount the current folder as /root/cwd  which corresponds to the working directory inside the container and will let Verus find the file `fibo.rs` in this case.

Verus Standard Library (vstd) documentation

The Verus Standard Library documentation for the version of Verus used in the course is accessible at: https://principled-systems.github.io/verus/verusdoc/vstd/

How to submit take-home exercises

The handouts for the take-home exercises will be published on CMS: https://cms.sic.saarland/sysverification2425/materials/

You will download a zip file containing all the take home exercises in a chapter. Modify them according to the instructions in each exercise file.

Remember to add the --crate-type=lib flag when verifying exercises, if they don't have a main function.

To submit, zip the folder that contains the exercise files and upload them via the "Submission" feature on CMS.

Take-home exercises and project rules

• Exercises and projects are individual
  • Okay to clarify problem or discuss Verus syntax
  • on Discourse, in person
• It is not okay to discuss solutions
• Do not publish your exercise solutions anywhere

• You may not use /* */ comments
• You must leave the existing /* */ comments in place
• You may only change text between /*{*/ and /*}*/
• You are not allowed to add axioms (I have not taught you how to do this)
• You are not allowed to use assume(_); or admit(); in the code you submit
• Do not rename the files