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.

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.

Operational Assurance

Tools that support a system's lifecycle.

Rust Ecosystem

Open-source binaries and libraries hosted on


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


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


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