Crux is a tool for improving the assurance of software using symbolic testing, currently supporting C/C++ and Rust. Crux can provide you with additional assurance that your code does what you want it to do, and provides higher coverage of possible inputs than techniques such as randomized fuzzing or unit testing.
Specifically, Crux uses symbolic reasoning to check tests exhaustively, on all possible inputs, rather than on a smaller number of fixed or randomly-chosen values. In this way, Crux improves the coverage possible with property-based testing, a popular approach supported by libraries for many languages.
Crux can:
Perform symbolic reasoning to evaluate tests exhaustively
Analyze C/C++ and Rust code
Generate counter-examples when tests fail
Generate executable versions of counter-examples to load in a debugger
Generate complete models of programs to comprehensively rule out failure cases
Crux tends to work well with small, critical segments of code that primarily perform computation, rather than interacting with the outside world. For example, it is well-suited to code such as cryptographic algorithms, network packet serialization, signal processing, and similar domains. When using Crux to ensure the absence of specific bugs, the code being analyzed should operate only over fixed-size data structures, and include only loops that will terminate after a bounded number of iterations, regardless of the contents of input data. However, Crux can still be useful for finding bugs in programs that operate over unbounded data or use unbounded loops.
For larger programs, or programs where certain portions of code are missing, the Software Analysis Workbench (SAW) allows additional user input to divide programs into components and reason about those components more efficiently by considering them independently.
Behind the scenes, Crux uses symbolic execution to translate code into a mathematical model describing its behavior. Unlike many symbolic execution systems, Crux focuses on constructing complete models of the underlying software, and is therefore suitable for verification as well as bug finding.
Crux works similarly to the tools that participate in the Competition on Software Verification (SV-COMP), and supports the same API for C and C++ code.
Crux is available in source and binary form under the OSI-approved 3-clause BSD license. Binaries are available for Linux and macOS (with Windows on the way).
See the README files for the C/C++ (LLVM) and Rust (MIR) versions of Crux for more information on how to use each of the tools.
You can see future development plans for Crux and other Galois tools here.
We would love feedback on how to make Crux better. Please contact us at crux@galois.com if you have any questions about Crux or high assurance development in general. If you encounter any issues using Crux, please file an issue on GitHub.