Tutorials

• Program Verification with SAW

• Rust Verification with SAW

• Verification with LLVM/Java

Publications

• "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

First Example: Counting Set Bits

Most developers are used to techniques like testing, continuous integration, and thoughtful documentation that can help prevent mistakes from being introduced into a system during its development and evolution. These techniques can be relatively effective, but they risk missing certain classes of bugs. For the most important systems, like those that protect human life or information security, it can make sense to also use formal verification, in which a program is mathematically proved to be correct for all inputs.

Testing takes the actual binary executable and runs it on a subset of the possible inputs to check for expected outputs. The downside of this approach is that tests may miss some critical case. Compared to testing, verification is the process of building a mathematical model of the software and proving properties of that model for all possible inputs.

In this lesson you’ll learn how to use a system called SAW, the Software Analysis Workbench, to build models of functions written in C. You’ll learn how to specify what those functions are supposed to do, and how to write a program in SAWScript that orchestrates the proof that the functions meet their specifications.

The Code

The first program to be verified is pop_count. This function takes a 32-bit integer and returns the number of bits that are set (“populated”). For example pop_count(0) is 0, pop_count(3) is 2, and pop_count(8) is 1. This description is an English language specification of the pop_count function. A specification can be written in a number of formats, including English sentences, but also in machine-readable forms. The advantage of machine-readable specifications is that they can be used as part of an automated workflow.

Note: The pop_count function has uses in many kinds of algorithms and has an interesting folklore.

Here is a sophisticated implementation of pop_count from the book Hacker’s Delight by Henry S. Warren Jr.:

int pop_count(uint32_t x) {
    x = x - ((x >> 1) & 0x55555555);
    x = (x & 0x33333333) + ((x >> 2) & 0x33333333);
    x = (x + (x >> 4)) & 0x0F0F0F0F;
    x = x + (x >> 8);
    x = x + (x >> 16);
    return x & 0x0000003F;
}

Exercise: A Safe and a Broken pop_count

Write a version of pop_count that you believe to be correct, and also a version that includes the kind of error that could be made by accident (perhaps by adding a typo to the optimized version). Add them as pop_count_ok and pop_count_broken1 to popcount.c in the examples/intro directory.

Testing Programs

You’re not likely to be able to convince yourself that the optimized pop_count function is correct just by inspection. A unit test, like the following pop_check can help:

/* Test pop_count on a few values to make sure it's at least sometimes correct */
bool pop_check() {
    return (pop_count(0x0) == 0) &&
           (pop_count(0x3) == 2) &&
           (pop_count(0xFFFFFFFF) == 32) &&
           (pop_count(0xAAAAAAAA) == 16) &&
           (pop_count(0x55555555) == 16);
}

There are some downsides to testing only with chosen values, however. First off, these tests are usually selected by the author of the code, and there is a risk that important values are not tested. This can be ameliorated by a systematic, disciplined approach to choosing test values, but it can never be completely eliminated. This particular unit test is likely to catch egregiously buggy versions of popcount, but not subtle or tricky bugs.

A second approach to testing is to choose many random values at each execution. This approach may eventually find subtle or tricky mistakes, but not reliably or in a predictable amount of time.

Testing with random values requires an executable specification. This specification may just describe some properties of the output (e.g. that the length of two appended lists is the sum of the lengths of the input lists, or that the output of a sorting function is sorted), or it may be a simpler, more straightforward version of the code that uses an easier algorithm. An executable specification for popcount can loop over the bits in the word, masking them off one at a time. While this implementation is straightforward, it is also slow.

int pop_spec(uint32_t x) {
    uint32_t pop = 0;
    uint32_t mask = 1;
    for (int i = 0; i < 32; i++) {
        if (x & mask) { pop++; }
        mask = mask << 1;
    }
    return pop;
}

The function random_value_test performs randomized testing of a provided population count function, comparing its output to that of pop_spec. When they are not identical, it prints the offending input, which can aid in debugging.

void random_value_test(int (*fun)(uint32_t), char *name) {
    srand(time(NULL));

    int failures = 0;
    for (int i = 0; i < 100000; i ++) {
        uint32_t x = rand();
        int test = (*fun)(x);
        int check = pop_spec(x);
        if (test != check) {
            printf("Test failure: %s(%u) was %u, != %u\n",
                    name, x, test, check);
            failures++;
        }
    }
    if (failures == 0) {
        printf("Testing %s succeeded!\n", name);
    }
}

Finally, one could attempt to exhaustively check the values by enumerating and testing all possible combinations. In the simple case of pop_count, which only takes one 32-bit integer, this will take about 20 seconds. With a 64-bit version of the program, however, the test would take longer than a normal human lifetime, so this technique is not practical for ongoing software development.

The way formal verification addresses this is by reasoning about mathematical models of a program, which allows it to eliminate huge regions of the state space with single steps. There are many tools and techniques for performing full formal verification, each suitable to different classes of problem. SAW is particularly suited to imperative programs that don’t contain potentially-unbounded loops. In general, the cost of verification is that it requires specialized knowledge and developing mathematical proofs can take much longer than writing test cases. However, for many programs, automated tools like SAW can be used with similar levels of effort to testing, but resulting in much stronger guarantees. At the same time, re-checking a proof can sometimes be much faster than testing large parts of the input space, leading to quicker feedback during development.

Exercise: Testing popcount

Write a test that detects the defects in your pop_count_broken1 function, and also check that your pop_count_ok and the optimized pop_count function have no defects by using manual and random testing. How much confidence do those techniques provide?

Finally, consider pop_count_broken2, which is only incorrect for exactly one input value. Check how often the randomized test detects the one buggy input.

int pop_count_broken2(uint32_t x) {
    if (x == 0xDEADBEEF) return 22;
    return pop_count(x);
}

Symbolic Execution

The way SAW can prove properties about programs is by converting them into an internal representation that is much closer to a pure mathematical function. For instance, pop_count might be converted to a function like:

There are complications, of course, such as what to do with conditional branches, but as a user of the tool you won’t have to worry about them except when they introduce limitations to what you can reason about. The main such limitation is that symbolic simulation can’t effectively deal with loops whose termination depends on a symbolic value. For example, this simple implementation of add would not be easily analyzed:

unsigned int add(unsigned int x, unsigned int y) {
    for (unsigned int i = 0; i < y; i ++) {
        x++;
    }
    return x;
}

Running SAW

Note: This section uses a library of SAW helpers, in the file helpers.saw. If you’re comparing this text to the SAW manual, you may notice that a few operations have been abbreviated.

SAW is a tool for extracting models from compiled programs and then applying both automatic and manual reasoning to compare them against a specification of some kind. SAW builds models of programs by symbolically executing them, and is capable of building models from LLVM bitcode, JVM bytecode, x86 machine code, Rust’s MIR internal representation, and a number of other formats.

The first step to verifying pop_count with SAW is to use clang to construct its representation in LLVM bitcode. It is important to pass clang the -O1 flag, because important symbols are stripped at higher optimization levels, while lower optimization levels yield code that is less amenable to symbolic execution. The -g flag leaves symbols in the output which helps SAW produce helpful messages when verification fails. It can be convenient to include this rule in a Makefile:

.SUFFIXES: .c .bc

%.bc : %.c
	clang -g -O1 -c -emit-llvm $< -o $@

After building the LLVM bitcode file (by typing make popcount.bc), the next step is to use SAW to verify that the program meets its specification. SAW is controlled using a language called SAWScript. SAWScript contains commands for loading code artifacts, for describing program specifications, for comparing code artifacts to specifications, and for helping SAW in situations when fully automatic proofs are impossible.

The specific fact to be verified using SAW is that pop_count and pop_spec always return the same answer, no matter their input. For any particular input, this can be checked using pop_spec_check:

bool pop_spec_check(uint32_t x) {
    return (pop_spec(x) == pop_count(x));
}

The SAWScript to verify pop_count is really checking that pop_spec_check always returns true.

include "helpers.saw";
popmod <- llvm_load_module "popcount.bc";

let pop_is_ok = do {
     x <- symbolic_variable uint32_t "x";
     execute [x];
     returns TRUE;
};

llvm_verify popmod "pop_spec_check" [] pop_is_ok;

To execute the verification, we invoke saw on the SAWScript file:

$ saw pop.saw
[20:24:45.159] Loading file "/.../pop.saw"
[20:24:45.160] Loading file "/.../helpers.saw"
[20:24:45.282] Verifying pop_spec ...
[20:24:45.282] Simulating pop_spec ...
[20:24:45.291] Checking proof obligations pop_spec ...
[20:24:46.212] Proof succeeded! pop_spec

The Proof succeeded! message indicates to us that our pop_spec_check function returns True for all possible inputs. Hooray!

Returning to the SAWScript we used, it has three parts:

1. Lines 1–2 load helper functions and the LLVM module to be verified. This step builds the model from your code.

2. Lines 4–8 defines the pop_is_ok SAWScript specification, which sets up the symbolic inputs to the pop_spec function, calls the function on those symbolic inputs, and asserts that the return value is True.

3. Line 10 instructs SAW to verify that pop_is_ok is true for all possible input values.

The LLVM module is loaded using the llvm_load_module command. This command takes a string that contains the filename as an argument, and returns the module itself. In SAWScript, the results of a command are saved using the <- operator; here, the name popmod is made to refer to the module.

SAW specifications have three main parts:

1. Preconditions which state what the code being verified may assume to be true when it is called,

2. Instructions for executing the code.

3. Postconditions which state what the code must ensure to be true after it is called.

The function is invoked using the execute command, which takes an array of SAWScript variables that correspond to the function’s arguments. The function being executed is the one named by the string argument in the call to llvm_verify.

In the postcondition, the expected return value of the function is specified using returns. In this example, the function is expected to return TRUE.

Translated to English, pop_is_ok says:

In other words, pop_is_ok wraps the C function pop_spec_check. This C function computes the believed-correct result (by calling pop_spec), calls the pop_count function we are analyzing and returns TRUE if the results agree. The SAW wrapper creates the symbolic input variable, executes the function on its input, and ensures that the return value is TRUE.

Note: SAWScript distinguishes between defining a name and saving the result of a command. Use let to define a name, which may refer to a command or a value, and <- to run a command and save the result under the given name. Defining a command with let is analogous to defining a C function, and invoking commands with <- is analogous to calling it.

The arguments to llvm_verify (on line 10 above) are popmod, which specifies the LLVM module that contains the code to be verified; "pop_spec_check", the C function to be symbolically executed; and pop_is_ok, the SAW specification to check "pop_spec_check" against. The empty list ([]) is an optional list of previously proven statements, which is used in larger verification projects as described later in this tutorial. This verification script provides the same level of assurance that exhaustive testing would provide, but it completes in a tiny fraction of the time, fast enough to be part of a standard CI (continuous integration) workflow.

Exercise: Verifying Clever Versions of popcount

The following versions of popcount are quite different from the preceding implementations, but they should always return the same value. For both pop_count_mul and pop_count_sparse, do the following:

1. Write a C function, analogous to pop_spec_check, that relates pop_spec to the new implementation.

2. Use pop_is_ok in pop.saw together with additional calls to llvm_verify to asserts that the modified versions pop_spec_check also always return true. The string argument to llvm_verify states the name of the C function being verified - modify it to point to your new specification.

3. Use SAW to verify the implementation. Remember to rebuild the bitcode file after modifying the C sources.

/* A version of popcount that uses multiplication */
int pop_count_mul(uint32_t x) {
    x = x - ((x >> 1) & 0x55555555);
    x = (x & 0x33333333) + ((x >> 2) & 0x33333333);
    x = ((x + (x >> 4)) & 0x0F0F0F0F);
    return (x * 0x01010101) >> 24;
}

/* A version of popcount that uses an indefinite while loop(!) */
int pop_count_sparse(uint32_t x) {
    int n;
    n = 0;
    while (x != 0) {
        n = n + 1;
        x = x & (x - 1);
    }
    return n;
}

Exercise: Verifying Your pop_count Implementations

Verification is useful for more than just carefully-chosen examples. This exercise is about your programs.

Start with your solutions pop_count_ok and pop_count_broken1 from the first exercise. Repeat the tasks from the previous exercise, creating specifications and extending pop.saw to attempt to verify the functions.

$ make popcount.bc
$ saw pop.saw
...
[19:27:38.518] Proof succeeded! pop_ok_check
[19:27:38.520] Verifying pop_broken1_check ...
... many lines deleted
[19:27:38.856] ----------Counterexample----------
[19:27:38.856]   x: 3735928559
[19:27:38.856] ----------------------------------

As in the output above, you should see one successful verification (for the wrapper corresponding to pop_count_ok) and one failed one (for pop_count_broken1). SAW’s messages for failed verifications are quite verbose, but the most important part is the counterexample, which is a concrete input value for which the program fails to return TRUE. Next apply verification popcount_broken2 from the exercise above, which is only incorrect for exactly one input value, you will see SAW comes up with exactly that counterexample without any guidance from you.

This tutorial is intended to be an interactive experience. It is much easier to learn how to use a new tool by actually using it, making mistakes, and recovering from them. Please follow along in the provided exercises.

Background

This tutorial is written for programmers who know C, but who do not necessarily have any experience with formal verification. Deep knowledge of C is not required, but familiarity with pointers and the concept of undefined behavior are assumed. It is not necessary to be able to identify undefined behavior on sight.

Notation

Code examples, filenames, and commands that should be literally typed into a computer are represented with monospace font. For instance, the file main.c might contain the function

int main(int argc, char** argv) { ... }

which has an argument called argc. At times, italic text is used to represent mathematical variables. For instance, when relating programs to mathematical specifications, the program variable n might have the mathematical value $𝑥2$.

Exercises: Initial Setup

The first step is to install all of the necessary tools. For this tutorial, you’ll need the following:

SAW

SAW can be dowloaded from the SAW web page.

Yices and Z3

This tutorial uses Yices and Z3. If you plan to work seriously with SAW, it is also

a good idea to install the other solvers listed on the SAW download page.

Cryptol

Cryptol is included with SAW. Please use the version of Cryptol that’s included,

because each SAW release requires a specific Cryptol version.

LLVM and Clang

Please make sure that you have LLVM and clang installed.

To make sure that you have everything working, download the example files. In the examples/intro directory, run the following commands:

make swap.bc
saw swap_cryptol.saw
cryptol Swap.cry

If everything succeeds, you’ll be at a Cryptol prompt. Use :q to exit Cryptol.

Troubleshooting / Installation Alternatives

If things don’t succeed, the most likely cause is that you have a newly-released version of LLVM. SAW is dependent on LLVM’s bitcode format, which often change between releases. If you get an error along these lines:

Are you sure you’re using a supported version of LLVM/Clang?
Check here: https://github.com/GaloisInc/llvm-pretty-bc-parser

you have a couple options:

• Install an earlier version of clang and configure your platform’s PATH to use it instead of the current version, or

• Use docker or vagrant to run saw and its tools in a virtual machine. The SAW VM configurations for docker and vagrant include known-good versions of all of SAW’s dependencies. The SAW install page describes how to install SAW in a Docker container.

Using Vagrant to Install and Use SAW

In some cases, it can be easiest to run the SAW tools in a virtual machine. Vagrant is a tool that manages the installation, configuration, starting and stopping of virtual machines with Linux guests. Here’s how to run SAW in a Vagrant virtual machine:

• Install VirtualBox - instructions here

• Install Vagrant - instructions here

• cd to the examples directory unpacked from example files, which includes a Vagrantfile

• Start and log in to the virtual machine with the SAW tools configured with these commands:

vagrant up       # launch the virtual machine
vagrant ssh      # log in to your virtual machine
cd /vagrant/examples/intro
make popcount.bc
saw pop.saw      # should run to completion

• The first time you type vagrant up the system will download and configure SAW and its dependencies, so it will take a few minutes. Subsequent launches will be much faster.

• When you’re done with a session, log out of the guest and cleanly shut down your virtual machine with the host command vagrant halt

• Editing files while logged in to a virtual machine can be inconvenient. Vagrant guests have access to the host file system in the directory with the Vagrantfile, which is located in the guest at /vagrant, so it can be convenient to do your work in that directory, editing on your host, but running the SAW tools inside the virtual machine. In some cases you may have to install the “VirtualBox guest additions” to enable the shared vagrant folder.

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.

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

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, the Software Analysis Workbench, is a tool for program verification. This example-driven tutorial demonstrates how to use SAW for common tasks and how to integrate it into the software development lifecycle. The tutorial makes use of several example files.

