Galois Releases New Versions of Verification Tools SAW, Cryptol, and Crux
Galois this week announced the latest releases in our suite of verification tools: SAW 1.1, Cryptol 3.1.0, and Crux 0.8. These updates mark significant strides forward in “the possible” for cryptographic specification, program verification, and computational model validation.
SAW 1.1
SAW is our tool for constructing mathematical models of computational behavior and validating their properties. In addition to existing support for LLVM and JVM code, the 1.1 release adds the ability to verify a reasonable subset of Rust code, including support for structs, enums, and slices. We have written a tutorial for how to use SAW with Rust code here, which includes a case study on how to verify a Rust implementation of the Salsa20 stream cipher.
Cryptol 3.1.0
The 3.1.0 release of Cryptol, our language for writing and specifying cryptographic algorithms, now supports the ability to define enum declarations, akin to user-defined algebraic data types found in other languages. Looking ahead, we plan to expand SAW’s support for Cryptol enums, including adding the ability to write specifications for Rust code that make use of Cryptol enums.
Crux 0.8
The 0.8 release of Crux, our tool for verifying programs with inline specifications, now offers support for a more recent Rust toolchain in its Rust backend (Crux-MIR). In addition, Crux’s C/C++ backend (Crux-LLVM) now offers support for LLVM bitcode files compiled with Apple Clang on macOS.
By continuously evolving our core verification toolset, Galois continues to push the boundaries of innovation and empower developers to reach higher standards of security, reliability, and correctness in their software.
Binary distributions, source distributions, and more detailed changelogs can be downloaded from the links below: