Soteria is a library for writing efficient symbolic interpreters directly in OCaml. The core library is just a small toolbox that we use for writing a set of analyses, currently for C and Rust.

Build instructions #

To build the current repository, you first need to install OCaml. We then advise to create a local switch for development, and build the project:

opam switch create . --deps-only -y
dune build @all

If you want to run the build version of the code, you must also install Z3.

You can make sure that everything is working properly by running the test suite:

dune test

Soteria-c (working name) #

Soteria-C is an automatic in-IDE bug finder for C programs. It is in heavy development.

It can currently be tested on standalone files by opening this project in VSCode. To do so, open the Run and Debug tab of the sidebar, select the "Launch (Local)" configuration and click the "play" button.

Rusteria (soteria-rust) #

Soteria-Rust is a Kani-like symbolic execution engine for Rust. It is in heavy development.

It can run standalone files, symbolically executing the main function, or any function with the attribute #[kani::proof]. You must have Charon built and on your path -- to do so, clone Charon and run make build-dev-charon-rust and add charon/bin to your path. Once this is done, simply run:

soteria-rust exec-main <file>

To test Rusteria on the Kani test suite, clone Kani next to soteria, and run soteria-rust/scripts/kani.sh. Run soteria-rust/scripts/kani.sh --help to see all available arguments.

You can also test Rusteria on the Miri test suite: clone Miri next to soteria and run soteria-rust/scripts/miri.sh.