Contents:

• Getting Started

  • Background

  • Notation

  • Exercises: Initial Setup

  • Troubleshooting / Installation Alternatives

• Specifications and Verification

  • The Code

  • Testing Programs

  • Symbolic Execution

  • Running SAW

• Memory Layout and Pointers

  • Cryptol

• Compositional Verification of Salsa20

  • Salsa20 Verification Overview

  • A Cryptol Specification

  • SAW Specification and Verification

  • Comparing Compositional and Non-compositional Verification

• Extended Exercise: HMAC Maintenance

  • Background: The Updates to the Implementation

  • Exercise: Update the Cryptol Specification

  • Exercise: Update the SAW Specifications

• Example Solution: HMAC Maintenance

  • Updating the Cryptol Specification

  • Updating the SAW Specifications

• Further Reading

  • Specification with Cryptol

  • Verification with SAW

• Glossary

Proof Maintenance Exercises: Solutions

This section provides a detailed solution to the two exercises in .

Updating the Cryptol Specification

The Cryptol type corresponding to the updated state container must, like the C structure, be augmented with an outer_just_key field that has the appropriate type, like so:

This very clearly corresponds to the change to the s2n_hmac_state structure in the C implementation, other than the specialization to SHA512. In the C implementation, the code is abstracted over the chosen hashing algorithm.

Here is a sample of how the functions that use the HMAC_c_state type must change:

Take note of how similar these changes are to those in the analogous C code; this is true more generally, as can be seen in the complete diff between HMAC_iterative_old.cry and HMAC_iterative_new.cry:

Updating the SAW Specifications

Using the hint given in the exercise, a search for the term “outer” in HMAC_old.saw reveals not only where memory layouts are specified, but embedded Cryptol terms of the type adjusted in the previous section. One of the memory layout specifications found through this search looks like this:

Another improvement that can be made to this code is to use the crucible_field primitive instead of crucible_elem, which allows reference to structure fields by name rather than by index. This, and the necessary change to memory layout, appear below.

The other change necessary is the aforementioned update to embedded Cryptol terms using the HMAC_c_state type augmented in the previous section. The original code found by searching looks like this:

And the update corresponds exactly to the one in the Cryptol specification:

The complete set of changes to the SAW specification can be seen in the diff between HMAC_old.saw and HMAC_new.saw:

With this, the specifications have been updated to account for the changes to the implementation, and verification via SAW will go through as intended.

demonstrates verification and maintenance for a small standalone function. Most interesting programs are not just single functions, however. Good software engineering practice entails splitting programs into smaller functions, each of which can be understood and tested independently. Compositional verification in SAW allows this structure to be reflected in proofs as well, so that each function can be verified independently. In addition to being more maintainable, this can greatly increase the performance of a verification script.

This section describes the verification of an implementation of the Salsa20 encryption algorithm. Complete example code can be found in the examples/salsa20 directory of the example code.

Salsa20 Verification Overview

is a stream cipher developed in 2005 by Daniel J. Bernstein, built on a pseudorandom function utilizing add-rotate-XOR (ARX) operations on 32-bit words. The original specification can be found .

The specification for this task is a trusted implementation written in . This is analogous to what is covered in in the minmax example, but for a larger system. Some examples from this specification are explored below for the sake of showing what larger Cryptol programs look like.

The implementation to be verified is written in C. This implementation is shown in part alongside the specification for comparison purposes.

A SAWScript containing the specifications of memory layouts and orchestration of the verification itself ties everything together. This will be covered last, including some performance comparisons between compositional and non-compositional verification.

A Cryptol Specification

The Cryptol specification in examples/salsa20/salsa20.cry directly implements the functions defined in Bernstein’s . Because there is so much code, this section will only go through some of the functions in detail, in order to highlight some features of Cryptol.

The first example function is quarterround. Its type is [4][32] -> [4][32], which means that it is a function that maps sequences of four 32-bit words into sequences of four 32-bit words. The [y0, y1, y2, y3] notation is pattern matching that pulls apart the four elements of the input sequence, naming each 32-bit word. The Cryptol operator <<< performs a left rotation on a sequence.

This Cryptol code closely resembles the definition in Section 3 of the specification. The definition reads:

Contrast this with the C implementation of s20_quarterround, which makes heavy use of in-place mutation rather than the functional paradigm of building and returning a new sequence:

This function directly modifies the targets of its argument pointers, a shift in paradigm that will be highlighted by the SAW specification since that is where the memory management of the C is connected to the pure computation of the Cryptol.

quarterround is used in the definition of two other functions, rowround and columnround, which perform the operation on the rows and columns of a particular matrix, represented as a flat sequence of 16 32-bit words.

These two operations are composed (rowround after columnround) to form the doubleround operation. The Cryptol code for this composition closely resembles the definition in the specification:

Combined with some utility functions for mapping sequences of four bytes to and from little-endian 32-bit words, doubleround gives us the Salsa20 hash function:

All three definitions in the where clause are sequence comprehensions, which are similar to Python’s generator expressions or C#’s LINQ. A sequence comprehension consists of square brackets that contain an expression, and then one or more branches. Branches begin with a vertical bar, and they contain one or more comma-separated bindings. Each binding is a name, an arrow, and another sequence.

The value of a comprehension with one branch is found by evaluating the expression for each element of the sequence in the branch, with the name to the left of the arrow set to the current element. The value of [x + 1 | x <- [1,2,3]] is [2, 3, 4]. If there are multiple bindings in the branch, later bindings are repeated for each earlier value. So the value of [(x + 1, y - 1) | x <- [1,2], y <- [11, 12]] is [(2, 10), (2, 11), (3, 10), (3, 11)]. The value of a comprehension with multiple branches is found by evaluating each branch in parallel; thus, the value of [(x + 1, y - 1) | x <- [1,2] | y <- [11,12]] is [(2, 10), (3, 11)].

In the where clause, the definition of xw can be read as “First split xs into 4-byte words, then combine them in a little-endian manner to obtain 32-bit words.” The specific sizes are automatically found by Cryptol’s type checker.

The definition of zs is an infinite sequence. It begins with xw, the little-endian reorganization of xs from the previous paragraph. The # operator appends sequences. The rest of the sequence consists of doubleround applied to each element of zs itself. In other words, the second element is found by applying doubleround to xw, the third by applying doubleround to the second, and so forth. Stepping through the evaluation yields this sequence:

The final definition is ar, which adds xw to the tenth element of zs, which is the result of applying doubleround ten times to xw. In Cryptol, + is extended over sequences so that adding two sequences adds their elements. The final result of Salsa20 is computed by re-joining the split words into the appropriate-sized sequence.

The C implementation uses in-place mutation and an explicit loop. Due to the use of mutation, it must be careful to copy data that will be used again later.

Note again the pervasive use of in-place mutation - as with s20_quarterround, the connection between this and the functionally pure Cryptol specification will be made clear through the SAW specification.

Salsa20 supports two key sizes: 16 and 32 bytes. Rather than writing two separate implementations, Salsa20_expansion uses two unique feature of Cryptol’s type system to implement both at once. These features are numbers in types and arithmetic predicates. Numbers in types, seen earlier, are used for the lengths of sequences, and it is possible to write functions that work on any length.

In Cryptol, some types accept arguments, which are written at the beginning of the type in curly braces. For instance, the most general type signature for a swap function on pairs is swap : {a, b} (a, b) -> (b, a). This is equivalent to the Java signature Pair<B, A> swap<A, B> (Pair<A, B> x). The {a, b} corresponds to the <A,B> immediately after swap. Arguments to types can be both ordinary types, like [8] or ([16][8], [8]), or numbers.

Type arguments can additionally be constrained. This means that a type or number argument must satisfy certain properties in order to be used. These constraints are written in parentheses and followed by a double arrow. For instance, the type of a function that takes the first element of a sequence is {n, a} (n > 0) => [n]a -> a, where n must be greater than zero (because empty sequences have no first element).

The beginning of the type signature for Salsa20_expansion reads {a} (a >= 1, 2 >= a) => ..., which says that a can only be 1 or 2. Later on in the type, [16*a][8] is used for the key length, resulting in a length of either 16 or 32 8-bit bytes. The back-tick operator allows a program to inspect the value of a length from a type, which is used in the if expression to select the appropriate input to Salsa20. Cryptol strings, like C string literals, represent sequences of ASCII byte values. The specific strings used here come from the Salsa20 specification.

SAW Specification and Verification

The SAW specification for this Salsa20 implementation is comprised of a couple of convenient helper functions, a specification for each of the interesting functions in the Salsa20 specification (i.e. the functions detailed in Bernstein’s specification document), and a defined command main that performs the actual verification.

One big difference between the Cryptol specification and the C implementation is that Cryptol, a functional language, returns new values, while programs in C, an imperative language, tend to write new values to a pointer’s target. In this case, the C version of the program overwrites an argument with the value that the Cryptol version returns. This pattern is abstracted over in oneptr_update_func, a SAWScript command that describes this relationship between the C and Cryptol versions of a function. The arguments are type : LLVMType that describes the parameter type, name : String that names the parameter for pretty-printing, and the function f : Term to apply to the parameter.

Note: If you haven’t already, look at the file helpers.saw - it defines a number of SAW functions that factor out common patterns as in oneptr_update_func, but also give more user-friendly names to various functions. Feel free to use, modify or ignore helpers.saw in SAW programs you write, and be on the lookout for new helpful functions when you work with SAW programs written by others. Good choice of names can make SAW programs much more readable.

All of Salsa20 depends on s20_quarterround. Here is its specification:

The specification for s20_hash is an example of one for which oneptr_update_func is useful.

The third argument to crucible_llvm_verify is a list of CrucibleMethodSpec objects. While performing verification, the work that was done to construct a CrucibleMethodSpec is re-used. Specifically, instead of recursively symbolically executing a verified function, the prior specification is used as an axiomatization of its behavior. In the definition of main, the results of earlier verifications are passed along:

This example also uses the fourth argument to crucible_llvm_verify. During symbolic execution, conditionals require that both branches be explored. If the fourth argument is true, then an SMT solver is used to rule out impossible branches. For some problems, the overhead of the solver exceeds the time saved on exploring branches; for others, a short time spent in the solver saves a long time spent in the symbolic execution engine. Ruling out impossible branches can also allow termination of programs in which the number of iterations can depend on a symbolic value. This is called path satisfiability checking.

The 16-byte version of Salsa20 is not verified, because the C program does not implement it. Also, Salsa20 is verified only with respect to some particular message lengths, because SAW is not yet capable of verifying infinite programs. This is why main verifies multiple lengths, in the hope that this is sufficient to increase our confidence.

Comparing Compositional and Non-compositional Verification

In examples/salsa20, there are two SAW specifications: salsa20_compositional.saw, which contains main as presented above, and salsa20_noncompositional.saw, which replaces the CrucibleMethodSpec list parameter in each call to crucible_llvm_verify with the empty list, effectively disabling compositional verification. The one exception to this is in the verification of s20_hash; not using compositional verification for this function did not terminate in a reasonable amount of time.

These two verification tasks were run on a 2019 15-inch MacBook Pro, 2.4 GHz 8-Core Intel i9 processor, 32 GB DDR4 RAM. The values shown are the average over five runs:

Even with this limited data set, the benefits of using compositional verification are clear: There’s effectively a 2x increase in speed in this example, even accounting for the fact that the verification of s20_hash is still treated compositionally.

Exercise: Rot13

Rot13 is a Caesar cipher that is its own inverse. In it, each letter is mapped to the letter that is 13 places greater than it in the alphabet, modulo 26. Non-letters are untouched, and case is preserved. For instance, “abc” becomes “nop”, and “SAW is fun!” becomes “FNJ vf sha!”.

Your task is to implement rot13 in C, and verify it using SAW.

Start by writing a function that performs a single character of rot13, assuming 7-bit ASCII encoding. Verify it using SAW and Cryptol.

Then, write a function that uses your single-character rot13 to perform rot13 on a string with precisely 20 characters in it. Verify this using SAW and Cryptol with compositional verification.

Proof Maintenance Exercises: s2n HMAC

The evolution of a program is accompanied by the evolution of its specifications. A key part of using SAW and Cryptol to verify a software system is the ongoing maintenance of proof artifacts through the software development lifecycle.

is the process of preserving the correspondence between a program, its specification, and its proof of correctness as requirements change over time. This section poses as an exercise an extended proof-maintenance task, adapted from . The code’s file structure has been reorganized slightly, but the code itself is untouched.

This task will be approached as if the changes to the implementation are given, and the goal will be to evolve the relevant specifications to match. While completing the exercises, take note of the correspondences between the changes to the code and the changes to the specifications.

Background: The Updates to the Implementation

This section provides an overview of the changes to the implementation that form the basis of the proof maintenance task to be completed.

The s2n HMAC implementation needed to be updated to make use of an additional piece of hashing state, outer_just_key, for the implementation of TLS. At its core, this change is captured by the addition of a new field to the s2n_hmac_state structure as it is defined in s2n_hmac_old.h. The resulting structure looks like this:

The addition of this new field saw corresponding changes to the implementation code, which can be found in s2n_hmac_new.c, below.

These changes included memory allocations, initializations, updates, and frees. The following code sample gives a good sense of the types of changes involved:

The complete diff between s2n_hmac_old.c and s2n_hmac_new.c shows a number of updates similar to that above:

From these changes alone, the work needed to keep the proofs up-to-date with the implementation can be very reasonably estimated. In this case, it will be necessary to complete the following tasks:

• Add the new field to the correct type(s) in the Cryptol reference implementation

• Add the relevant implementation details to the function(s) using the changed type

• Update the SAWScript to reflect new memory layouts, initializations, etc implied by the updated type

Exercise: Update the Cryptol Specification

In order for verification to go through, the Cryptol specification (that is, the implementation trusted to be correct) must be updated to reflect the existence of the new state field introduced above.

Your task is to perform these updates in HMAC_iterative_old.cry.

Use the bullet points above as a rough guide, and if you get stuck, there is a complete solution presented on the next page.

Exercise: Update the SAW Specifications

The final step to proof maintenance is updating the SAW portion of the specification. This can range in difficulty from simply updating memory layouts to changing what the specification actually asserts about the program. For the HMAC updates, the necessary changes are closer to the former rather than the latter, since the implementation change was the addition of a data field rather than overall changes to the control flow.

In this exercise, you will edit the file HMAC_old.saw ...

... to add the memory layout information for the state field added to the C implementation. Hint: A reliable strategy for updating HMAC_old.saw to account for outer_just_key is a simple search for the names of other fields already present in the structure; these will likely appear where memory layouts and initializations that need to be augmented are specified.

Note: HMAC_old.saw does not use the helpers.saw file as the previous examples did. Feel free to consult helpers.saw to help understand what the various functions do, and perhaps even rewrite HMAC_old.saw to use the helper functions.

As before, if you get stuck, there is a complete solution presented on the next page.

Specifying Memory Layout

Programs are about more than just numeric values. describes a program that works on integer values, but most C programs involve changes to values in memory. In addition to describing the return value, specifying most C programs involves describing an initial state of the heap and then relating it to the state of the heap after the program has run. SAW supports specifying programs that involve heaps and pointers.

The specification for popcount could get away with talking only about the integer values of arguments to a function and its return value. This section introduces minmax, which swaps two pointers if the first pointer’s target is greater than the second pointer’s target. The return value is -1 if the first pointer’s original target was less than the second’s, 0 if they were equal, and 1 if the second pointer’s original target was greater than the first’s.

A reference implementation of minmax follows the English specification closely:

However, the ordering of the modifications to memory and the comparisons of values can be tricky to get right in C. Instead of using a C program as the specification, this section will use a specification written in a language called Cryptol.

Cryptol

A Cryptol specification for minmax looks like this:

The first line of the file is a module header. It states that the current module is named MinMax. In this module, there are two definitions: minmax, which specifies the values expected in the pointers’ targets after running minmax, and minmax_return, which specifies the value to be returned from minmax.

Each definition begins with a type declaration. These are optional: Cryptol always type checks code, but it can usually infer types on its own. Nevertheless, they make the specification easier to understand. Also, Cryptol’s type system is very general, and some of the types that it finds on its own may be complicated. The type of minmax can be read as “a function that takes an pair of 64-bit values as an argument, and returns a pair of 64-bit values” (the arrow -> separates the argument type from the return type). The type of minmax_return can be read as “a function that takes a pair of 64-bit values as an argument, and returns a single 8-bit value”.

The Cryptol definition of minmax uses pattern matching to name the first and second elements of the incoming pair as x and y, respectively. The right side of the = specifies that the return value is the pair (y, x) if x is greater than y, or the original argument pair (x, y) otherwise. Because Cryptol’s type system doesn’t distinguish between signed and unsigned integers, the operator >$ is used for signed comparison, while > is used for unsigned comparison.

Alternatively, the definition could be written without pattern matching. In this case, the first and second elements of the pair are accessed using the .1 and .0 operators. Pairs can be seen as analogous to structs whose fields are named by numbers.

Here is the complete SAWScript for verifying our minmax function.

After including helpers.saw, the first step in using a Cryptol specification for minmax is to load the Cryptol module.

Note: In SAWScript, include is used to include the contents of a SAWScript file, while import is used for Cryptol files.

The SAWScript definition minmax_ok specifies the following:

1. Symbolic integers and pointers to them in the heap are established. pointer_to_fresh returns a tuple - the first element is a symbolic variable that’s accessible from Cryptol, the second element is a pointer to allocated memory of some type (in this case, int64_t). The pointer’s value is set to point at the allocated memory. This is done twice, once for each argument.

2. The arguments to be provided to minmax are specified using execute. In this case, the function will be called on the two pointers.

3. The desired targets of the pointers (that is, the values that they should point at after the function call) are specified using points_to after execute. In this case, the Cryptol minmax function is called, and the resulting pair is saved in result_spec, which is then used to provide the pointers’ targets.

4. The return value is specified in the same manner as that of popcount, by using returns. In this case, rather than specifying the constant TRUE, the result is also given by a Cryptol specification.

1. Finally, verification is invoked just as in popcount, using llvm_verify.

Exercises: Getting Started with SAW and Pointers

This exercise does not require the use of Cryptol.

1. Write a C function that zeroes out the target of a pointer. It should have the following prototype:
2. Write a C function zero_spec that returns true when zero is correct for some input. It should have the following prototype:
3. Use SAW to verify that zero_spec always returns true for your implementation of zero.

Exercise: Unsigned Arithmetic

Create a version of minmax that specifies its arguments as uint64_t instead of int64_t, and attempt to verify it using minmax_ok. What does the counterexample tell you about the bug that is introduced?

Exercise: Alternative Implementations

This version of minmax avoids conditional statements, relying heavily on C’s ternary operator. Verify that it fulfills the specification.

Exercise: Swapping and Rotating

Using SAW, write a specification for a C function that unconditionally swaps the targets of two pointers. Implement the function in C, and verify that it fulfills the specification. Both the specification and the implementation are simpler versions of minmax, and the specification for swap can be written without a Cryptol specification.

In the course of ordinary software development, requirements change over time. As requirements change, both programs and their specifications must evolve. A verification-oriented workflow can help maintain a correspondence between updated specifcations and code.

Modify the specification so that it describes a function rotr3. After invoking rotr3 on pointers x, y, and z, x points to the previous target of y, y points to the previous target of z, and z points to the previous target of x. Note the error message that occurs when using this specification for swap.

Implement rotr3, and verify it using the new specification.

Exercise: Arrays

In SAW, a C array type can be referred to using llvm_array, which takes the number of elements and their type as arguments. For instance, uint32[3] can be represented as llvm_array 3 (llvm_int 32). Similarly, the setup value that corresponds to an index in an array can be referred to using element. For instance, if arr refers to an array allocated using alloc, then element arr 0 is the first element in arr. These can be used with points_to.

Write a version of rotr3 that expects its argument to be an array of three integers. Verify it using SAW.

This tutorial is only the beginning. The concepts of specification, verification, and proof maintenance are applicable to a variety of tools, not just SAW, and SAW itself contains many more features than those exhibited here.

Specification with Cryptol

The best source for learning more about Cryptol is the free book Programming Cryptol. Galois maintains this book as Cryptol evolves.

This book is suitable both as a tutorial and as a reference.

Verification with SAW

The SAW Rust Tutorial and SAW LLVM/Java Tutorial describe small problems, similar in scope to Specifying Memory Layout, but use a somewhat different set of SAW features. They are good next steps after this document. After that, the SAW manual provides detailed descriptions.

compositional verification

A verification technique based on the idea that, when proving properties of a given method or function, we can make use of properties we have already proved about its callees.

Cryptol

A specification language for algorithms. Used as the notation for SAWCore in SAWScript.

proof maintenance

The process of keeping verification artifacts, such as specifications and proofs, up to date with changes in a software system over time.

SAWCore

The internal representation for programs in SAW.

SAWScript

The language used to write specifications and describe verification tasks in SAW.

SetupValue

A SAWScript SetupValue can be either a Term or a pointer. Arguments passed to symbolically executed functions must be SetupValues.

specification

A description of what is desired of a program. Specifications can be written in anything from informal English to precise, machine-readable logical formulations.

symbolic execution

The process of running a program where some input values are mathematical expressions (also called a symbolic value) instead of actual values. If the program terminates, the result is a mathematical expression that characterizes its behavior.

symbolic value

A program value that is a mathematical expression, like $∣∣𝑥+⌊𝑦⌋∣∣|x+⌊y⌋|$, instead of concrete bits in memory.

testing

The practice of finding empirical evidence that a program lives up to a specification.

Term

A SAWScript Term is a symbolic value that can only represent values, not pointers. This is in contrast to a SetupValue, which is a superclass of Terms and Pointers. Arguments passed to Cryptol functions must be Terms.

verification

The practice of finding mathematical evidence that a program lives up to a specification.

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 saw@galois.com 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.

The Software Analysis Workbench (SAW) is a tool for constructing mathematical models of the computational behavior of software, transforming these models, and proving properties about them.

SAW can currently construct models of a subset of programs written in Cryptol, LLVM (and therefore C), and JVM (and therefore Java). SAW also has experimental, incomplete support for MIR (and therefore Rust). The models take the form of typed functional programs, so in a sense SAW can be considered a translator from imperative programs to their functional equivalents. Various external proof tools, including a variety of SAT and SMT solvers, can be used to prove properties about the functional models. SAW can construct models from arbitrary Cryptol programs, and from C and Java programs that have fixed-size inputs and outputs and that terminate after a fixed number of iterations of any loop (or a fixed number of recursive calls). One common use case is to verify that an algorithm specification in Cryptol is equivalent to an algorithm implementation in C or Java.

The process of extracting models from programs, manipulating them, forming queries about them, and sending them to external provers is orchestrated using a special purpose language called SAWScript. SAWScript is a typed functional language with support for sequencing of imperative commands.

The rest of this document first describes how to use the SAW tool, saw, and outlines the structure of the SAWScript language and its relationship to Cryptol. It then presents the SAWScript commands that transform functional models and prove properties about them. Finally, it describes the specific commands available for constructing models from imperative programs.

Invoking SAW

The primary mechanism for interacting with SAW is through the saw executable included as part of the standard binary distribution. With no arguments, saw starts a read-evaluate-print loop (REPL) that allows the user to interactively evaluate commands in the SAWScript language. With one file name argument, it executes the specified file as a SAWScript program.

In addition to a file name, the saw executable accepts several command-line options:

-h, -?, --help

Print a help message.

-V, --version

Show the version of the SAWScript interpreter.

-c path, --classpath=path

Specify a colon-delimited list of paths to search for Java classes.

-i path, --import-path=path

Specify a colon-delimited list of paths to search for imports.

-t, --extra-type-checking

Perform extra type checking of intermediate values.

-I, --interactive

Run interactively (with a REPL). This is the default if no other arguments are specified.

-j path, --jars=path

Specify a colon-delimited list of paths to .jar files to search for Java classes.

-b path, --java-bin-dirs

Specify a colon-delimited list of paths to search for a Java executable.

-d num, --sim-verbose=num

Set the verbosity level of the Java and LLVM simulators.

-v num, --verbose=num

Set the verbosity level of the SAWScript interpreter.

--clean-mismatched-versions-solver-cache[=path]

Run the clean_mismatched_versions_solver_cache command on the solver cache at the given path, or if no path is given, the solver cache at the value of the SAW_SOLVER_CACHE_PATH environment variable, then exit. See the section Caching Solver Results for a description of the clean_mismatched_versions_solver_cache command and the solver caching feature in general.

SAW also uses several environment variables for configuration:

CRYPTOLPATH

Specify a colon-delimited list of directory paths to search for Cryptol imports (including the Cryptol prelude).

PATH

If the --java-bin-dirs option is not set, then the PATH will be searched to find a Java executable.

SAW_IMPORT_PATH

Specify a colon-delimited list of directory paths to search for imports.

SAW_JDK_JAR

Specify the path of the .jar file containing the core Java libraries. Note that that is not necessary if the --java-bin-dirs option or the PATH environment variable is used, as SAW can use this information to determine the location of the core Java libraries’ .jar file.

SAW_SOLVER_CACHE_PATH

Specify a path at which to keep a cache of solver results obtained during calls to certain tactics. A cache is not created at this path until it is needed. See the section Caching Solver Results for more detail about this feature.

On Windows, semicolon-delimited lists are used instead of colon-delimited lists.

Structure of SAWScript

A SAWScript program consists, at the top level, of a sequence of commands to be executed in order. Each command is terminated with a semicolon. For example, the print command displays a textual representation of its argument. Suppose the following text is stored in the file print.saw:

print 3;

The command saw print.saw will then yield output similar to the following:

Loading module Cryptol
Loading file "print.saw"
3

The same code can be run from the interactive REPL:

sawscript> print 3;
3

At the REPL, terminating semicolons can be omitted:

sawscript> print 3
3

To make common use cases simpler, bare values at the REPL are treated as if they were arguments to print:

sawscript> 3
3

One SAWScript file can be included in another using the include command, which takes the name of the file to be included as an argument. For example:

sawscript> include "print.saw"
Loading file "print.saw"
3

Typically, included files are used to import definitions, not perform side effects like printing. However, as you can see, if any commands with side effects occur at the top level of the imported file, those side effects will occur during import.

Syntax

The syntax of SAWScript is reminiscent of functional languages such as Cryptol, Haskell and ML. In particular, functions are applied by writing them next to their arguments rather than by using parentheses and commas. Rather than writing f(x, y), write f x y.

Comments are written as in C, Java, and Rust (among many other languages). All text from // until the end of a line is ignored. Additionally, all text between /* and */ is ignored, regardless of whether the line ends.

Basic Types and Values

All values in SAWScript have types, and these types are determined and checked before a program runs (that is, SAWScript is statically typed). The basic types available are similar to those in many other languages.

• The Int type represents unbounded mathematical integers. Integer constants can be written in decimal notation (e.g., 42), hexadecimal notation (0x2a), and binary (0b00101010). However, unlike many languages, integers in SAWScript are used primarily as constants. Arithmetic is usually encoded in Cryptol, as discussed in the next section.

• The Boolean type, Bool, contains the values true and false, like in many other languages. As with integers, computations on Boolean values usually occur in Cryptol.

• Values of any type can be aggregated into tuples. For example, the value (true, 10) has the type (Bool, Int).

• Values of any type can also be aggregated into records, which are exactly like tuples except that their components have names. For example, the value { b = true, n = 10 } has the type { b : Bool, n : Int }.

• A sequence of values of the same type can be stored in a list. For example, the value [true, false, true] has the type [Bool].

• Strings of textual characters can be represented in the String type. For example, the value "example" has type String.

• The “unit” type, written (), is essentially a placeholder, similar to void in languages like C and Java. It has only one value, also written (). Values of type () convey no information. We will show in later sections several cases where this is useful.

• Functions are given types that indicate what type they consume and what type they produce. For example, the type Int -> Bool indicates a function that takes an Int as input and produces a Bool as output. Functions with multiple arguments use multiple arrows. For example, the type Int -> String -> Bool indicates a function in which the first argument is an Int, the second is a String, and the result is a Bool. It is possible, but not necessary, to group arguments in tuples, as well, so the type (Int, String) -> Bool describes a function that takes one argument, a pair of an Int and a String, and returns a Bool.

SAWScript also includes some more specialized types that do not have straightforward counterparts in most other languages. These will appear in later sections.

Basic Expression Forms

One of the key forms of top-level command in SAWScript is a binding, introduced with the let keyword, which gives a name to a value. For example:

sawscript> let x = 5
sawscript> x
5

Bindings can have parameters, in which case they define functions. For instance, the following function takes one parameter and constructs a list containing that parameter as its single element.

sawscript> let f x = [x]
sawscript> f "text"
["text"]

Functions themselves are values and have types. The type of a function that takes an argument of type a and returns a result of type b is a -> b.

Function types are typically inferred, as in the example f above. In this case, because f only creates a list with the given argument, and because it is possible to create a list of any element type, f can be applied to an argument of any type. We say, therefore, that f is polymorphic. Concretely, we write the type of f as {a} a -> [a], meaning it takes a value of any type (denoted a) and returns a list containing elements of that same type. This means we can also apply f to 10:

sawscript> f 10
[10]

However, we may want to specify that a function has a more specific type. In this case, we could restrict f to operate only on Int parameters.

sawscript> let f (x : Int) = [x]

This will work identically to the original f on an Int parameter:

sawscript> f 10
[10]

However, it will fail for a String parameter:

sawscript> f "text"

type mismatch: String -> t.0 and Int -> [Int]
 at "_" (REPL)
mismatched type constructors: String and Int

Type annotations can be applied to any expression. The notation (e : t) indicates that expression e is expected to have type t and that it is an error for e to have a different type. Most types in SAWScript are inferred automatically, but specifying them explicitly can sometimes enhance readability.

Because functions are values, functions can return other functions. We make use of this feature when writing functions of multiple arguments. Consider the function g, similar to f but with two arguments:

sawscript> let g x y = [x, y]

Like f, g is polymorphic. Its type is {a} a -> a -> [a]. This means it takes an argument of type a and returns a function that takes an argument of the same type a and returns a list of a values. We can therefore apply g to any two arguments of the same type:

sawscript> g 2 3
[2,3]
sawscript> g true false
[true,false]

But type checking will fail if we apply it to two values of different types:

sawscript> g 2 false

type mismatch: Bool -> t.0 and Int -> [Int]
 at "_" (REPL)
mismatched type constructors: Bool and Int

So far we have used two related terms, function and command, and we take these to mean slightly different things. A function is any value with a function type (e.g., Int -> [Int]). A command is any value with a special command type (e.g. TopLevel (), as shown below). These special types allow us to restrict command usage to specific contexts, and are also parameterized (like the list type). Most but not all commands are also functions.

The most important command type is the TopLevel type, indicating a command that can run at the top level (directly at the REPL, or as one of the top level commands in a script file). The print command has the type {a} a -> TopLevel (), where TopLevel () means that it is a command that runs in the TopLevel context and returns a value of type () (that is, no useful information). In other words, it has a side effect (printing some text to the screen) but doesn’t produce any information to use in the rest of the SAWScript program. This is the primary usage of the () type.

It can sometimes be useful to bind a sequence of commands together. This can be accomplished with the do { ... } construct. For example:

sawscript> let print_two = do { print "first"; print "second"; }
sawscript> print_two
first
second

The bound value, print_two, has type TopLevel (), since that is the type of its last command.

Note that in the previous example the printing doesn’t occur until print_two directly appears at the REPL. The let expression does not cause those commands to run. The construct that runs a command is written using the <- operator. This operator works like let except that it says to run the command listed on the right hand side and bind the result, rather than binding the variable to the command itself. Using <- instead of let in the previous example yields:

sawscript> print_two <- do { print "first"; print "second"; }
first
second
sawscript> print print_two
()

Here, the print commands run first, and then print_two gets the value returned by the second print command, namely (). Any command run without using <- at either the top level of a script or within a do block discards its result. However, the REPL prints the result of any command run without using the <- operator.

