LogoLogo
Galois Website
SAW
SAW
  • SAW: The Software Analysis Workbench
  • DOCUMENTATION
    • 📋SAW Tutorials and Manual
    • 📚Publications
  • Crux
    • 🔣What is Crux?
    • ❓When should I use Crux?
    • ⬇️Download Crux
  • OPEN SOURCE
    • Overview
    • How to Contribute
  • Download
    • Get SAW
      • Public Key
Powered by GitBook
On this page
  • What is SAW?
  • Core Features and Capabilities
  • How Does it Work?
  • Impact
  • Open Source
Export as PDF

SAW: The Software Analysis Workbench

NextSAW Tutorials and Manual

Last updated 4 months ago

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 that interfaces with the RPC API.

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.

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.

Impact

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.

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

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.

At Galois, we have used SAW primarily to verify implementations of cryptographic algorithms such as the , the , and . We have used this to verify existing widely used libraries such as and .

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

open source
READ OUR DOCUMENTATION
AES block cipher
Secure Hash Algorithm (SHA)
Elliptic Curve Digital Signature Algorithm (ECDSA)
libgcrypt
Bouncy Castle
s2n
here
SAW SCRIPT REPO
Python library
View on GitHub
Download
Cryptol
Cryptol
Cryptol