Getting Started
Get up and running with in minutes.
This guide will walk you through installing Soteria and running your first analysis. By the end, you'll be able to find bugs in Rust or C code using symbolic execution.
Soteria provides tools for both Rust and C. Choose the one that matches your needs:
On macOS (Apple Silicon) and Linux (x86-64), install Soteria
Rust directly with cargo:
cargo install soteria
cargo soteria setup # Install all necessary binaries
# You can run "cargo soteria setup" again to update the binaries after
# each nightly releaseFor other architectures, follow the manual installation instructions in the contributing guide.
Create a symbolic test
Inside of your library, for example lib.rs:
example.rsfn abs(x: i32) -> i32 {
if x < 0 { -x }
else { x }
}
fn panic_if_negative(x: i32) {
if x < 0 { panic!("Oh No!") }
}
#[soteria::test]
fn test_abs() {
let x = soteria::nondet_bytes();
// Test that this assert holds for
// **all** possible values of x
assert!(abs(x) >= 0);
}
#[soteria::test]
#[should_panic]
fn test_panic() {
let x = soteria::nondet_bytes();
soteria::assume(x < -5);
// Test that this function panics for
// **all** values of x that are less than -5
panic_if_negative(x)
}Running Soteria Rust
Running all tests in your crate:
cargo soteriaRunning one test:
cargo soteria --filter "test_abs"Pre-built binaries for macOS (Apple Silicon) and Linux (x86-64) are available on the GitHub releases page . Download the appropriate archive and add the binaries to your PATH.
For other architectures, follow the manual installation instructions in the contributing guide.
Running Soteria C
Analyze C files using a compilation database:
soteria-c capture-db compilation_database.jsonManually specify files to analyse:
soteria-c gen-sumaries file1.c file2.c -I ./includeExample: Finding a Bug
Create a file called example.c:
example.c#include <stdlib.h>
int main() {
int *p = malloc(sizeof(int));
*p = 42;
free(p);
return *p; // Bug: use-after-free!
}Run Soteria C on this file:
soteria-c exec example.cSoteria will detect the use-after-free bug and report it.
To build Soteria from source, please follow the instructions on the Soteria repository
Need Help?
If you run into issues or have questions, join our Zulip community where the team and other users can help you out.