In some cases it can be useful to have more control over the value returned by a do block. The return command allows us to do this. For example, say we wanted to write a function that would print a message before and after running some arbitrary command and then return the result of that command. We could write:

let run_with_message msg c =
  do {
    print "Starting.";
    print msg;
    res <- c;
    print "Done.";
    return res;
  };

x <- run_with_message "Hello" (return 3);
print x;

If we put this script in run.saw and run it with saw, we get something like:

Loading module Cryptol
Loading file "run.saw"
Starting.
Hello
Done.
3

Note that it ran the first print command, then the caller-specified command, then the second print command. The result stored in x at the end is the result of the return command passed in as an argument.

Other Basic Functions

Aside from the functions we have listed so far, there are a number of other operations for working with basic data structures and interacting with the operating system.

The following functions work on lists:

• concat : {a} [a] -> [a] -> [a] takes two lists and returns the concatenation of the two.

• head : {a} [a] -> a returns the first element of a list.

• tail : {a} [a] -> [a] returns everything except the first element.

• length : {a} [a] -> Int counts the number of elements in a list.

• null : {a} [a] -> Bool indicates whether a list is empty (has zero elements).

• nth : {a} [a] -> Int -> a returns the element at the given position, with nth l 0 being equivalent to head l.

• for : {m, a, b} [a] -> (a -> m b) -> m [b] takes a list and a function that runs in some command context. The passed command will be called once for every element of the list, in order. Returns a list of all of the results produced by the command.

For interacting with the operating system, we have:

• get_opt : Int -> String returns the command-line argument to saw at the given index. Argument 0 is always the name of the saw executable itself, and higher indices represent later arguments.

• exec : String -> [String] -> String -> TopLevel String runs an external program given, respectively, an executable name, a list of arguments, and a string to send to the standard input of the program. The exec command returns the standard output from the program it executes and prints standard error to the screen.

• exit : Int -> TopLevel () stops execution of the current script and returns the given exit code to the operating system.

Finally, there are a few miscellaneous functions and commands:

• show : {a} a -> String computes the textual representation of its argument in the same way as print, but instead of displaying the value it returns it as a String value for later use in the program. This can be useful for constructing more detailed messages later.

• str_concat : String -> String -> String concatenates two String values, and can also be useful with show.

• time : {a} TopLevel a -> TopLevel a runs any other TopLevel command and prints out the time it took to execute.

• with_time : {a} TopLevel a -> TopLevel (Int, a) returns both the original result of the timed command and the time taken to execute it (in milliseconds), without printing anything in the process.

The Term Type

Perhaps the most important type in SAWScript, and the one most unlike the built-in types of most other languages, is the Term type. Essentially, a value of type Term precisely describes all possible computations performed by some program. In particular, if two Term values are equivalent, then the programs that they represent will always compute the same results given the same inputs. We will say more later about exactly what it means for two terms to be equivalent, and how to determine whether two terms are equivalent.

Before exploring the Term type more deeply, it is important to understand the role of the Cryptol language in SAW.

Cryptol and its Role in SAW

Cryptol is a domain-specific language originally designed for the high-level specification of cryptographic algorithms. It is general enough, however, to describe a wide variety of programs, and is particularly applicable to describing computations that operate on streams of data of some fixed size.

In addition to being integrated into SAW, Cryptol is a standalone language with its own manual:

CRYPTOL MANUAL

SAW includes deep support for Cryptol, and in fact requires the use of Cryptol for most non-trivial tasks. To fully understand the rest of this manual and to effectively use SAW, you will need to develop at least a rudimentary understanding of Cryptol.

The primary use of Cryptol within SAWScript is to construct values of type Term. Although Term values can be constructed from various sources, inline Cryptol expressions are the most direct and convenient way to create them.

Specifically, a Cryptol expression can be placed inside double curly braces ({{ and }}), resulting in a value of type Term. As a very simple example, there is no built-in integer addition operation in SAWScript. However, we can use Cryptol’s built-in integer addition operator within SAWScript as follows:

sawscript> let t = {{ 0x22 + 0x33 }}
sawscript> print t
85
sawscript> :type t
Term

Although it printed out in the same way as an Int, it is important to note that t actually has type Term. We can see how this term is represented internally, before being evaluated, with the print_term function.

sawscript> print_term t
let { x@1 = Prelude.Vec 8 Prelude.Bool
      x@2 = Cryptol.TCNum 8
      x@3 = Cryptol.PLiteralSeqBool x@2
    }
 in Cryptol.ecPlus x@1 (Cryptol.PArithSeqBool x@2)
      (Cryptol.ecNumber (Cryptol.TCNum 34) x@1 x@3)
      (Cryptol.ecNumber (Cryptol.TCNum 51) x@1 x@3)

For the moment, it’s not important to understand what this output means. We show it only to clarify that Term values have their own internal structure that goes beyond what exists in SAWScript. The internal representation of Term values is in a language called SAWCore. The full semantics of SAWCore are beyond the scope of this manual.

The text constructed by print_term can also be accessed programmatically (instead of printing to the screen) using the show_term function, which returns a String. The show_term function is not a command, so it executes directly and does not need <- to bind its result. Therefore, the following will have the same result as the print_term command above:

sawscript> let s = show_term t
sawscript> :type s
String
sawscript> print s
<same as above>

Numbers are printed in decimal notation by default when printing terms, but the following two commands can change that behavior.

• set_ascii : Bool -> TopLevel (), when passed true, makes subsequent print_term or show_term commands print sequences of bytes as ASCII strings (and doesn’t affect printing of anything else).

• set_base : Int -> TopLevel () prints all bit vectors in the given base, which can be between 2 and 36 (inclusive).

A Term that represents an integer (any bit vector, as affected by set_base) can be translated into a SAWScript Int using the eval_int : Term -> Int function. This function returns an Int if the Term can be represented as one, and fails at runtime otherwise.

sawscript> print (eval_int t)
85
sawscript> print (eval_int {{ True }})

"eval_int" (<stdin>:1:1):
eval_int: argument is not a finite bitvector
sawscript> print (eval_int {{ [True] }})
1

Similarly, values of type Bit in Cryptol can be translated into values of type Bool in SAWScript using the eval_bool : Term -> Bool function:

sawscript> let b = {{ True }}
sawscript> print_term b
Prelude.True
sawscript> print (eval_bool b)
true

Anything with sequence type in Cryptol can be translated into a list of Term values in SAWScript using the eval_list : Term -> [Term] function.

sawscript> let l = {{ [0x01, 0x02, 0x03] }}
sawscript> print_term l
let { x@1 = Prelude.Vec 8 Prelude.Bool
      x@2 = Cryptol.PLiteralSeqBool (Cryptol.TCNum 8)
    }
 in [Cryptol.ecNumber (Cryptol.TCNum 1) x@1 x@2
    ,Cryptol.ecNumber (Cryptol.TCNum 2) x@1 x@2
    ,Cryptol.ecNumber (Cryptol.TCNum 3) x@1 x@2]
sawscript> print (eval_list l)
[Cryptol.ecNumber (Cryptol.TCNum 1) (Prelude.Vec 8 Prelude.Bool)
  (Cryptol.PLiteralSeqBool (Cryptol.TCNum 8))
,Cryptol.ecNumber (Cryptol.TCNum 2) (Prelude.Vec 8 Prelude.Bool)
  (Cryptol.PLiteralSeqBool (Cryptol.TCNum 8))
,Cryptol.ecNumber (Cryptol.TCNum 3) (Prelude.Vec 8 Prelude.Bool)
  (Cryptol.PLiteralSeqBool (Cryptol.TCNum 8))]

Finally, a list of Term values in SAWScript can be collapsed into a single Term with sequence type using the list_term : [Term] -> Term function, which is the inverse of eval_list.

sawscript> let ts = eval_list l
sawscript> let l = list_term ts
sawscript> print_term l
let { x@1 = Prelude.Vec 8 Prelude.Bool
      x@2 = Cryptol.PLiteralSeqBool (Cryptol.TCNum 8)
    }
 in [Cryptol.ecNumber (Cryptol.TCNum 1) x@1 x@2
    ,Cryptol.ecNumber (Cryptol.TCNum 2) x@1 x@2
    ,Cryptol.ecNumber (Cryptol.TCNum 3) x@1 x@2]

In addition to being able to extract integer and Boolean values from Cryptol expressions, Term values can be injected into Cryptol expressions. When SAWScript evaluates a Cryptol expression between {{ and }} delimiters, it does so with several extra bindings in scope:

• Any variable in scope that has SAWScript type Bool is visible in Cryptol expressions as a value of type Bit.

