Modular Formal Verification of Rust Programs with Unsafe Blocks

This is a git bundle of work in progress, extending VeriFast to verify the safety of Rust programs with unsafe blocks. The corresponding technical report can be found at https://doi.org/10.48550/arXiv.2212.12976. To explore, follow the instructions below. These instructions have been tested on Ubuntu 20.04.5 LTS. Download the .bundle file and run: sudo apt update sudo apt install curl git You need to have Rust installed. run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh And in the following menu choose the default by just pressing the enter key. 1) Proceed with installation (default) 2) Customize installation 3) Cancel installation Then set up the current environment either by running the following command or simply restarting your shell. source "$HOME/.cargo/env" Now you can proceed and build VeriFast: git clone verifast_rust_tr_drop.bundle verifast cd verifast git checkout rust-tr-drop ./setup-build.sh ./build.sh The build.sh script runs VeriFast's test suite after building it. The last test case is the Rust example alloc.rs. You should see the following lines after running the test suite is finished. Total execution time: 158.274742 seconds (Obviously this time would be different depending on the machine power) 0 failed processes To play with the rust example in ide run: ./bin/vfide tests/rust/purely_unsafe/alloc.r