This is a complete inventory of all the software assurance tools and Rust libraries you'll use in this book. You'll get deep experience in a few, but only a taste of most. Each name below is a link to the tool's homepage or documentation.
Rust's Open Formal Verification Ecosystem
With a spectrum of open-source options, Rust's assurance ecosystem is thriving. The Rust Formal Methods Interest Group (RFMIG) maintains a list of verification tools, available here, more comprehensive than the sample we cover in this book.
Most tools in this category reason about source-level semantics to prove the absence of certain bugs. They trust the compiler and, by extension, its backend.
rustc(Rust-only, it's literally the compiler!)
kani(Rust front-end, underlying tool also supports C/C++)
prusti* (Underlying tool supports Rust, Python, Java, ...).
Most tools in this category test compiled executables to discover specific bugs or observe program behavior. They remove the compiler from the chain of trust.
valgrind* (x86, x86_64, ARM32, ARM64, MIPS, PPC)
cargo-fuzz(x86, x86_64, ARM64)
qemu(x86, x86_64, ARM32, ARM64, MIPS, PPC, AVR, ...)
Tools that support a system's lifecycle.
Open-source binaries and libraries hosted on crates.io.
clap- Command line argument parsing.
serde* - Rust structure serialization and deserialization.
#![forbid(unsafe_code)]floating point approximations.
lazy_static* - runtime-initialized static variables.
owo-colors- embedded-friendly text coloring.
criterion- micro-benchmarking toolset.
cargo-modules- text render of project's module architecture.
cargo-audit- search project's decency graph for known-vulnerable versions.
cargo-binutils- inspect the properties and contents of Linux binaries.
cargo-bloat- determine what parts of an executable contribute to it's size.
siderophile* - search project's call graph for pockets of
cargo-tarpaulin* - code coverage reporting (MC/DC support planned).
xgadget* - ROP/JOP exploit development.
* == may be subject to change. This book is a work in progress.
Additional tools are likely to be added as the book matures. Though unlikely, tools may also be removed.