Tools of the Trade

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.

Core Tooling

Static Assurance

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!)
• cbmc via kani (Rust front-end, underlying tool also supports C/C++)
• viper via prusti* (Underlying tool supports Rust, Python, Java, ...).
• creusot* (Rust-only)

Dynamic Assurance

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)
• rr (x86, x86_64)
• libfuzzer via cargo-fuzz (x86, x86_64, ARM64)
• qemu (x86, x86_64, ARM32, ARM64, MIPS, PPC, AVR, ...)
• miri (Rust-only)

Operational Assurance

Tools that support a system's lifecycle.

• docker (Linux guests)
• cbindgen (CFFI)

Rust Ecosystem

Open-source binaries and libraries hosted on crates.io.

Development

• clap - Command line argument parsing.
• serde* - Rust structure serialization and deserialization.
• tinyvec - !#[no_std], #![forbid(unsafe_code)] Vec alternative.
• micromath - !#[no_std], #![forbid(unsafe_code)] floating point approximations.
• lazy_static* - runtime-initialized static variables.
• owo-colors - embedded-friendly text coloring.

Testing

• 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 unsafe code.
• cargo-tarpaulin* - code coverage reporting (MC/DC support planned).

Other

• 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.