About

RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.

We see static verification (formal verification) and dynamic verification (testing) as two parts of the same activity and so these tools can be used for either form of verification.

Dynamic verification using the proptest fuzzing/property testing library.
Static verification using the KLEE symbolic execution engine.

We aim to add other backends in the near future.

In addition, we write articles about how the tools we wrote work (and you can read the source) in case you are porting a verification tool for use with Rust. (In particular, we describe how to generate LLVM bitcode files that can be used with LLVM-based verification tools.)

Usage

Here’s the basics of getting started with our tools.

Build a docker image

Rust verification is relatively new and we are trying to use multiple verification tools so, at least for now, these libraries have many complex dependencies that are best handled by using Docker.
```
 git clone https://github.com/project-oak/rust-verification-tools.git
 cd rust-verification-tools
 docker/build
```
This will take about 15-20 minutes to build the Docker images. The resulting docker image can be run by executing docker/run which executes a bash shell using the current user in the current directory.

If building on OSX, you should increase the container memory limit before running docker/build using the slider in the Configure:Resources menu. We tested with 8GB but 4GB is probably enough.

If you are unable to use Docker, the best approach is to manually execute the commands in the Dockerfiles invoked at the end of the docker/build script.
Open a docker shell
```
docker/run
```
All subsequent instructions assume that you are running inside docker. We normally run docker in one terminal and run an editor, git, etc. in a normal (non-docker) terminal.

If you have changed RVT since building your docker image (e.g., you edited the RVT tools/libraries or did a git pull), you should run docker/init each time you start a new docker shell to make sure that the tools and libraries have been rebuilt.
Fuzz some examples with proptest
```
cd compatibility-test
cargo test
cd ..
```
(You can also use cargo-verify --backend=proptest --verbose.)

One test should fail – this is correct behaviour.
Verify some examples with propverify

cd verification-annotations; cargo-verify --tests

or

cd compatibility-test; cargo-verify --tests

No tests should fail.
Read the propverify intro for an example of fuzzing with proptest and verifying with propverify.
Read the proptest book
Read the source code for the compatibility test suite.

(Many of these examples are taken from or based on examples in the proptest book.)

Articles: Our goals and plans

We wrote a paper about our vision for Rust verification “Towards making formal methods normal: meeting developers where they are” about tool usability, the vision of building on developers existing comfort and familiarity with testing and fuzzing, and the challenges of getting adoption of formal verification in large organizations.

Articles: Using our tools and libraries

Using the propverify library to verify Rust programs

Demonstrates the idea of writing a single verification harness that can be used for testing (using the PropTest structure-aware fuzzing library) or for verification (using the KLEE symbolic execution engine).

Also shows the basics of using our cargo-verify adaptation of cargo-test.

We also recommend reading the proptest book that thoroughly explains and documents the proptest API that propverify is based on.
Profiling Rust verification

Formal verification tools push up against Leino’s “decidability ceiling”: taking the risk of trying to solve undecidable problems in order to create more powerful tools. The cost of this is that sometimes the verifier will “blow up” on some part of your program.

This article is about finding the problem code so that you can try to fix it.

Articles: Under the hood

Using the verification-annotations crate

Demonstrates the verification API underlying propverify.
Using KLEE

Explains how to compile Rust programs to generate an LLVM file that can be used for verification and then how to use KLEE with that file.

This is a (slightly simplified) explanation of what cargo-verify does internally. (To really see how cargo-verify works, we recommend using the --script=PATH flag when using cargo-verify.)
Crux-Mir installation

Some slightly out of date instructions on using the Crux-MIR Rust verifier with our libraries.
Using command-line arguments (‘argv’)

We have been working on identifying features of realistic Rust programs that prevent you from verifying them. A surprising blocker was that we could not pass command line arguments to Rust when verifying them and so we could not do any meaningful verification of most Rust programs.

This article delves into how command line arguments (i.e., std::env::args()) work in Rust and how our rvt-patch-llvm preprocessor patches the LLVM file to make initializers work in verifiers.
Using Rust’s foreign function interface

Another common feature of Rust crates is that they are partly written in C and use Alex Crichton’s CC-rs crate to compile the C code. This was a major blocker because we need LLVM code for the entire application, not just the Rust parts of the application.

This article describes how to arrange that the C code is compiled to LLVM instead of x86/Arm machine code.
Verifying hand-vectorized Rust code

Verification tools don’t support every intrinsic function for every architecture: so they may reject hand-vectorized code.

This article describes how to bypass hand vectorized code in portable libraries that provide an unoptimized fallback path.

License

Our RVT tools and libraries are licensed under either of

Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)

at your option.

Our tools invoke KLEE, PropTest, Crux-MIR, SeaHorn, etc. which generally have flexible open-source licenses as well.

Acknowledgements

The propverify crate is heavily based on the design and API of the wonderful proptest property/fuzz-testing library. The implementation also borrows techniques, tricks and code from the implementation – you can learn a lot about how to write an embedded DSL from reading the proptest code.

In turn, proptest was influenced by the Rust port of QuickCheck and the Hypothesis fuzzing/property testing library for Python. (proptest also acknowledges regex_generate – but we have not yet implemented regex strategies for this library.)

Known limitations

This is not an officially supported Google product; this is an early release of a research project to enable experiments, feedback and contributions. It is probably not useful to use on real projects at this stage and it may change significantly in the future.

Our current goal is to make propverify as compatible with proptest as possible but we are not there yet. The most obvious features that are not even implemented are support for using regular expressions for string strategies, the Arbitrary trait, proptest-derive.

We would like the propverify library and the cargo-verify script to work with as many Rust verification tools as possible and we welcome pull requests to add support. We expect that this will require design/interface changes.

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.

See the contribution instructions for further details.