What is SAW?

The Software Analysis Workbench (SAW) is a tool that provides the ability to formally verify properties of code written in C, Java, Rust, and . It leverages automated SAT and SMT solvers to make this process as automated as possible, and provides a scripting language, called SAWScript, to enable verification to scale up to more complex systems. We also provide a remote procedure call (RPC) API and offer a Python library that interfaces with the RPC API.

View on GitHub Download

Core Features and Capabilities

• Comprehensive Assurance: As a formal verification tool, SAW is capable of showing that your program works on all inputs, not just the ones it was tested on, and is capable of finding counterexamples when code doesn’t agree with its specification.

• Scalable Security: and SAW automate much of the most time-consuming parts of formal verification, enabling the process to scale to complex systems.

• Open Source Library: You can access the code for SAW in our open source repository.

How Does it Work?

Behind the scenes, SAW leverages symbolic execution to translate code into formal models. During this process it executes code on symbolic inputs, effectively unrolling loops, and translating the code into a circuit representation. Symbolic execution is well suited to verifying code with bounded loops such as cryptographic verification.

SAW is closely connected with , a domain-specific language Galois created for the high-level specification of cryptographic algorithms. The most common use of SAW is to prove equivalence between a Cryptol specification of an algorithm and a production implementation written in a language such as C or Java.

READ OUR DOCUMENTATION

Impact

At Galois, we have used SAW primarily to verify implementations of cryptographic algorithms such as the AES block cipher, the Secure Hash Algorithm (SHA), and Elliptic Curve Digital Signature Algorithm (ECDSA). We have used this to verify existing widely used libraries such as libgcrypt and Bouncy Castle.

We also have used SAW in collaboration with Amazon to prove the correctness of the HMAC implementation in their s2n implementation of the TLS protocol. You can read more about that work here.

More broadly, Cryptol and SAW have been used in national security, fintech, and cloud computing applications to keep citizens, systems, and data safe; secure financial transactions; and protect the privacy of millions of people across the globe. The high assurance approach they represent forms the backbone—both technologically and philosophically—of Galois’s larger effort to create trustworthiness in the most critical systems on the planet, and to maximize impact through sharing these powerful tools with the open source community.

Open Source

The R&D community, industry, and the public at large can benefit when tools like SAW are open sourced. In addition, open-source tools can themselves benefit from and be independently verified by a broad, diverse user community. With this in mind, Galois has developed SAW as an open source tool from the very beginning, and the tool is open for anyone to use and explore.

SAW SCRIPT REPO

SAW's tutorials and user manual are built and deployed to GitHub Pages as part of saw-script's continuous integration system.

We deploy versions for the master branch and all release/version tags (such that you can easily reference the documentation for the version(s) of SAW that you use).

Visit https://galoisinc.github.io/saw-script to view all available Web versions of the documentation.

• Crux-LLVM (Ubuntu 22.04 64-bit) (GPG Signature)

• Crux-LLVM (Ubuntu 20.04 64-bit) (GPG Signature)

• Crux-LLVM (OSX Arm) (GPG Signature)

• Crux-LLVM (Windows 64-bit) (GPG Signature)

• Crux-MIR (Ubuntu 22.04 64-bit) (GPG Signature)

• Crux-MIR (OSX Arm) (GPG Signature)

Crux binaries for Linux, macOS, and Windows are available from the GitHub releases page. Binaries are distributed as tarballs which you can extract to a location of your choice. Note that Crux-MIR binaries for Windows are not currently included, but we expect to include them in an upcoming release.

GPG signatures are available for each release, and we encourage you to check the signature against our public key before installing to ensure the integrity of the release you downloaded.

Crux is also packaged using Docker, and can be fetched using one of the following commands:

docker pull ghcr.io/galoisinc/crux-llvm:0.10
docker pull ghcr.io/galoisinc/crux-mir:0.10

Use the following command to run crux-mir through cargo crux-test from Docker on the Cargo project in the current directory:

docker run --rm -it --mount type=bind,source=$(pwd),target="/crux-mir/workspace" ghcr.io/galoisinc/crux-mir:0.10

Dependencies

Crux requires a companion tool, mir-json, which provides a Cargo plugin and rustc wrapper. We recommend installing mir-json directly with Cargo by following the instructions in the mir-json README.

Crux can make use of a variety of external SMT solvers, including Boolector, CVC4, CVC5, Yices, and Z3. These solvers can be downloaded from their respective developers at the locations below.

• Boolector from Johannes Kepler University Linz

• CVC4 from New York University

• CVC5 from Stanford University and the University of Iowa

• Yices from SRI International

• Z3 from Microsoft Research

SAW is an open source project, hosted on GitHub, licensed under the 3-clause BSD license. We believe that anyone who uses SAW is making an important contribution toward making the tool better. There are many ways to get involved.

Explore the Github Repository

SAW is in active development. At Galois, we are passionate about improving the security and safety of critical software, and we think that verification tools such as SAW have an important role in achieving that goal.

We would love feedback on how to make SAW better. Please contact us at [email protected] if you have any questions about SAW or high assurance development in general. If you encounter any issues using SAW, please file a ticket on GitHub.

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.

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 is available open-source under the 3-Clause BSD License on GitHub.

Download a Binary

• Linux (Ubuntu 22.04) (GPG Signature)

• Linux (Ubuntu 20.04) (GPG Signature)

• macOS 13 (X64) (GPG Signature)

• macOS 14 (ARM64) (GPG Signature)

• Windows (GPG Signature)

SAW binaries for Linux and macOS are available from the GitHub releases page. Binaries are distributed as .tar.gz or .zip files which you can extract to a location of your choice.

Nightly builds are also available here.

GPG signatures are available for each release, and we encourage you to check the signature against our public key before installing to ensure the integrity of the release you downloaded.

SAW is also available for Docker and can be fetched using one of the following commands (for the REPL and RPC API, respectively):

docker pull ghcr.io/galoisinc/saw:1.3
docker pull ghcr.io/galoisinc/saw-remote-api:1.3

Nightly versions of the Docker images are also available:

docker pull ghcr.io/galoisinc/saw:nightly
docker pull ghcr.io/galoisinc/saw-remote-api:nightly

Dependencies

SAW can make use of a variety of external tools, particularly SMT solvers. Due to SAW’s use of , the Z3 solver is a strict dependency for Cryptol type checking.

The full set of SMT solvers we currently support for other verification tasks is determined by Levent Erkök’s SBV package and Galois’ What4 package. This set currently includes ABC, Boolector, CVC4, CVC5, MathSAT, Yices, and Z3. These solvers can be downloaded from their respective developers at the locations below.

• ABC from UC Berkeley

• Boolector from Johannes Kepler University Linz

• CVC4 from New York University

• CVC5 from Stanford University and the University of Iowa

• MathSAT from Fondazione Bruno Kessler

• Yices from SRI International

• Z3 from Microsoft Research

As of release v1.1, we also provide binary packages for SAW that include compatible versions of a variety of solvers. Look for archive files that have with-solvers in the filename on the v1.2 release page.

• "Constructing semantic models of programs with the software analysis workbench" by Robert Dockins, Adam Foltzer, Joe Hendrix, Brian Huffman, Dylan McNamee, and Aaron Tomb

• “Verified Cryptographic Code for Everybody” by Brett Boston, Samuel Breese, Joey Dodds, Mike Dodds, Brian Huffman, Adam Petcher, and Andrei Stefanescu

• “Continuous Formal Verification of Amazon s2n” by Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, and Eddy Westbrook