Crux: Introducing Our New Open-Source Tool for Software Verification

We are happy to announce the first formal release of Crux, a new open-source verification tool from Galois. This new tool aims to improve software assurance using symbolic testing, a technique that allows for smooth migration from testing to verification. Crux builds on the same infrastructure as our Software Analysis Workbench (SAW), but with a much simpler user interface.

Using Crux

Preparing input for Crux is similar to the process of integrating with many common testing frameworks, including the testing support built into the Cargo tool for Rust. To use Crux, you write code similar to a test harness that consists of the following steps:

• Specify or generate values for all inputs.
• Execute the code to be tested on those inputs.
• Check that the result of executing the code satisfies some correctness criteria.

Crux works with both C/C++ and Rust code. As a first example of how it works, consider the following normal Rust test harness, not using Crux:

#[test]
fn test_inc_correct_concrete() {
   let x = 12345;
   assert!(x + 1 > x);
}

The #[test] attribute on this function indicates that it should be executed when running the cargo test command, which in this case, will succeed. 

The following code checks the same property using Crux:

#[crux_test]
fn test_inc_correct_symbolic() {
   let x = u32::symbolic("x");
   assert!(x + 1 > x);
}

Instead of specifying a single concrete input, this code generates a symbolic input using the u32::symbolic call. The result, stored in x, can be thought of as simultaneously representing all possible values of type u32.

Similarly, the #[crux_test] attribute on this second harness indicates that it should be executed when running the cargo crux-test command. If you’re familiar with two’s complement arithmetic, and Rust’s default overflow checking, you might have noticed, however, that there’s a value of x for which the call to assert! would fail, namely the largest 32-bit unsigned integer. And, indeed, Crux will report failure for the version of test_inc_correct_symbolic above. Consider the following modified version, instead:

#[crux_test]
fn test_inc_correct_good() {
   let x = u32::symbolic("x");
   if(x != u32::MAX) {
       assert!(x + 1 > x);
   }
}

There are now no values of x that will result in assert! being called with an argument of false, and Crux can quickly confirm this (almost as quickly as running the single concrete test described first).

How Crux Works

We call Crux a symbolic testing tool because it uses an interface very similar to existing test frameworks. But, instead of executing your program normally, Crux uses a process called symbolic execution to build up a mathematical formula that describes what the output or resulting state of the program will look like for any possible values of any symbolic inputs. In the common terminology used by the field of program analysis, the values used during normal program execution are called “concrete” values, and formulas representing many possible executions of the program are called “symbolic” values. Symbolic execution is then the process of executing a program on symbolic inputs and constructing a symbolic result.

When encountering a call to assert!, Crux passes the symbolic value of its argument to a tool called a Satisfiability Modulo Theories (SMT) solver. The solver can automatically either prove that the formula is true, regardless of the values of any variables it contains, or produce a concrete value that makes it false.

For those interested in the more technical details, Crux builds on a symbolic execution engine called Crucible that:

• Uses path merging by default. When symbolic execution of two separate paths reaches the same point in the control flow graph (a node that post-dominates all nodes in both paths), Crux will merge the two paths’ symbolic states into a single symbolic state. Optionally, this behavior can be turned off, and Crux will explore each path independently until reaching the end of the program.
• Supports many SMT solvers, including Boolector, CVC4, dReal, STP, Yices, and Z3.
• Uses aggressive formula simplification and common subterm sharing to keep symbolic values small.
• Allows path satisfiability checking to be turned on or off.
• Attempts to construct a complete final symbolic state for the program, making it suitable for verification of programs that are intrinsically bounded. Options exist to impose bounds on execution depth for bug finding in programs with potentially unbounded execution.
• Supports profiling of the symbolic execution process with an HTML-based profile viewer. Profiles include symbolic execution time for each function and solving time for each call to an SMT solver.
• Supports reasoning about floating-point values using either the real or floating-point theories available within some SMT solvers.

The interface provided by Crux is similar to that provided by CBMC and other tools that participate in the Competition on Software Verification (SV-COMP). At the moment, Crux works very similarly to CBMC on C code, though we have future plans to build on the SAW infrastructure to support features not available in CBMC.

Getting Crux and Learning More

Two versions of Crux exist. The first, Crux-LLVM, can analyze C and C++ code by working with the LLVM intermediate language generated by the clang compiler. In principle, Crux can also analyze LLVM code generated from compilers for other languages, but it has been more widely tested on C and C++ programs. The second, Crux-MIR, can analyze Rust code by working with the MIR language used internally by the Rust compiler.

More information on Crux is available on the Crux website, including a video demonstrating its use to verify portions of the curve25519-dalek Rust library. For a complete summary of the API available within user programs for interacting with Crux, see the C header file and Rust module that define them.

Binaries of Crux-LLVM and Crux-MIR for Ubuntu Linux and macOS are available on GitHub. We expect to make binaries for other platforms available in the future.

Crux can also be used through Docker by downloading one of the images from DockerHub:

docker pull galoisinc/crux-llvm:0.4
docker pull galoisinc/crux-mir:0.4

We’d love feedback! Feel free to file issues here, or contact us at crux@galois.com.