• Any variable in scope that has SAWScript type Int is visible in Cryptol expressions as a type variable. Type variables can be demoted to numeric bit vector values using the backtick (`) operator.

• Any variable in scope that has SAWScript type Term is visible in Cryptol expressions as a value with the Cryptol type corresponding to the internal type of the term. The power of this conversion is that the Term does not need to have originally been derived from a Cryptol expression.

In addition to these rules, bindings created at the Cryptol level, either from included files or inside Cryptol quoting brackets, are visible only to later Cryptol expressions, and not as SAWScript variables.

To make these rules more concrete, consider the following examples. If we bind a SAWScript Int, we can use it as a Cryptol type variable. If we create a Term variable that internally has function type, we can apply it to an argument within a Cryptol expression, but not at the SAWScript level:

sawscript> let n = 8
sawscript> :type n
Int
sawscript> let {{ f (x : [n]) = x + 1 }}
sawscript> :type {{ f }}
Term
sawscript> :type f

<stdin>:1:1-1:2: unbound variable: "f" (<stdin>:1:1-1:2)
sawscript> print {{ f 2 }}
3

If f was a binding of a SAWScript variable to a Term of function type, we would get a different error:

sawscript> let f = {{ \(x : [n]) -> x + 1 }}
sawscript> :type {{ f }}
Term
sawscript> :type f
Term
sawscript> print {{ f 2 }}
3
sawscript> print (f 2)

type mismatch: Int -> t.0 and Term
 at "_" (REPL)
 mismatched type constructors: (->) and Term

One subtlety of dealing with Terms constructed from Cryptol is that because the Cryptol expressions themselves are type checked by the Cryptol type checker, and because they may make use of other Term values already in scope, they are not type checked until the Cryptol brackets are evaluated. So type errors at the Cryptol level may occur at runtime from the SAWScript perspective (though they occur before the Cryptol expressions are run).

So far, we have talked about using Cryptol value expressions. However, SAWScript can also work with Cryptol types. The most direct way to refer to a Cryptol type is to use type brackets: {| and |}. Any Cryptol type written between these brackets becomes a Type value in SAWScript. Some types in Cryptol are numeric (also known as size) types, and correspond to non-negative integers. These can be translated into SAWScript integers with the eval_size function. For example:

sawscript> let {{ type n = 16 }}
sawscript> eval_size {| n |}
16
sawscript> eval_size {| 16 |}
16

For non-numeric types, eval_size fails at runtime:

sawscript> eval_size {| [16] |}

"eval_size" (<stdin>:1:1):
eval_size: not a numeric type

In addition to the use of brackets to write Cryptol expressions inline, several built-in functions can extract Term values from Cryptol files in other ways. The import command at the top level imports all top-level definitions from a Cryptol file and places them in scope within later bracketed expressions. This includes Cryptol foreign declarations. If a Cryptol implementation of a foreign function is present, then it will be used as the definition when reasoning about the function. Otherwise, the function will be imported as an opaque constant with no definition.

The cryptol_load command behaves similarly, but returns a CryptolModule instead. If any CryptolModule is in scope, its contents are available qualified with the name of the CryptolModule variable. A specific definition can be explicitly extracted from a CryptolModule using the cryptol_extract command:

• cryptol_extract : CryptolModule -> String -> TopLevel Term

Transforming Term Values

The three primary functions of SAW are extracting models (Term values) from programs, transforming those models, and proving properties about models using external provers. So far we’ve shown how to construct Term values from Cryptol programs; later sections will describe how to extract them from other programs. Now we show how to use the various term transformation features available in SAW.

Rewriting

Rewriting a Term consists of applying one or more rewrite rules to it, resulting in a new Term. A rewrite rule in SAW can be specified in multiple ways:

1. as the definition of a function that can be unfolded,

2. as a term of Boolean type (or a function returning a Boolean) that is an equality statement, and

3. as a term of equality type with a body that encodes a proof that the equality in the type is valid.

In each case the term logically consists of two sides and describes a way to transform the left side into the right side. Each side may contain variables (bound by enclosing lambda expressions) and is therefore a pattern which can match any term in which each variable represents an arbitrary sub-term. The left-hand pattern describes a term to match (which may be a sub-term of the full term being rewritten), and the right-hand pattern describes a term to replace it with. Any variable in the right-hand pattern must also appear in the left-hand pattern and will be instantiated with whatever sub-term matched that variable in the original term.

For example, say we have the following Cryptol function:

 \(x:[8]) -> (x * 2) + 1

We might for some reason want to replace multiplication by a power of two with a shift. We can describe this replacement using an equality statement in Cryptol (a rule of form 2 above):

\(y:[8]) -> (y * 2) == (y << 1)

Interpreting this as a rewrite rule, it says that for any 8-bit vector (call it y for now), we can replace y * 2 with y << 1. Using this rule to rewrite the earlier expression would then yield:

 \(x:[8]) -> (x << 1) + 1

The general philosophy of rewriting is that the left and right patterns, while syntactically different, should be semantically equivalent. Therefore, applying a set of rewrite rules should not change the fundamental meaning of the term being rewritten. SAW is particularly focused on the task of proving that some logical statement expressed as a Term is always true. If that is in fact the case, then the entire term can be replaced by the term True without changing its meaning. The rewriting process can in some cases, by repeatedly applying rules that themselves are known to be valid, reduce a complex term entirely to True, which constitutes a proof of the original statement. In other cases, rewriting can simplify terms before sending them to external automated provers that can then finish the job. Sometimes this simplification can help the automated provers run more quickly, and sometimes it can help them prove things they would otherwise be unable to prove by applying reasoning steps (rewrite rules) that are not available to the automated provers.

In practical use, rewrite rules can be aggregated into Simpset values in SAWScript. A few pre-defined Simpset values exist:

• empty_ss : Simpset is the empty set of rules. Rewriting with it should have no effect, but it is useful as an argument to some of the functions that construct larger Simpset values.

• basic_ss : Simpset is a collection of rules that are useful in most proof scripts.

• cryptol_ss : () -> Simpset includes a collection of Cryptol-specific rules. Some of these simplify away the abstractions introduced in the translation from Cryptol to SAWCore, which can be useful when proving equivalence between Cryptol and non-Cryptol code. Leaving these abstractions in place is appropriate when comparing only Cryptol code, however, so cryptol_ss is not included in basic_ss.

The next set of functions can extend or apply a Simpset:

• addsimp' : Term -> Simpset -> Simpset adds a single Term to an existing `Simpset.

• addsimps' : [Term] -> Simpset -> Simpset adds a list of Terms to an existing Simpset.

• rewrite : Simpset -> Term -> Term applies a Simpset to an existing Term to produce a new Term.

To make this more concrete, we examine how the rewriting example sketched above, to convert multiplication into shift, can work in practice. We simplify everything with cryptol_ss as we go along so that the Terms don’t get too cluttered. First, we declare the term to be transformed:

sawscript> let term = rewrite (cryptol_ss ()) {{ \(x:[8]) -> (x * 2) + 1 }}
sawscript> print_term term
\(x : Prelude.Vec 8 Prelude.Bool) ->
  Prelude.bvAdd 8 (Prelude.bvMul 8 x (Prelude.bvNat 8 2))
    (Prelude.bvNat 8 1)

Next, we declare the rewrite rule:

sawscript> let rule = rewrite (cryptol_ss ()) {{ \(y:[8]) -> (y * 2) == (y << 1) }}
sawscript> print_term rule
let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in \(y : x@1) ->
      Cryptol.ecEq x@1 (Cryptol.PCmpWord 8)
        (Prelude.bvMul 8 y (Prelude.bvNat 8 2))
        (Prelude.bvShiftL 8 Prelude.Bool 1 Prelude.False y
           (Prelude.bvNat 1 1))

Finally, we apply the rule to the target term:

sawscript> let result = rewrite (addsimp' rule empty_ss) term
sawscript> print_term result
\(x : Prelude.Vec 8 Prelude.Bool) ->
  Prelude.bvAdd 8
    (Prelude.bvShiftL 8 Prelude.Bool 1 Prelude.False x
       (Prelude.bvNat 1 1))
    (Prelude.bvNat 8 1)

Note that addsimp' and addsimps' take a Term or list of Terms; these could in principle be anything, and are not necessarily terms representing logically valid equalities. They have ' suffixes because they are not intended to be the primary interface to rewriting. When using these functions, the soundness of the proof process depends on the correctness of these rules as a side condition.

The primary interface to rewriting uses the Theorem type instead of the Term type, as shown in the signatures for addsimp and addsimps.

• addsimp : Theorem -> Simpset -> Simpset adds a single Theorem to a Simpset.

• addsimps : [Theorem] -> Simpset -> Simpset adds several Theorem values to a Simpset.

A Theorem is essentially a Term that is proven correct in some way. In general, a Theorem can be any statement, and may not be useful as a rewrite rule. However, if it has an appropriate shape it can be used for rewriting. In the “Proofs about Terms” section, we’ll describe how to construct Theorem values from Term values.

In the absence of user-constructed Theorem values, there are some additional built-in rules that are not included in either basic_ss and cryptol_ss because they are not always beneficial, but that can sometimes be helpful or essential. The cryptol_ss simpset includes rewrite rules to unfold all definitions in the Cryptol SAWCore module, but does not include any of the terms of equality type.

• add_cryptol_defs :[String] -> Simpset -> Simpsetadds unfolding rules for functions with the given names from the SAWCoreCryptolmodule to the givenSimpset`.

• add_cryptol_eqs : [String] -> Simpset -> Simpset adds the terms of equality type with the given names from the SAWCore Cryptol module to the given Simpset.

• add_prelude_defs : [String] -> Simpset -> Simpset adds unfolding rules from the SAWCore Prelude module to a Simpset.

• add_prelude_eqs : [String] -> Simpset -> Simpset adds equality-typed terms from the SAWCore Prelude module to a Simpset.

Finally, it’s possible to construct a theorem from an arbitrary SAWCore expression (rather than a Cryptol expression), using the core_axiom function.

• core_axiom : String -> Theorem creates a Theorem from a String in SAWCore syntax. Any Theorem introduced by this function is assumed to be correct, so use it with caution.

Folding and Unfolding

A SAWCore term can be given a name using the define function, and is then by default printed as that name alone. A named subterm can be “unfolded” so that the original definition appears again.

• define : String -> Term -> TopLevel Term

• unfold_term : [String] -> Term -> Term

For example:

sawscript> let t = {{ 0x22 }}
sawscript> print_term t
Cryptol.ecNumber (Cryptol.TCNum 34) (Prelude.Vec 8 Prelude.Bool)
  (Cryptol.PLiteralSeqBool (Cryptol.TCNum 8))
sawscript> t' <- define "t" t
sawscript> print_term t'
t
sawscript> let t'' = unfold_term ["t"] t'
sawscript> print_term t''
Cryptol.ecNumber (Cryptol.TCNum 34) (Prelude.Vec 8 Prelude.Bool)
  (Cryptol.PLiteralSeqBool (Cryptol.TCNum 8))

This process of folding and unfolding is useful both to make large terms easier for humans to work with and to make automated proofs more tractable. We’ll describe the latter in more detail when we discuss interacting with external provers.

In some cases, folding happens automatically when constructing Cryptol expressions. Consider the following example:

sawscript> let t = {{ 0x22 }}
sawscript> print_term t
Cryptol.ecNumber (Cryptol.TCNum 34) (Prelude.Vec 8 Prelude.Bool)
  (Cryptol.PLiteralSeqBool (Cryptol.TCNum 8))
sawscript> let {{ t' = 0x22 }}
sawscript> print_term {{ t' }}
t'

This illustrates that a bare expression in Cryptol braces gets translated directly to a SAWCore term. However, a Cryptol definition gets translated into a folded SAWCore term. In addition, because the second definition of t occurs at the Cryptol level, rather than the SAWScript level, it is visible only inside Cryptol braces. Definitions imported from Cryptol source files are also initially folded and can be unfolded as needed.

Other Built-in Transformation and Inspection Functions

In addition to the Term transformation functions described so far, a variety of others also exist.

• beta_reduce_term : Term -> Term takes any sub-expression of the form (\x -> t) v in the given Term and replaces it with a transformed version of t in which all instances of x are replaced by v.

• replace : Term -> Term -> Term -> TopLevel Term replaces arbitrary subterms. A call to replace x y t replaces any instance of x inside t with y.

Assessing the size of a term can be particularly useful during benchmarking. SAWScript provides two mechanisms for this.

• term_size : Term -> Int calculates the number of nodes in the Directed Acyclic Graph (DAG) representation of a Term used internally by SAW. This is the most appropriate way of determining the resource use of a particular term.

• term_tree_size : Term -> Int calculates how large a Term would be if it were represented by a tree instead of a DAG. This can, in general, be much, much larger than the number returned by term_size, and serves primarily as a way of assessing, for a specific term, how much benefit there is to the term sharing used by the DAG representation.

Finally, there are a few commands related to the internal SAWCore type of a Term.

• check_term : Term -> TopLevel () checks that the internal structure of a Term is well-formed and that it passes all of the rules of the SAWCore type checker.

• type : Term -> Type returns the type of a particular Term, which can then be used to, for example, construct a new fresh variable with fresh_symbolic.

Loading and Storing Terms

Most frequently, Term values in SAWScript come from Cryptol, JVM, or LLVM programs, or some transformation thereof. However, it is also possible to obtain them from various other sources.

• parse_core : String -> Term parses a String containing a term in SAWCore syntax, returning a Term.

• read_core : String -> TopLevel Term is like parse_core, but obtains the text from the given file and expects it to be in the simpler SAWCore external representation format, rather than the human-readable syntax shown so far.

• read_aig : String -> TopLevel Term returns a Term representation of an And-Inverter-Graph (AIG) file in AIGER format.

• read_bytes : String -> TopLevel Term reads a constant sequence of bytes from a file and represents it as a Term. Its result will always have Cryptol type [n][8] for some n.

It is also possible to write Term values into files in various formats, including: AIGER (write_aig), CNF (write_cnf), SAWCore external representation (write_core), and SMT-Lib version 2 (write_smtlib2).

• write_aig : String -> Term -> TopLevel ()

• write_cnf : String -> Term -> TopLevel ()

• write_core : String -> Term -> TopLevel ()

• write_smtlib2 : String -> Term -> TopLevel ()

Proofs about Terms

The goal of SAW is to facilitate proofs about the behavior of programs. It may be useful to prove some small fact to use as a rewrite rule in later proofs, but ultimately these rewrite rules come together into a proof of some higher-level property about a software system.

Whether proving small lemmas (in the form of rewrite rules) or a top-level theorem, the process builds on the idea of a proof script that is run by one of the top level proof commands.

• prove_print : ProofScript () -> Term -> TopLevel Theorem takes a proof script (which we’ll describe next) and a Term. The Term should be of function type with a return value of Bool (Bit at the Cryptol level). It will then use the proof script to attempt to show that the Term returns True for all possible inputs. If it is successful, it will print Valid and return a Theorem. If not, it will abort.

• sat_print : ProofScript () -> Term -> TopLevel () is similar except that it looks for a single value for which the Term evaluates to True and prints out that value, returning nothing.

• prove_core : ProofScript () -> String -> TopLevel Theorem proves and returns a Theorem from a string in SAWCore syntax.

Automated Tactics

The simplest proof scripts just specify the automated prover to use. The ProofScript values abc and z3 select the ABC and Z3 theorem provers, respectively, and are typically good choices.

For example, combining prove_print with abc:

sawscript> t <- prove_print abc {{ \(x:[8]) -> x+x == x*2 }}
Valid
sawscript> t
Theorem (let { x@1 = Prelude.Vec 8 Prelude.Bool
      x@2 = Cryptol.TCNum 8
      x@3 = Cryptol.PArithSeqBool x@2
    }
 in (x : x@1)
-> Prelude.EqTrue
     (Cryptol.ecEq x@1 (Cryptol.PCmpSeqBool x@2)
        (Cryptol.ecPlus x@1 x@3 x x)
        (Cryptol.ecMul x@1 x@3 x
           (Cryptol.ecNumber (Cryptol.TCNum 2) x@1
              (Cryptol.PLiteralSeqBool x@2)))))

Similarly, sat_print will show that the function returns True for one specific input (which it should, since we already know it returns True for all inputs):

sawscript> sat_print abc {{ \(x:[8]) -> x+x == x*2 }}
Sat: [x = 0]

In addition to these, the boolector, cvc4, cvc5, mathsat, and yices provers are available. The internal decision procedure rme, short for Reed-Muller Expansion, is an automated prover that works particularly well on the Galois field operations that show up, for example, in AES.

In more complex cases, some pre-processing can be helpful or necessary before handing the problem off to an automated prover. The pre-processing can involve rewriting, beta reduction, unfolding, the use of provers that require slightly more configuration, or the use of provers that do very little real work.

Proof Script Diagnostics

During development of a proof, it can be useful to print various information about the current goal. The following tactics are useful in that context.

• print_goal : ProofScript () prints the entire goal in SAWCore syntax.

• print_goal_consts : ProofScript () prints a list of unfoldable constants in the current goal.

• print_goal_depth : Int -> ProofScript () takes an integer argument, n, and prints the goal up to depth n. Any elided subterms are printed with a ... notation.

• print_goal_size : ProofScript () prints the number of nodes in the DAG representation of the goal.

Rewriting in Proof Scripts

One of the key techniques available for completing proofs in SAWScript is the use of rewriting or transformation. The following commands support this approach.

• simplify : Simpset -> ProofScript () works just like rewrite, except that it works in a ProofScript context and implicitly transforms the current (unnamed) goal rather than taking a Term as a parameter.

• goal_eval : ProofScript () will evaluate the current proof goal to a first-order combination of primitives.

• goal_eval_unint : [String] -> ProofScript () works like goal_eval but avoids expanding or simplifying the given names.

Other Transformations

Some useful transformations are not easily specified using equality statements, and instead have special tactics.

• beta_reduce_goal : ProofScript () works like beta_reduce_term but on the current goal. It takes any sub-expression of the form (\x -> t) v and replaces it with a transformed version of t in which all instances of x are replaced by v.

• unfolding : [String] -> ProofScript () works like unfold_term but on the current goal.

Using unfolding is mostly valuable for proofs based entirely on rewriting, since the default behavior for automated provers is to unfold everything before sending a goal to a prover. However, with some provers it is possible to indicate that specific named subterms should be represented as uninterpreted functions.

• unint_cvc4 : [String] -> ProofScript ()

• unint_cvc5 : [String] -> ProofScript ()

• unint_yices : [String] -> ProofScript ()

• unint_z3 : [String] -> ProofScript ()

The list of String arguments in these cases indicates the names of the subterms to leave folded, and therefore present as uninterpreted functions to the prover. To determine which folded constants appear in a goal, use the print_goal_consts function described above.

Ultimately, we plan to implement a more generic tactic that leaves certain constants uninterpreted in whatever prover is ultimately used (provided that uninterpreted functions are expressible in the prover).

Note that each of the unint_* tactics have variants that are prefixed with sbv_ and w4_. The sbv_-prefixed tactics make use of the SBV library to represent and solve SMT queries:

• sbv_unint_cvc4 : [String] -> ProofScript ()

• sbv_unint_cvc5 : [String] -> ProofScript ()

• sbv_unint_yices : [String] -> ProofScript ()

• sbv_unint_z3 : [String] -> ProofScript ()

The w4_-prefixed tactics make use of the What4 library instead of SBV:

• w4_unint_cvc4 : [String] -> ProofScript ()

• w4_unint_cvc5 : [String] -> ProofScript ()

• w4_unint_yices : [String] -> ProofScript ()

• w4_unint_z3 : [String] -> ProofScript ()

In most specifications, the choice of SBV versus What4 is not important, as both libraries are broadly compatible in terms of functionality. There are some situations where one library may outpeform the other, however, due to differences in how each library represents certain SMT queries. There are also some experimental features that are only supported with What4 at the moment, such as enable_lax_loads_and_stores.

Caching Solver Results

SAW has the capability to cache the results of tactics which call out to automated provers. This can save a considerable amount of time in cases such as proof development and CI, where the same proof scripts are often run repeatedly without changes.

This caching is available for all tactics which call out to automated provers at runtime: abc, boolector, cvc4, cvc5, mathsat, yices, z3, rme, and the family of unint tactics described in the previous section.

When solver caching is enabled and one of the tactics mentioned above is encountered, if there is already an entry in the cache corresponding to the call then the cached result is used, otherwise the appropriate solver is queried, and the result saved to the cache. Entries are indexed by a SHA256 hash of the exact query to the solver (ignoring variable names), any options passed to the solver, and the names and full version strings of all the solver backends involved (e.g. ABC and SBV for the abc tactic). This ensures cached results are only used when they would be identical to the result of actually running the tactic.

The simplest way to enable solver caching is to set the environment variable SAW_SOLVER_CACHE_PATH. With this environment variable set, saw and saw-remote-api will automatically keep an LMDB database at the given path containing the solver result cache. Setting this environment variable globally therefore creates a global, concurrency-safe solver result cache used by all newly created saw or saw-remote-api processes. Note that when this environment variable is set, SAW does not create a cache at the specified path until it is actually needed.

There are also a number of SAW commands related to solver caching.

• set_solver_cache_path is like setting SAW_SOLVER_CACHE_PATH for the remainder of the current session, but opens an LMDB database at the specified path immediately. If a cache is already in use in the current session (i.e. through a prior call to set_solver_cache_path or through SAW_SOLVER_CACHE_PATH being set and the cache being used at least once) then all entries in the cache already in use will be copied to the new cache being opened.

• clean_mismatched_versions_solver_cache will remove all entries in the solver result cache which were created using solver backend versions which do not match the versions in the current environment. This can be run after an update to clear out any old, unusable entries from the solver cache. This command can also be run directly from the command line through the --clean-mismatched-versions-solver-cache command-line option.

• print_solver_cache prints to the console all entries in the cache whose SHA256 hash keys start with the given hex string. Providing an empty string results in all entries in the cache being printed.

• print_solver_cache_stats prints to the console statistics including the size of the solver cache, where on disk it is stored, and some counts of how often it has been used during the current session.

For performing more complicated database operations on the set of cached results, the file solver_cache.py is provided with the Python bindings of the SAW Remote API. This file implements a general-purpose Python interface for interacting with the LMDB databases kept by SAW for solver caching.

Below is an example of using solver caching with saw -v Debug. Only the relevant output is shown, the rest abbreviated with “…”.

sawscript> set_solver_cache_path "example.cache"
sawscript> prove_print z3 {{ \(x:[8]) -> x+x == x*2 }}
[22:13:00.832] Caching result: d1f5a76e7a0b7c01 (SBV 9.2, Z3 4.8.7 - 64 bit)
...
sawscript> prove_print z3 {{ \(new:[8]) -> new+new == new*2 }}
[22:13:04.122] Using cached result: d1f5a76e7a0b7c01 (SBV 9.2, Z3 4.8.7 - 64 bit)
...
sawscript> prove_print (w4_unint_z3_using "qfnia" []) \
                                  {{ \(x:[8]) -> x+x == x*2 }}
[22:13:09.484] Caching result: 4ee451f8429c2dfe (What4 v1.3-29-g6c462cd using qfnia, Z3 4.8.7 - 64 bit)
...
sawscript> print_solver_cache "d1f5a76e7a0b7c01"
[22:13:13.250] SHA: d1f5a76e7a0b7c01bdfe7d0e1be82b4f233a805ae85a287d45933ed12a54d3eb
[22:13:13.250] - Result: unsat
[22:13:13.250] - Solver: "SBV->Z3"
[22:13:13.250] - Versions: SBV 9.2, Z3 4.8.7 - 64 bit
[22:13:13.250] - Last used: 2023-07-25 22:13:04.120351 UTC

sawscript> print_solver_cache "4ee451f8429c2dfe"
[22:13:16.727] SHA: 4ee451f8429c2dfefecb6216162bd33cf053f8e66a3b41833193529449ef5752
[22:13:16.727] - Result: unsat
[22:13:16.727] - Solver: "W4 ->z3"
[22:13:16.727] - Versions: What4 v1.3-29-g6c462cd using qfnia, Z3 4.8.7 - 64 bit
[22:13:16.727] - Last used: 2023-07-25 22:13:09.484464 UTC

sawscript> print_solver_cache_stats
[22:13:20.585] == Solver result cache statistics ==
[22:13:20.585] - 2 results cached in example.cache
[22:13:20.585] - 2 insertions into the cache so far this run (0 failed attempts)
[22:13:20.585] - 1 usage of cached results so far this run (0 failed attempts)

Other External Provers

In addition to the built-in automated provers already discussed, SAW supports more generic interfaces to other arbitrary theorem provers supporting specific interfaces.

• external_aig_solver : String -> [String] -> ProofScript () supports theorem provers that can take input as a single-output AIGER file. The first argument is the name of the executable to run. The second argument is the list of command-line parameters to pass to that executable. Any element of this list equal to "%f" will be replaced with the name of the temporary AIGER file generated for the proof goal. The output from the solver is expected to be in DIMACS solution format.

• external_cnf_solver : String -> [String] -> ProofScript () works similarly but for SAT solvers that take input in DIMACS CNF format and produce output in DIMACS solution format.

Offline Provers

For provers that must be invoked in more complex ways, or to defer proof until a later time, there are functions to write the current goal to a file in various formats, and then assume that the goal is valid through the rest of the script.

• offline_aig : String -> ProofScript ()

• offline_cnf : String -> ProofScript ()

• offline_extcore : String -> ProofScript ()

• offline_smtlib2 : String -> ProofScript ()

• offline_unint_smtlib2 : [String] -> String -> ProofScript ()

These support the AIGER, DIMACS CNF, shared SAWCore, and SMT-Lib v2 formats, respectively. The shared representation for SAWCore is described in the saw-script repository. The offline_unint_smtlib2 command represents the folded subterms listed in its first argument as uninterpreted functions.

Finishing Proofs without External Solvers

Some proofs can be completed using unsound placeholders, or using techniques that do not require significant computation.

• assume_unsat : ProofScript () indicates that the current goal should be assumed to be unsatisfiable. This is an alias for assume_valid. Users should prefer to use admit instead.

• assume_valid : ProofScript () indicates that the current goal should be assumed to be valid. Users should prefer to use admit instead

• admit : String -> ProofScript () indicates that the current goal should be assumed to be valid without proof. The given string should be used to record why the user has decided to assume this proof goal.

• quickcheck : Int -> ProofScript () runs the goal on the given number of random inputs, and succeeds if the result of evaluation is always True. This is unsound, but can be helpful during proof development, or as a way to provide some evidence for the validity of a specification believed to be true but difficult or infeasible to prove.

• trivial : ProofScript () states that the current goal should be trivially true. This tactic recognizes instances of equality that can be demonstrated by conversion alone. In particular it is able to prove EqTrue x goals where x reduces to the constant value True. It fails if this is not the case.

Multiple Goals

The proof scripts shown so far all have a single implicit goal. As in many other interactive provers, however, SAWScript proofs can have multiple goals. The following commands can introduce or work with multiple goals. These are experimental and can be used only after enable_experimental has been called.

• goal_apply : Theorem -> ProofScript () will apply a given introduction rule to the current goal. This will result in zero or more new subgoals.

• goal_assume : ProofScript Theorem will convert the first hypothesis in the current proof goal into a local Theorem

• goal_insert : Theorem -> ProofScript () will insert a given Theorem as a new hypothesis in the current proof goal.

• goal_intro : String -> ProofScript Term will introduce a quantified variable in the current proof goal, returning the variable as a Term.

• goal_when : String -> ProofScript () -> ProofScript () will run the given proof script only when the goal name contains the given string.

• goal_exact : Term -> ProofScript () will attempt to use the given term as an exact proof for the current goal. This tactic will succeed whever the type of the given term exactly matches the current goal, and will fail otherwise.

• split_goal : ProofScript () will split a goal of the form Prelude.and prop1 prop2 into two separate goals prop1 and prop2.

Proof Failure and Satisfying Assignments

The prove_print and sat_print commands print out their essential results (potentially returning a Theorem in the case of prove_print). In some cases, though, one may want to act programmatically on the result of a proof rather than displaying it.

The prove and sat commands allow this sort of programmatic analysis of proof results. To allow this, they use two types we haven’t mentioned yet: ProofResult and SatResult. These are different from the other types in SAWScript because they encode the possibility of two outcomes. In the case of ProofResult, a statement may be valid or there may be a counter-example. In the case of SatResult, there may be a satisfying assignment or the statement may be unsatisfiable.

• prove : ProofScript SatResult -> Term -> TopLevel ProofResult

• sat : ProofScript SatResult -> Term -> TopLevel SatResult

To operate on these new types, SAWScript includes a pair of functions:

• caseProofResult : {b} ProofResult -> b -> (Term -> b) -> b takes a ProofResult, a value to return in the case that the statement is valid, and a function to run on the counter-example, if there is one.

• caseSatResult : {b} SatResult -> b -> (Term -> b) -> b has the same shape: it returns its first argument if the result represents an unsatisfiable statement, or its second argument applied to a satisfying assignment if it finds one.

AIG Values and Proofs

Most SAWScript programs operate on Term values, and in most cases this is the appropriate representation. It is possible, however, to represent the same function that a Term may represent using a different data structure: an And-Inverter-Graph (AIG). An AIG is a representation of a Boolean function as a circuit composed entirely of AND gates and inverters. Hardware synthesis and verification tools, including the ABC tool that SAW has built in, can do efficient verification and particularly equivalence checking on AIGs.

To take advantage of this capability, a handful of built-in commands can operate on AIGs.

• bitblast : Term -> TopLevel AIG represents a Term as an AIG by “blasting” all of its primitive operations (things like bit-vector addition) down to the level of individual bits.

• load_aig : String -> TopLevel AIG loads an AIG from an external AIGER file.

• save_aig : String -> AIG -> TopLevel () saves an AIG to an external AIGER file.

• save_aig_as_cnf : String -> AIG -> TopLevel () writes an AIG out in CNF format for input into a standard SAT solver.

Symbolic Execution

Analysis of Java and LLVM within SAWScript relies heavily on symbolic execution, so some background on how this process works can help with understanding the behavior of the available built-in functions.

At the most abstract level, symbolic execution works like normal program execution except that the values of all variables within the program can be arbitrary expressions, potentially containing free variables, rather than concrete values. Therefore, each symbolic execution corresponds to some set of possible concrete executions.

As a concrete example, consider the following C program that returns the maximum of two values:

unsigned int max(unsigned int x, unsigned int y) {
    if (y > x) {
        return y;
    } else {
        return x;
    }
}

If you call this function with two concrete inputs, like this:

int r = max(5, 4);

then it will assign the value 5 to r. However, we can also consider what it will do for arbitrary inputs. Consider the following example:

int r = max(a, b);

where a and b are variables with unknown values. It is still possible to describe the result of the max function in terms of a and b. The following expression describes the value of r:

ite (b > a) b a

where ite is the “if-then-else” mathematical function, which based on the value of the first argument returns either the second or third. One subtlety of constructing this expression, however, is the treatment of conditionals in the original program. For any concrete values of a and b, only one branch of the if statement will execute. During symbolic execution, on the other hand, it is necessary to execute both branches, track two different program states (each composed of symbolic values), and then merge those states after executing the if statement. This merging process takes into account the original branch condition and introduces the ite expression.

A symbolic execution system, then, is very similar to an interpreter that has a different notion of what constitutes a value and executes all paths through the program instead of just one. Therefore, the execution process is similar to that of a normal interpreter, and the process of generating a model for a piece of code is similar to building a test harness for that same code.

More specifically, the setup process for a test harness typically takes the following form:

• Initialize or allocate any resources needed by the code. For Java and LLVM code, this typically means allocating memory and setting the initial values of variables.

• Execute the code.

• Check the desired properties of the system state after the code completes.

Accordingly, three pieces of information are particularly relevant to the symbolic execution process, and are therefore needed as input to the symbolic execution system:

• The initial (potentially symbolic) state of the system.

• The code to execute.

• The final state of the system, and which parts of it are relevant to the properties being tested.

In the following sections, we describe how the Java and LLVM analysis primitives work in the context of these key concepts. We start with the simplest situation, in which the structure of the initial and final states can be directly inferred, and move on to more complex cases that require more information from the user.

Symbolic Termination

Above we described the process of executing multiple branches and merging the results when encountering a conditional statement in the program. When a program contains loops, the branch that chooses to continue or terminate a loop could go either way. Therefore, without a bit more information, the most obvious implementation of symbolic execution would never terminate when executing programs that contain loops.

The solution to this problem is to analyze the branch condition whenever considering multiple branches. If the condition for one branch can never be true in the context of the current symbolic state, there is no reason to execute that branch, and skipping it can make it possible for symbolic execution to terminate.

Directly comparing the branch condition to a constant can sometimes be enough to ensure termination. For example, in simple, bounded loops like the following, comparison with a constant is sufficient.

for (int i = 0; i < 10; i++) {
    // do something
}

In this case, the value of i is always concrete, and will eventually reach the value 10, at which point the branch corresponding to continuing the loop will be infeasible.

As a more complex example, consider the following function:

uint8_t f(uint8_t i) {
  int done = 0;
  while (!done) {
    if (i % 8 == 0) done = 1;
    i += 5;
  }
  return i;
}

The loop in this function can only be determined to symbolically terminate if the analysis takes into account algebraic rules about common multiples. Similarly, it can be difficult to prove that a base case is eventually reached for all inputs to a recursive program.

In this particular case, however, the code is guaranteed to terminate after a fixed number of iterations (where the number of possible iterations is a function of the number of bits in the integers being used). To show that the last iteration is in fact the last possible one, it’s necessary to do more than just compare the branch condition with a constant. Instead, we can use the same proof tools that we use to ultimately analyze the generated models to, early in the process, prove that certain branch conditions can never be true (i.e., are unsatisfiable).

Normally, most of the Java and LLVM analysis commands simply compare branch conditions to the constant True or False to determine whether a branch may be feasible. However, each form of analysis allows branch satisfiability checking to be turned on if needed, in which case functions like f above will terminate.

Next, we examine the details of the specific commands available to analyze JVM and LLVM programs.

Loading Code

The first step in analyzing any code is to load it into the system.

Loading LLVM

To load LLVM code, simply provide the location of a valid bitcode file to the llvm_load_module function.

• llvm_load_module : String -> TopLevel LLVMModule

The resulting LLVMModule can be passed into the various functions described below to perform analysis of specific LLVM functions.

The LLVM bitcode parser should generally work with LLVM versions between 3.5 and 16.0, though it may be incomplete for some versions. Debug metadata has changed somewhat throughout that version range, so is the most likely case of incompleteness. We aim to support every version after 3.5, however, so report any parsing failures as on GitHub.

Loading Java

Loading Java code is slightly more complex, because of the more structured nature of Java packages. First, when running saw, three flags control where to look for classes:

• The -b flag takes the path where the java executable lives, which is used to locate the Java standard library classes and add them to the class database. Alternatively, one can put the directory where java lives on the PATH, which SAW will search if -b is not set.

• The -j flag takes the name of a JAR file as an argument and adds the contents of that file to the class database.

• The -c flag takes the name of a directory as an argument and adds all class files found in that directory (and its subdirectories) to the class database. By default, the current directory is included in the class path.

Most Java programs will only require setting the -b flag (or the PATH), as that is enough to bring in the standard Java libraries. Note that when searching the PATH, SAW makes assumptions about where the standard library classes live. These assumptions are likely to hold on JDK 7 or later, but they may not hold on older JDKs on certain operating systems. If you are using an old version of the JDK and SAW is unable to find a standard Java class, you may need to specify the location of the standard classes’ JAR file with the -j flag (or, alternatively, with the SAW_JDK_JAR environment variable).

Once the class path is configured, you can pass the name of a class to the java_load_class function.

• java_load_class : String -> TopLevel JavaClass

The resulting JavaClass can be passed into the various functions described below to perform analysis of specific Java methods.

Java class files from any JDK newer than version 6 should work. However, support for JDK 9 and later is experimental. Verifying code that only uses primitive data types is known to work well, but there are some as-of-yet unresolved issues in verifying code involving classes such as String. For more information on these issues, refer to this GitHub issue.

Loading MIR

To load a piece of Rust code, first compile it to a MIR JSON file, as described in this section, and then provide the location of the JSON file to the mir_load_module function:

• mir_load_module : String -> TopLevel MIRModule

SAW currently supports Rust code that can be built with a January 23, 2023 Rust nightly. If you encounter a Rust feature that SAW does not support, please report it on GitHub.

Notes on Compiling Code for SAW

SAW will generally be able to load arbitrary LLVM bitcode, JVM bytecode, and MIR JSON files, but several guidelines can help make verification easier or more likely to succeed.

Compiling LLVM

For generating LLVM with clang, it can be helpful to:

• Turn on debugging symbols with -g so that SAW can find source locations of functions, names of variables, etc.

• Optimize with -O1 so that the generated bitcode more closely matches the C/C++ source, making the results more comprehensible.

• Use -fno-threadsafe-statics to prevent clang from emitting unnecessary pthread code.

• Link all relevant bitcode with llvm-link (including, e.g., the C++ standard library when analyzing C++ code).

All SAW proofs include side conditions to rule out undefined behavior, and proofs will only succeed if all of these side conditions have been discharged. However the default SAW notion of undefined behavior is with respect to the semantics of LLVM, rather than C or C++. If you want to rule out undefined behavior according to the C or C++ standards, consider compiling your code with -fsanitize=undefined or one of the related flags1 to clang.

Generally, you’ll also want to use -fsanitize-trap=undefined, or one of the related flags, to cause the compiled code to use llvm.trap to indicate the presence of undefined behavior. Otherwise, the compiled code will call a separate function, such as __ubsan_handle_shift_out_of_bounds, for each type of undefined behavior, and SAW currently does not have built in support for these functions (though you could manually create overrides for them in a verification script).

Compiling Java

For Java, the only compilation flag that tends to be valuable is -g to retain information about the names of function arguments and local variables.

Compiling MIR

In order to verify Rust code, SAW analyzes Rust’s MIR (mid-level intermediate representation) language. In particular, SAW analyzes a particular form of MIR that the mir-json tool produces. You will need to intall mir-json and run it on Rust code in order to produce MIR JSON files that SAW can load (see this section).

For cargo-based projects, mir-json provides a cargo subcommand called cargo saw-build that builds a JSON file suitable for use with SAW. cargo saw-build integrates directly with cargo, so you can pass flags to it like any other cargo subcommand. For example:

$ export SAW_RUST_LIBRARY_PATH=<...>
$ cargo saw-build <other cargo flags>
<snip>
linking 11 mir files into <...>/example-364cf2df365c7055.linked-mir.json
<snip>

Note that:

• The full output of cargo saw-build here is omitted. The important part is the .linked-mir.json file that appears after linking X mir files into, as that is the JSON file that must be loaded with SAW.

• SAW_RUST_LIBRARY_PATH should point to the the MIR JSON files for the Rust standard library.

mir-json also supports compiling individual .rs files through mir-json’s saw-rustc command. As the name suggests, it accepts all of the flags that rustc accepts. For example:

$ export SAW_RUST_LIBRARY_PATH=<...>
$ saw-rustc example.rs <other rustc flags>
<snip>
linking 11 mir files into <...>/example.linked-mir.json
<snip>

Notes on C++ Analysis

The distance between C++ code and LLVM is greater than between C and LLVM, so some additional considerations come into play when analyzing C++ code with SAW.

The first key issue is that the C++ standard library is large and complex, and tends to be widely used by C++ applications. To analyze most C++ code, it will be necessary to link your code with a version of the libc++ library2 compiled to LLVM bitcode. The wllvm program can3 be useful for this.

The C++ standard library includes a number of key global variables, and any code that touches them will require that they be initialized using llvm_alloc_global.

Many C++ names are slightly awkward to deal with in SAW. They may be mangled relative to the text that appears in the C++ source code. SAW currently only understands the mangled names. The llvm-nm program can be used to show the list of symbols in an LLVM bitcode file, and the c++filt program can be used to demangle them, which can help in identifying the symbol you want to refer to. In addition, C++ names from namespaces can sometimes include quote marks in their LLVM encoding. For example:

%"class.quux::Foo" = type { i32, i32 }

This can be mentioned in SAW by saying:

llvm_type "%\"class.quux::Foo\""

Finally, there is no support for calling constructors in specifications, so you will need to construct objects piece-by-piece using, e.g., llvm_alloc and llvm_points_to.

Direct Extraction

In the case of the max function described earlier, the relevant inputs and outputs are immediately apparent. The function takes two integer arguments, always uses both of them, and returns a single integer value, making no other changes to the program state.

In cases like this, a direct translation is possible, given only an identification of which code to execute. Two functions exist to handle such simple code. The first, for LLVM is the more stable of the two:

• llvm_extract : LLVMModule -> String -> TopLevel Term

A similar function exists for Java, but is more experimental.

• jvm_extract : JavaClass -> String -> TopLevel Term

Because of its lack of maturity, it (and later Java-related commands) must be enabled by running the enable_experimental command beforehand.

• enable_experimental : TopLevel ()

The structure of these two extraction functions is essentially identical. The first argument describes where to look for code (in either a Java class or an LLVM module, loaded as described in the previous section). The second argument is the name of the method or function to extract.

When the extraction functions complete, they return a Term corresponding to the value returned by the function or method as a function of its arguments.

These functions currently work only for code that takes some fixed number of integral parameters, returns an integral result, and does not access any dynamically-allocated memory (although temporary memory allocated during execution is allowed).

Creating Symbolic Variables

The direct extraction process just discussed automatically introduces symbolic variables and then abstracts over them, yielding a SAWScript Term that reflects the semantics of the original Java, LLVM, or MIR code. For simple functions, this is often the most convenient interface. For more complex code, however, it can be necessary (or more natural) to specifically introduce fresh variables and indicate what portions of the program state they correspond to.

• fresh_symbolic : String -> Type -> TopLevel Term is responsible for creating new variables in this context. The first argument is a name used for pretty-printing of terms and counter-examples. In many cases it makes sense for this to be the same as the name used within SAWScript, as in the following:

x <- fresh_symbolic "x" ty;

However, using the same name is not required.

The second argument to fresh_symbolic is the type of the fresh variable. Ultimately, this will be a SAWCore type; however, it is usually convenient to specify it using Cryptol syntax with the type quoting brackets {| and |}. For example, creating a 32-bit integer, as might be used to represent a Java int or an LLVM i32, can be done as follows:

x <- fresh_symbolic "x" {| [32] |};

Although symbolic execution works best on symbolic variables, which are “unbound” or “free”, most of the proof infrastructure within SAW uses variables that are bound by an enclosing lambda expression. Given a Term with free symbolic variables, we can construct a lambda term that binds them in several ways.

• abstract_symbolic : Term -> Term finds all symbolic variables in the Term and constructs a lambda expression binding each one, in some order. The result is a function of some number of arguments, one for each symbolic variable. It is the simplest but least flexible way to bind symbolic variables.

sawscript> x <- fresh_symbolic "x" {| [8] |}
sawscript> let t = {{ x + x }}
sawscript> print_term t
let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in Cryptol.ecPlus x@1 (Cryptol.PArithSeqBool (Cryptol.TCNum 8))
      x
      x
sawscript> let f = abstract_symbolic t
sawscript> print_term f
let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in \(x : x@1) ->
      Cryptol.ecPlus x@1 (Cryptol.PArithSeqBool (Cryptol.TCNum 8)) x x

If there are multiple symbolic variables in the Term passed to abstract_symbolic, the ordering of parameters can be hard to predict. In some cases (such as when a proof is the immediate next step, and it’s expected to succeed) the order isn’t important. In others, it’s nice to have more control over the order.

• lambda : Term -> Term -> Term is the building block for controlled binding. It takes two terms: the one to transform, and the portion of the term to abstract over. Generally, the first Term is one obtained from fresh_symbolic and the second is a Term that would be passed to abstract_symbolic.

sawscript> let f = lambda x t
sawscript> print_term f
let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in \(x : x@1) ->
      Cryptol.ecPlus x@1 (Cryptol.PArithSeqBool (Cryptol.TCNum 8)) x x

• lambdas : [Term] -> Term -> Term allows you to list the order in which symbolic variables should be bound. Consider, for example, a Term which adds two symbolic variables:

sawscript> x1 <- fresh_symbolic "x1" {| [8] |}
sawscript> x2 <- fresh_symbolic "x2" {| [8] |}
sawscript> let t = {{ x1 + x2 }}
sawscript> print_term t
let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in Cryptol.ecPlus x@1 (Cryptol.PArithSeqBool (Cryptol.TCNum 8))
      x1
      x2

We can turn t into a function that takes x1 followed by x2:

sawscript> let f1 = lambdas [x1, x2] t
sawscript> print_term f1
let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in \(x1 : x@1) ->
      \(x2 : x@1) ->
        Cryptol.ecPlus x@1 (Cryptol.PArithSeqBool (Cryptol.TCNum 8)) x1
          x2

Or we can turn t into a function that takes x2 followed by x1:

sawscript> let f1 = lambdas [x2, x1] t
sawscript> print_term f1
let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in \(x2 : x@1) ->
      \(x1 : x@1) ->
        Cryptol.ecPlus x@1 (Cryptol.PArithSeqBool (Cryptol.TCNum 8)) x1
          x2

Specification-Based Verification

The built-in functions described so far work by extracting models of code that can then be used for a variety of purposes, including proofs about the properties of the code.

When the goal is to prove equivalence between some LLVM, Java, or MIR code and a specification, however, a more declarative approach is sometimes convenient. The following sections describe an approach that combines model extraction and verification with respect to a specification. A verified specification can then be used as input to future verifications, allowing the proof process to be decomposed.

Running a Verification

Verification of LLVM is controlled by the llvm_verify command.

llvm_verify :
  LLVMModule ->
  String ->
  [CrucibleMethodSpec] ->
  Bool ->
  LLVMSetup () ->
  ProofScript SatResult ->
  TopLevel CrucibleMethodSpec

The first two arguments specify the module and function name to verify, as with llvm_verify. The third argument specifies the list of already-verified specifications to use for compositional verification (described later; use [] for now). The fourth argument specifies whether to do path satisfiability checking, and the fifth gives the specification of the function to be verified. Finally, the last argument gives the proof script to use for verification. The result is a proved specification that can be used to simplify verification of functions that call this one.

Similar commands are available for JVM programs:

jvm_verify :
  JavaClass ->
  String ->
  [JVMMethodSpec] ->
  Bool ->
  JVMSetup () ->
  ProofScript SatResult ->
  TopLevel JVMMethodSpec

And for MIR programs:

mir_verify :
  MIRModule ->
  String ->
  [MIRSpec] ->
  Bool ->
  MIRSetup () ->
  ProofScript () ->
  TopLevel MIRSpec

Running a MIR-based verification

(Note: API functions involving MIR verification require enable_experimental in order to be used. As such, some parts of this API may change before being finalized.)

The String supplied as an argument to mir_verify is expected to be a function identifier. An identifier is expected adhere to one of the following conventions:

• <crate name>/<disambiguator>::<function path>

• <crate name>::<function path>

Where:

• <crate name> is the name of the crate in which the function is defined. (If you produced your MIR JSON file by compiling a single .rs file with saw-rustc, then the crate name is the same as the name of the file, but without the .rs file extension.)

• <disambiguator> is a hash of the crate and its dependencies. In extreme cases, it is possible for two different crates to have identical crate names, in which case the disambiguator must be used to distinguish between the two crates. In the common case, however, most crate names will correspond to exactly one disambiguator, and you are allowed to leave out the /<disambiguator> part of the String in this case. If you supply an identifier with an ambiguous crate name and omit the disambiguator, then SAW will raise an error.

• <function path> is the path to the function within the crate. Sometimes, this is as simple as the function name itself. In other cases, a function path may involve multiple segments, depending on the module hierarchy for the program being verified. For instance, a read function located in core/src/ptr/mod.rs will have the identifier:

  Copy

  core::ptr::read

  Where core is the crate name and ptr::read is the function path, which has two segments ptr and read. There are also some special forms of segments that appear for functions defined in certain language constructs. For instance, if a function is defined in an impl block, then it will have {impl} as one of its segments, e.g.,

  Copy

  core::ptr::const_ptr::{impl}::offset

  If you are in doubt about what the full identifier for a given function is, consult the MIR JSON file for your program.

Now we describe how to construct a value of type LLVMSetup (), JVMSetup (), or MIRSetup ().

Structure of a Specification

A specifications for Crucible consists of three logical components:

• A specification of the initial state before execution of the function.

• A description of how to call the function within that state.

• A specification of the expected final value of the program state.

These three portions of the specification are written in sequence within a do block of type {LLVM,JVM,MIR}Setup. The command {llvm,jvm,mir}_execute_func separates the specification of the initial state from the specification of the final state, and specifies the arguments to the function in terms of the initial state. Most of the commands available for state description will work either before or after {llvm,jvm,mir}_execute_func, though with slightly different meaning, as described below.

Creating Fresh Variables

In any case where you want to prove a property of a function for an entire class of inputs (perhaps all inputs) rather than concrete values, the initial values of at least some elements of the program state must contain fresh variables. These are created in a specification with the {llvm,jvm,mir}_fresh_var commands rather than fresh_symbolic.

• llvm_fresh_var : String -> LLVMType -> LLVMSetup Term

• jvm_fresh_var : String -> JavaType -> JVMSetup Term

• mir_fresh_var : String -> MIRType -> MIRSetup Term

The first parameter to both functions is a name, used only for presentation. It’s possible (though not recommended) to create multiple variables with the same name, but SAW will distinguish between them internally. The second parameter is the LLVM, Java, or MIR type of the variable. The resulting Term can be used in various subsequent commands.

Note that the second parameter to {llvm,jvm,mir}_fresh_var must be a type that has a counterpart in Cryptol. (For more information on this, refer to the “Cryptol type correspondence” section.) If the type does not have a Cryptol counterpart, the function will raise an error. If you do need to create a fresh value of a type that cannot be represented in Cryptol, consider using a function such as llvm_fresh_expanded_val (for LLVM verification) or mir_fresh_expanded_value (for MIR verification).

LLVM types are built with this set of functions:

• llvm_int : Int -> LLVMType

• llvm_alias : String -> LLVMType

• llvm_array : Int -> LLVMType -> LLVMType

• llvm_float : LLVMType

• llvm_double : LLVMType

• llvm_packed_struct : [LLVMType] -> LLVMType

• llvm_struct : [LLVMType] -> LLVMType

Java types are built up using the following functions:

• java_bool : JavaType

• java_byte : JavaType

• java_char : JavaType

• java_short : JavaType

• java_int : JavaType

• java_long : JavaType

• java_float : JavaType

• java_double : JavaType

• java_class : String -> JavaType

• java_array : Int -> JavaType -> JavaType

MIR types are built up using the following functions:

• mir_adt : MIRAdt -> MIRType

• mir_array : Int -> MIRType -> MIRType

• mir_bool : MIRType

• mir_char : MIRType

• mir_i8 : MIRType

• mir_i6 : MIRType

• mir_i32 : MIRType

• mir_i64 : MIRType

• mir_i128 : MIRType

• mir_isize : MIRType

• mir_f32 : MIRType

• mir_f64 : MIRType

• mir_lifetime : MIRType

• mir_ref : MIRType -> MIRType

• mir_ref_mut : MIRType -> MIRType

• mir_slice : MIRType -> MIRType

• mir_str : MIRType

• mir_tuple : [MIRType] -> MIRType

• mir_u8 : MIRType

• mir_u6 : MIRType

• mir_u32 : MIRType

• mir_u64 : MIRType

• mir_u128 : MIRType

• mir_usize : MIRType

Most of these types are straightforward mappings to the standard LLVM and Java types. The one key difference is that arrays must have a fixed, concrete size. Therefore, all analysis results are valid only under the assumption that any arrays have the specific size indicated, and may not hold for other sizes.

The llvm_int function takes an Int parameter indicating the variable’s bit width. For example, the C uint16_t and int16_t types correspond to llvm_int 16. The C bool type is slightly trickier. A bare bool type typically corresponds to llvm_int 1, but if a bool is a member of a composite type such as a pointer, array, or struct, then it corresponds to llvm_int 8. This is due to a peculiarity in the way Clang compiles bool down to LLVM. When in doubt about how a bool is represented, check the LLVM bitcode by compiling your code with clang -S -emit-llvm.

LLVM types can also be specified in LLVM syntax directly by using the llvm_type function.

• llvm_type : String -> LLVMType

For example, llvm_type "i32" yields the same result as llvm_int 32.

The most common use for creating fresh variables is to state that a particular function should have the specified behaviour for arbitrary initial values of the variables in question. Sometimes, however, it can be useful to specify that a function returns (or stores, more about this later) an arbitrary value, without specifying what that value should be. To express such a pattern, you can also run llvm_fresh_var from the post state (i.e., after llvm_execute_func).

The SetupValue and JVMValue Types

Many specifications require reasoning about both pure values and about the configuration of the heap. The SetupValue type corresponds to values that can occur during symbolic execution, which includes both Term values, pointers, and composite types consisting of either of these (both structures and arrays).

The llvm_term, jvm_term, and mir_term functions create a SetupValue, JVMValue, or MIRValue, respectively, from a Term:

• llvm_term : Term -> SetupValue

• jvm_term : Term -> JVMValue

• mir_term : Term -> MIRValue

The value that these functions return will have an LLVM, JVM, or MIR type corresponding to the Cryptol type of the Term argument. (For more information on this, refer to the “Cryptol type correspondence” section.) If the type does not have a Cryptol counterpart, the function will raise an error.

Cryptol type correspondence

The {llvm,jvm,mir}_fresh_var functions take an LLVM, JVM, or MIR type as an argument and produces a Term variable of the corresponding Cryptol type as output. Similarly, the {llvm,jvm,mir}_term functions take a Cryptol Term as input and produce a value of the corresponding LLVM, JVM, or MIR type as output. This section describes precisely which types can be converted to Cryptol types (and vice versa) in this way.

LLVM verification

The following LLVM types correspond to Cryptol types:

• llvm_alias <name>: Corresponds to the same Cryptol type as the type used in the definition of <name>.

• llvm_array <n> <ty>: Corresponds to the Cryptol sequence [<n>][<cty>], where <cty> is the Cryptol type corresponding to <ty>.

• llvm_int <n>: Corresponds to the Cryptol word [<n>].

• llvm_struct [<ty_1>, ..., <ty_n>] and llvm_packed_struct [<ty_1>, ..., <ty_n>]: Corresponds to the Cryptol tuple (<cty_1>, ..., <cty_n>), where <cty_i> is the Cryptol type corresponding to <ty_i> for each i ranging from 1 to n.

The following LLVM types do not correspond to Cryptol types:

• llvm_double

• llvm_float

• llvm_pointer

JVM verification

The following Java types correspond to Cryptol types:

• java_array <n> <ty>: Corresponds to the Cryptol sequence [<n>][<cty>], where <cty> is the Cryptol type corresponding to <ty>.

• java_bool: Corresponds to the Cryptol Bit type.

• java_byte: Corresponds to the Cryptol [8] type.

• java_char: Corresponds to the Cryptol [16] type.

• java_int: Corresponds to the Cryptol [32] type.

• java_long: Corresponds to the Cryptol [64] type.

• java_short: Corresponds to the Cryptol [16] type.

The following Java types do not correspond to Cryptol types:

• java_class

• java_double

• java_float

MIR verification

The following MIR types correspond to Cryptol types:

• mir_array <n> <ty>: Corresponds to the Cryptol sequence [<n>][<cty>], where <cty> is the Cryptol type corresponding to <ty>.

• mir_bool: Corresponds to the Cryptol Bit type.

• mir_char: Corresponds to the Cryptol [32] type.

• mir_i8 and mir_u8: Corresponds to the Cryptol [8] type.

• mir_i16 and mir_u16: Corresponds to the Cryptol [16] type.

• mir_i32 and mir_u32: Corresponds to the Cryptol [32] type.

• mir_i64 and mir_u64: Corresponds to the Cryptol [64] type.

• mir_i128 and mir_u128: Corresponds to the Cryptol [128] type.

• mir_isize and mir_usize: Corresponds to the Cryptol [32] type.

• mir_tuple [<ty_1>, ..., <ty_n>]: Corresponds to the Cryptol tuple (<cty_1>, ..., <cty_n>), where <cty_i> is the Cryptol type corresponding to <ty_i> for each i ranging from 1 to n.

The following MIR types do not correspond to Cryptol types:

• mir_adt

• mir_f32

• mir_f64

• mir_ref and mir_ref_mut

• mir_slice

• mir_str

Executing

Once the initial state has been configured, the {llvm,jvm,mir}_execute_func command specifies the parameters of the function being analyzed in terms of the state elements already configured.

• llvm_execute_func : [SetupValue] -> LLVMSetup ()

• jvm_execute_func : [JVMValue] -> JVMSetup ()

• mir_execute_func : [MIRValue] -> MIRSetup ()

Return Values

To specify the value that should be returned by the function being verified use the {llvm,jvm,mir}_return command.

• llvm_return : SetupValue -> LLVMSetup ()

• jvm_return : JVMValue -> JVMSetup ()

• mir_return : MIRValue -> MIRSetup ()

A First Simple Example

The commands introuduced so far are sufficient to verify simple programs that do not use pointers (or that use them only internally). Consider, for instance the C program that adds its two arguments together:

#include <stdint.h>
uint32_t add(uint32_t x, uint32_t y) {
    return x + y;
}

We can specify this function’s expected behavior as follows:

let add_setup = do {
    x <- llvm_fresh_var "x" (llvm_int 32);
    y <- llvm_fresh_var "y" (llvm_int 32);
    llvm_execute_func [llvm_term x, llvm_term y];
    llvm_return (llvm_term {{ x + y : [32] }});
};

We can then compile the C file add.c into the bitcode file add.bc and verify it with ABC:

m <- llvm_load_module "add.bc";
add_ms <- llvm_verify m "add" [] false add_setup abc;

Compositional Verification

The primary advantage of the specification-based approach to verification is that it allows for compositional reasoning. That is, when proving properties of a given method or function, we can make use of properties we have already proved about its callees rather than analyzing them anew. This enables us to reason about much larger and more complex systems than otherwise possible.

The llvm_verify, jvm_verify, and mir_verify functions return values of type CrucibleMethodSpec, JVMMethodSpec, and MIRMethodSpec, respectively. These values are opaque objects that internally contain both the information provided in the associated LLVMSetup, JVMSetup, or MIRSetup blocks, respectively, and the results of the verification process.

Any of these MethodSpec objects can be passed in via the third argument of the ..._verify functions. For any function or method specified by one of these parameters, the simulator will not follow calls to the associated target. Instead, it will perform the following steps:

• Check that all llvm_points_to and llvm_precond statements (or the corresponding JVM or MIR statements) in the specification are satisfied.

• Update the simulator state and optionally construct a return value as described in the specification.

More concretely, building on the previous example, say we have a doubling function written in terms of add:

uint32_t dbl(uint32_t x) {
    return add(x, x);
}

It has a similar specification to add:

let dbl_setup = do {
    x <- llvm_fresh_var "x" (llvm_int 32);
    llvm_execute_func [llvm_term x];
    llvm_return (llvm_term {{ x + x : [32] }});
};

And we can verify it using what we’ve already proved about add:

llvm_verify m "dbl" [add_ms] false dbl_setup abc;

In this case, doing the verification compositionally doesn’t save computational effort, since the functions are so simple, but it illustrates the approach.

Compositional Verification and Mutable Allocations

A common pitfall when using compositional verification is to reuse a specification that underspecifies the value of a mutable allocation. In general, doing so can lead to unsound verification, so SAW goes through great lengths to check for this.

Here is an example of this pitfall in an LLVM verification. Given this C code:

void side_effect(uint32_t *a) {
  *a = 0;
}

uint32_t foo(uint32_t x) {
  uint32_t b = x;
  side_effect(&b);
  return b;
}

And the following SAW specifications:

let side_effect_spec = do {
  a_ptr <- llvm_alloc (llvm_int 32);
  a_val <- llvm_fresh_var "a_val" (llvm_int 32);
  llvm_points_to a_ptr (llvm_term a_val);

  llvm_execute_func [a_ptr];
};

let foo_spec = do {
  x <- llvm_fresh_var "x" (llvm_int 32);

  llvm_execute_func [llvm_term x];

  llvm_return (llvm_term x);
};

Should SAW be able to verify the foo function against foo_spec using compositional verification? That is, should the following be expected to work?

side_effect_ov <- llvm_verify m "side_effect" [] false side_effect_spec z3;
llvm_verify m "foo" [side_effect_ov] false foo_spec z3;

A literal reading of side_effect_spec would suggest that the side_effect function allocates a_ptr but then does nothing with it, implying that foo returns its argument unchanged. This is incorrect, however, as the side_effect function actually changes its argument to point to 0, so the foo function ought to return 0 as a result. SAW should not verify foo against foo_spec, and indeed it does not.

The problem is that side_effect_spec underspecifies the value of a_ptr in its postconditions, which can lead to the potential unsoundness seen above when side_effect_spec is used in compositional verification. To prevent this source of unsoundness, SAW will invalidate the underlying memory of any mutable pointers (i.e., those declared with llvm_alloc, not llvm_alloc_global) allocated in the preconditions of compositional override that do not have a corresponding llvm_points_to statement in the postconditions. Attempting to read from invalidated memory constitutes an error, as can be seen in this portion of the error message when attempting to verify foo against foo_spec:

invalidate (state of memory allocated in precondition (at side.saw:3:12) not described in postcondition)

To fix this particular issue, add an llvm_points_to statement to side_effect_spec:

let side_effect_spec = do {
  a_ptr <- llvm_alloc (llvm_int 32);
  a_val <- llvm_fresh_var "a_val" (llvm_int 32);
  llvm_points_to a_ptr (llvm_term a_val);

  llvm_execute_func [a_ptr];

  // This is new
  llvm_points_to a_ptr (llvm_term {{ 0 : [32] }});
};

After making this change, SAW will reject foo_spec for a different reason, as it claims that foo returns its argument unchanged when it actually returns 0.

Note that invalidating memory itself does not constitute an error, so if the foo function never read the value of b after calling side_effect(&b), then there would be no issue. It is only when a function attempts to read from invalidated memory that an error is thrown. In general, it can be difficult to predict when a function will or will not read from invalidated memory, however. For this reason, it is recommended to always specify the values of mutable allocations in the postconditions of your specs, as it can avoid pitfalls like the one above.

The same pitfalls apply to compositional MIR verification, with a couple of key differences. In MIR verification, mutable references are allocated using mir_alloc_mut. Here is a Rust version of the pitfall program above:

pub fn side_effect(a: &mut u32) {
    *a = 0;
}

pub fn foo(x: u32) -> u32 {
    let mut b: u32 = x;
    side_effect(&mut b);
    b
}

let side_effect_spec = do {
  a_ref <- mir_alloc_mut mir_u32;
  a_val <- mir_fresh_var "a_val" mir_u32;
  mir_points_to a_ref (mir_term a_val);

  mir_execute_func [a_ref];
};

let foo_spec = do {
  x <- mir_fresh_var "x" mir_u32;

  mir_execute_func [mir_term x];

  mir_return (mir_term {{ x }});
};

Just like above, if you attempted to prove foo against foo_spec using compositional verification:

side_effect_ov <- mir_verify m "test::side_effect" [] false side_effect_spec z3;
mir_verify m "test::foo" [side_effect_ov] false foo_spec z3;

Then SAW would throw an error, as side_effect_spec underspecifies the value of a_ref in its postconditions. side_effect_spec can similarly be repaired by adding a mir_points_to statement involving a_ref in side_effect_spec’s postconditions.

MIR verification differs slightly from LLVM verification in how it catches underspecified mutable allocations when using compositional overrides. The LLVM memory model achieves this by invalidating the underlying memory in underspecified allocations. The MIR memory model, on the other hand, does not have a direct counterpart to memory invalidation. As a result, any MIR overrides must specify the values of all mutable allocations in their postconditions, even if the function that calls the override never uses the allocations.

To illustrate this point more finely, suppose that the foo function had instead been defined like this:

pub fn foo(x: u32) -> u32 {
    let mut b: u32 = x;
    side_effect(&mut b);
    42
}

Here, it does not particularly matter what effects the side_effect function has on its argument, as foo will now return 42 regardless. Still, if you attempt to prove foo by using side_effect as a compositional override, then it is strictly required that you specify the value of side_effect’s argument in its postconditions, even though the answer that foo returns is unaffected by this. This is in contrast with LLVM verification, where one could get away without specifying side_effect’s argument in this example, as the invalidated memory in b would never be read.

Compositional Verification and Mutable Global Variables

Just like with local mutable allocations (see the previous section), specifications used in compositional overrides must specify the values of mutable global variables in their postconditions. To illustrate this using LLVM verification, here is a variant of the C program from the previous example that uses a mutable global variable a:

uint32_t a = 42;

void side_effect(void) {
  a = 0;
}

uint32_t foo(void) {
  side_effect();
  return a;
}

If we attempted to verify foo against this foo_spec specification using compositional verification:

let side_effect_spec = do {
  llvm_alloc_global "a";
  llvm_points_to (llvm_global "a") (llvm_global_initializer "a");

  llvm_execute_func [];
};

let foo_spec = do {
  llvm_alloc_global "a";
  llvm_points_to (llvm_global "a") (llvm_global_initializer "a");

  llvm_execute_func [];

  llvm_return (llvm_global_initializer "a");
};

side_effect_ov <- llvm_verify m "side_effect" [] false side_effect_spec z3;
llvm_verify m "foo" [side_effect_ov] false foo_spec z3;

Then SAW would reject it, as side_effect_spec does not specify what a’s value should be in its postconditions. Just as with local mutable allocations, SAW will invalidate the underlying memory in a, and subsequently reading from a in the foo function will throw an error. The solution is to add an llvm_points_to statement in the postconditions that declares that a’s value is set to 0.

The same concerns apply to MIR verification, where mutable global variables are referred to as static mut items. (See the MIR static items section for more information). Here is a Rust version of the program above:

static mut A: u32 = 42;

pub fn side_effect() {
    unsafe {
        A = 0;
    }
}

pub fn foo() -> u32 {
    side_effect();
    unsafe { A }
}

let side_effect_spec = do {
  mir_points_to (mir_static "test::A") (mir_static_initializer "test::A");

  mir_execute_func [];
};

let foo_spec = do {
  mir_points_to (mir_static "test::A") (mir_static_initializer "test::A");

  mir_execute_func [];

  mir_return (mir_static_initializer "test::A");
};

side_effect_ov <- mir_verify m "side_effect" [] false side_effect_spec z3;
mir_verify m "foo" [side_effect_ov] false foo_spec z3;

Just as above, we can repair this by adding a mir_points_to statement in side_effect_spec’s postconditions that specifies that A is set to 0.

Recall from the previous section that MIR verification is stricter than LLVM verification when it comes to specifying mutable allocations in the postconditions of compositional overrides. This is especially true for mutable static items. In MIR verification, any compositional overrides must specify the values of all mutable static items in the entire program in their postconditions, even if the function that calls the override never uses the static items. For example, if the foo function were instead defined like this:

pub fn foo() -> u32 {
    side_effect();
    42
}

Then it is still required for side_effect_spec to specify what A’s value will be in its postconditions, despite the fact that this has no effect on the value that foo will return.

Specifying Heap Layout

Most functions that operate on pointers expect that certain pointers point to allocated memory before they are called. The llvm_alloc command allows you to specify that a function expects a particular pointer to refer to an allocated region appropriate for a specific type.

• llvm_alloc : LLVMType -> LLVMSetup SetupValue

This command returns a SetupValue consisting of a pointer to the allocated space, which can be used wherever a pointer-valued SetupValue can be used.

In the initial state, llvm_alloc specifies that the function expects a pointer to allocated space to exist. In the final state, it specifies that the function itself performs an allocation.

When using the experimental Java implementation, separate functions exist for specifying that arrays or objects are allocated:

• jvm_alloc_array : Int -> JavaType -> JVMSetup JVMValue specifies an array of the given concrete size, with elements of the given type.

• jvm_alloc_object : String -> JVMSetup JVMValue specifies an object of the given class name.

The experimental MIR implementation also has a mir_alloc function, which behaves similarly to llvm_alloc. mir_alloc creates an immutable reference, but there is also a mir_alloc_mut function for creating a mutable reference:

• mir_alloc : MIRType -> MIRSetup MIRValue

• mir_alloc_mut : MIRType -> MIRSetup MIRValue

MIR tracks whether references are mutable or immutable at the type level, so it is important to use the right allocation command for a given reference type.

In LLVM, it’s also possible to construct fresh pointers that do not point to allocated memory (which can be useful for functions that manipulate pointers but not the values they point to):

• llvm_fresh_pointer : LLVMType -> LLVMSetup SetupValue

The NULL pointer is called llvm_null in LLVM and jvm_null in JVM:

• llvm_null : SetupValue

• jvm_null : JVMValue

One final, slightly more obscure command is the following:

• llvm_alloc_readonly : LLVMType -> LLVMSetup SetupValue

This works like llvm_alloc except that writes to the space allocated are forbidden. This can be useful for specifying that a function should take as an argument a pointer to allocated space that it will not modify. Unlike llvm_alloc, regions allocated with llvm_alloc_readonly are allowed to alias other read-only regions.

Specifying Heap Values

Pointers returned by llvm_alloc, jvm_alloc_{array,object}, or mir_alloc{,_mut} don’t initially point to anything. So if you pass such a pointer directly into a function that tried to dereference it, symbolic execution will fail with a message about an invalid load. For some functions, such as those that are intended to initialize data structures (writing to the memory pointed to, but never reading from it), this sort of uninitialized memory is appropriate. In most cases, however, it’s more useful to state that a pointer points to some specific (usually symbolic) value, which you can do with the points-to family of commands.

LLVM heap values

LLVM verification primarily uses the llvm_points_to command:

• llvm_points_to : SetupValue -> SetupValue -> LLVMSetup () takes two SetupValue arguments, the first of which must be a pointer, and states that the memory specified by that pointer should contain the value given in the second argument (which may be any type of SetupValue).

When used in the final state, llvm_points_to specifies that the given pointer should point to the given value when the function finishes.

Occasionally, because C programs frequently reinterpret memory of one type as another through casts, it can be useful to specify that a pointer points to a value that does not agree with its static type.

• llvm_points_to_untyped : SetupValue -> SetupValue -> LLVMSetup () works like llvm_points_to but omits type checking. Rather than omitting type checking across the board, we introduced this additional function to make it clear when a type reinterpretation is intentional. As an alternative, one may instead use llvm_cast_pointer to line up the static types.

JVM heap values

JVM verification has two categories of commands for specifying heap values. One category consists of the jvm_*_is commands, which allow users to directly specify what value a heap object points to. There are specific commands for each type of JVM heap object:

• jvm_array_is : JVMValue -> Term -> JVMSetup () declares that an array (the first argument) contains a sequence of values (the second argument).

• jvm_elem_is : JVMValue -> Int -> JVMValue -> JVMSetup () declares that an array (the first argument) has an element at the given index (the second argument) containing the given value (the third argument).

• jvm_field_is : JVMValue -> String -> JVMValue -> JVMSetup () declares that an object (the first argument) has a field (the second argument) containing the given value (the third argument).

• jvm_static_field_is : String -> JVMValue -> JVMSetup () declares that a named static field (the first argument) contains the given value (the second argument). By default, the field name is assumed to belong to the same class as the method being specified. Static fields belonging to other classes can be selected using the <classname>.<fieldname> syntax in the first argument.

Another category consists of the jvm_modifies_* commands. Like the jvm_*_is commands, these specify that a JVM heap object points to valid memory, but unlike the jvm_*_is commands, they leave the exact value being pointed to as unspecified. These are useful for writing partial specifications for methods that modify some heap value, but without saying anything specific about the new value.