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.

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.

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

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

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:

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.

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.

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.

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:

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.

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:

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:

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

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

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.

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.

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.

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.

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.

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:

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 . Galois maintains this book as Cryptol evolves.

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

Verification with SAW

The and describe small problems, similar in scope to , but use a somewhat different set of SAW features. They are good next steps after this document. After that, the 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 in .

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

symbolic value

testing

Term

verification

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.