Tutorial (Rust)
A tutorial on Rust verification with SAW
SAW is a special-purpose programming environment developed by Galois to help orchestrate and track the results of the large collection of proof tools necessary for analysis and verification of complex software artifacts.
SAW adopts the functional paradigm, and largely follows the structure of many other typed functional languages, with some special features specifically targeted at the coordination of verification and analysis tasks.
This tutorial introduces the details of the language by walking through several examples, and showing how simple verification tasks can be described. The complete examples are available on GitHub. Most of the examples make use of inline specifications written in Cryptol, a language originally designed for high-level descriptions of cryptographic algorithms. For readers unfamiliar with Cryptol, various documents describing its use are available here.
This tutorial also include a case study on how to use SAW to verify a real-world implementation of the Salsa20 stream cipher based on the stream-ciphers Rust project. The code for this case study is also available on GitHub.
Prerequisites
In order to run the examples in this tutorial, you will need to install the following prerequisite tools:
SAW itself, which can be installed by following the instructions here.
The
mir-jsontool, which can be installed by following the instructions here.
About mir-json
mir-jsonWe are interested in verifying code written in Rust, but Rust is an extremely rich programming language that has many distinct language features. To make the process of verifying Rust simpler, SAW targets an intermediate language used in the Rust compiler called MIR (short for “Mid-level IR”). MIR takes the variety of different features and syntactic extensions in Rust and boils them down to a minimal subset that is easier for a computer program to analyze.
The process of extracting MIR code that is suitable for SAW’s needs is somewhat tricky, so we wrote a suite of tools called mir-json to automate this process. mir-json provides a plugin for tools like rustc and cargo that lets you compile Rust code as you normally would and produce an additional .json file as output. This .json file contains the MIR code that was produced internally by the Rust compiler, with some additional minor tweaks to make it suitable for SAW’s needs.
mir-json is not a single tool but rather a suite of related tools that leverage the same underlying plugin. For SAW purposes, the two mir-json tools that are most relevant are:
saw-rustc: A thin wrapper aroundrustc(the Rust compiler), which is suitable for individual.rsfiles.cargo-saw-build: A thin wrapper around thecargo buildcommand, which is suitable forcargo-based Rust projects.
Most of the examples in this tutorial involve self-contained examples, which will use saw-rustc. Later in the tutorial, we will examine a Salsa20 case study that involves a cargo-based project, which will use cargo-saw-build.
A first example with saw-rustc
saw-rustcLet’s try out saw-rustc on a small example file, which we’ll name first-example.rs:
This is the identity function, but specialized to the type u8. We can compile this with saw-rustc like so:
saw-rustc prints out some additional information that rustc alone does not print, and we have displayed the parts of this information that are most interesting. In particular:
saw-rustcnotes that is isEmitting MIR for first_example/abef32c5::id_u8, wherefirst_example/abef32c5::id_u8is the full identifier used to uniquely refer to theid_u8function. It’s entirely possible that theabef32c5bit will look different on your machine; we’ll talk more about identifiers in the “Identifiers” section.Once
saw-rustcproduced a MIR JSON file namedfirst-example.linked-mir.json. This is an important bit of information, as SAW will ingest this JSON file.
If you’d like, you can inspect the first-example.linked-mir.json file with JSON tools (e.g., jq), but it is not important to understand everything that is going on there. This is machine-generated JSON, and as such, it is not meant to be particularly readable by human eyes.
The SAW_RUST_LIBRARY_PATH environment variable
SAW_RUST_LIBRARY_PATH environment variableRust has a large set of standard libraries that ship with the compiler, and parts of the standard library are quite low-level and tricky. SAW’s primary objective is to provide a tool that can analyze code in a tractable way. For this reason, SAW sometimes needs to invoke simplified versions of Rust standard library functions that are more reasonable for an SMT-based tool like SAW to handle. These simplified functions are equivalent in behavior, but avoid using problematic code patterns (e.g., gnarly pointer arithmetic or the transmute function).
If you are only ever compiling self-contained pieces of code with saw-rustc, there is a good chance that you can get away without needing to use SAW’s custom version of the Rust standard libraries. However, if you ever need to build something more complicated than that (e.g., the Salsa20 case study later in this tutorial), then you will need the custom libraries. For this reason, it is worthwhile to teach SAW the location of the custom libraries now.
At present, the best way to obtain the custom version of the Rust standard libraries is to perform the following steps:
Clone the
cruciblerepo like so:Navigate to the
crux-mirsubdirectory of thecruciblecheckout:Run the
translate_libs.shscript:This will compile the custom versions of the Rust standard libraries using
mir-json, placing the results under therlibssubdirectory.Finally, define a
SAW_RUST_LIBRARY_PATHenvironment variable that points to the newly createdrlibssubdirectory:
An upcoming release of SAW will include these custom libraries pre-built, which will greatly simplify the steps above. Either way, you will need to set the SAW_RUST_LIBRARY_PATH environment variable to point to the location of the custom libraries.
A note about generics
The id_u8 function above is likely not how most Rust programmers would define the identity function. Instead, it would seem more natural to define it generically, that is, by parameterizing the function by a type parameter:
If you compile this with saw-rustc, however, the resulting JSON file will lack a definition for id! We can see this by using jq:
What is going on here? This is the result of an important design choice that SAW makes: SAW only supports verifying monomorphic functions. To be more precise, SAW’s approach to symbolic simulation requires all of the code being simulated to have fixed types without any type parameters.
In order to verify a function using generics in your Rust code, you must provide a separate, monomorphic function that calls into the generic function. For example, you can rewrite the example above like so:
If you compile this version with saw-rustc, you’ll see:
This time, the resulting JSON file contains a definition for id_u8. The reason that this works is because when id_u8 calls id, the Rust compile will generate a specialized version of id where A is instantiated with the type u8. This specialized version of id is named id::_instaddce72e1232152c[0] in the output above. (You don’t have to remember this name, thankfully!)
Although the resulting JSON file contains a definition for id_u8, it does not contain a definition for the generic id function. As a result, SAW will only be able to verify the id_u8 function from this file. If you are ever in doubt about which functions are accessible for verification with SAW, you can check this with jq like so:
Here, “intrinsics” are monomorphic functions that are visible to SAW. Note that saw-rustc will optimize away all definitions that are not accessible from one of these intrinsic functions. This explains why the original program that only defined a generic id function resulted in a definition-less JSON file, as that program did not contain monomorphic functions (and therefore no intrinsics).
Generally speaking, we prefer to verify functions that are defined directly in the Rust source code, such as id_u8, as these functions’ names are more stable than the specialized versions of functions that the compiler generates, such as id::_instaddce72e1232152c[0]. Do note that SAW is capable of verifying both types of functions, however. (We will see an example of verifying an autogenerated function in the Salsa20 case study later in this tutorial.)
Identifiers
When you compile a function named id_u8, saw-rustc will expand it to a much longer name such as first_example/abef32c5::id_u8. This longer name is called an identifier, and it provides a globally unique name for that function. In the small examples we’ve seen up to this point, there hasn’t been any risk of name collisions, but you could imagine compiling this code alongside another file (or crate) that also defines an id_u8 function. If that happens, then it is essential that we can tell apart all of the different id_u8 functions, and identifiers provide us the mechanism for doing so.
Let’s take a closer look at what goes into an identifier. In general, an identifier will look like the following:
<crate name>/<disambiguator>::<function path>
<crate name> is the name of the crate in which the function is defined. All of the examples we’ve seen up to this point have been defined in standalone files, and as a result, the crate name has been the same as the file name, but without the .rs extension and with all hyphens replaced with underscores (e.g., first-example.rs is given the crate name first_example). In cargo-based projects, the crate name will likely differ from the file name.
<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. (More on this in a bit.)
<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:
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.,
The most cumbersome part of writing an identifier is the disambiguator, as it is extremely sensitive to changes in the code (not to mention hard to remember and type). Luckily, the vast majority of crate names correspond to exactly one disambiguator, and we can exploit this fact to abbreviate identifiers that live in such crates. For instance, we can abbreviate this identifier:
To simply:
We will adopt the latter, shorter notation throughout the rest of the tutorial. SAW also understands this shorthand, so we will also use this notation when passing identifiers to SAW commands.
SAW basics
A first SAW example
We now have the knowledge necessary to compile Rust code in a way that is suitable for SAW. Let’s put our skills to the test and verify something! We will build on the example from above, which we will put into a file named saw-basics.rs:
Our goal is to verify the correctness of the id_u8 function. However, it is meaningless to talk about whether a function is correct without having a specification for how the function should behave. This is where SAW enters the picture. SAW provides a scripting language named SAWScript that allows you to write a precise specification for describing a function’s behavior. For example, here is a specification that captures the intended behavior of id_u8:
At a high level, this specification says that id_u8 is a function that accepts a single argument of type u8, and it returns its argument unchanged. Nothing too surprising there, but this example illustrates many of the concepts that one must use when working with SAW. Let’s unpack what this is doing, line by line:
In SAWScript, specifications are ordinary values that are defined with
let. In this example, we are defining a specification namedid_u8_spec.Specifications are defined using “
do-notation”. That is, they are assembled by writingdo { <stmt>; <stmt>; ...; <stmt>; }, where each<stmt>is a statement that declares some property about the function being verified. A statement can optionally bind a variable that can be passed to later statements, which is accomplished by writing<var> <- <stmt>.The
x <- mir_fresh_var "x" mir_u8;line declares thatxis a fresh variable of typeu8(represented bymir_u8in SAWScript) that has some unspecified value. In SAW parlance, we refer to these unspecified values as symbolic values. SAW uses an SMT solver under the hood to reason about symbolic values.The
"x"string indicates what name the variablexshould have when sent to the underlying SMT solver. This is primarily meant as a debugging aid, and it is not required that the string match the name of the SAWScript variable. (For instance, you could just as well have passed"x_smt"or something else.)The
mir_execute_func [mir_term x];line declares that the function should be invoked withxas the argument. For technical reasons, we passmir_term xtomir_execute_funcrather than justx; we will go over whatmir_termdoes later in the tutorial.Finally, the
mir_return (mir_term x);line declares that the function should returnxonce it has finished.
Now that we have a specification in hand, it’s time to prove that id_u8 actually adheres to the spec. To do so, we need to load the MIR JSON version of id_u8 into SAW, which is done with the mir_load_module command:
This m variable contains the definition of id_u8, as well as the other code defined in the program. We can then pass m to the mir_verify command, which actually verifies that id_u8 behaves according to id_u8_spec:
Here is what is going on in this command:
The
mand"saw_basics::id_u8"arguments instruct SAW to verify theid_u8function located in thesaw_basicscrate defined inm. Note that we are using the shorthand identifier notation here, so we are allowed to omit the disambiguator for thesaw_basicscrate.The
[]argument indicates that we will not provide any function overrides to use when SAW simulates theid_u8function. (We will go over how overrides work later in the tutorial.)The
falseargument indicates that SAW should not use path satisfiability checking when analyzing the function. Path satisfiability checking is an advanced SAW feature that we will not be making use of in this tutorial, so we will always usefalsehere.The
id_u8_specargument indicates thatid_u8should be checked against the specification defined byid_u8_spec.The
z3argument indicates that SAW should use the Z3 SMT solver to solve any proof goals that are generated during verification. SAW also supports other SMT solvers, although we will mostly use Z3 in this tutorial.
Putting this all together, our complete saw-basics.saw file is:
One minor detail that we left out until just now is that the SAW’s interface to MIR is still experimental, so you must explicitly opt into it with the enable_experimental command.
Now that everything is in place, we can check this proof like so:
Tada! SAW was successfully able to prove that id_u8 adheres to its spec.
Cryptol
The spec in the previous section is nice and simple. It’s also not very interesting, as it’s fairly obvious at a glance that id_u8’s implementation is correct. Most of the time, we want to verify more complicated functions where the correspondence between the specification and the implementation is not always so clear.
For example, consider this function, which multiplies a number by two:
The straightforward way to implement this function would be to return 2 * x, but the author of this function really cared about performance. As such, the author applied a micro-optimization that computes the multiplication with a single left-shift (<<). This is the sort of scenario where we are pretty sure that the optimized version of the code is equivalent to the original version, but it would be nice for SAW to check this.
Let’s write a specification for the times_two function:
This spec introduces code delimited by double curly braces {{ ... }}, which is a piece of syntax that we haven’t seen before. The code in between the curly braces is written in Cryptol, a language designed for writing high-level specifications of various algorithms. Cryptol supports most arithmetic operations, so 2 * x works exactly as you would expect. Also note that the x variable was originally bound in the SAWScript language, but it is possible to embed x into the Cryptol language by referencing x within the curly braces. (We’ll say more about how this embedding works later.)
{{ 2 * x }} takes the Cryptol expression 2 * x and lifts it to a SAW expression. As such, this SAW spec declares that the function takes a single u32-typed argument x and returns 2 * x. We could have also wrote the specification to declare that the function returns x << 1, but that would have defeated the point of this exercise: we specifically want to check that the function against a spec that is as simple and readable as possible.
Our full SAW file is:
Which we can verify is correct like so:
Nice! Even though the times_two function does not literally return 2 * x, SAW is able to confirm that the function behaves as if it were implemented that way.
Terms and other types
Terms and other typesNow that we know how Cryptol can be used within SAW, we can go back and explain what the mir_term function does. It is helpful to examine the type of mir_term by using SAW’s interactive mode. To do so, run the saw binary without any other arguments:
Then run enable_experimental (to enable MIR-related commands) and run :type mir_term:
Here, we see that mir_term accepts a Term as an argument and returns a MIRValue. In this context, the Term type represents a Cryptol value, and the MIRValue type represents SAW-related MIR values. Terms can be thought of as a subset of MIRValues, and the mir_term function is used to promote a Term to a MIRValue.
Most other MIR-related commands work over MIRValues, as can be seen with SAW’s :type command:
Note that MIRSetup is the type of statements in a MIR specification, and two MIRSetup-typed commands can be chained together by using do-notation. Writing MIRSetup () means that the statement does not return anything interesting, and the use of () here is very much analogous to how () is used in Rust. There are other MIRSetup-typed commands that do return something interesting, as is the case with mir_fresh_var:
This command returns a MIRSetup Term, which means that when you write x <- mir_fresh_var ... ... in a MIR specification, then x will be bound at type Term.
Values of type Term have the property that they can be embedded into Cryptol expression that are enclosed in double curly braces {{ ... }}. This is why our earlier {{ 2 * x }} example works, as x is of type Term.
Preconditions and postconditions
As a sanity check, let’s write a naïve version of times_two that explicitly returns 2 * x:
It seems like we should be able to verify this times_two_ref function using the same spec that we used for times_two:
Somewhat surprisingly, SAW fails to verify this function:
The “which would overflow” portion of the error message suggests what went wrong. When a Rust program is compiled with debug settings (which is the default for rustc and saw-rustc), arithmetic operations such as multiplication will check if the result of the operation can fit in the requested number of bits. If not, the program will raise an error.
In this case, we must make the result of multiplication fit in a u32, which can represent values in the range 0 to 2^^32 - 1 (where ^^ is Cryptol’s exponentiation operator). But it is possible to take a number in this range, multiply it by two, and have the result fall outside of the range. In fact, SAW gives us a counterexample with exactly this number: 2147483648, which can also be written as 2^^31. Multiplying this by two yields 2^^32, which is just outside of the range of values expressible with u32. SAW’s duties include checking that a function cannot fail at runtime, so this function falls afoul of that check.
Note that we didn’t have this problem with the original definition of times_two because the semantics of << are such that if the result is too large to fit in the requested type, then the result will overflow, i.e., wrap back around to zero and count up. This means that (2^^31) << 1 evaluates to 0 rather than raising an error. Cryptol’s multiplication operation also performs integer overflow (unlike Rust in debug settings), which is why we didn’t notice any overflow-related issues when verifying times_two.
There are two possible ways that we can repair this. One way is to rewrite times_two_ref to use Rust’s wrapping_mul function, a variant of multiplication that always uses integer overflow. This work around the issue, but it is a bit more verbose.
The other way is to make our spec more precise such that we only verify times_two_ref for particular inputs. Although times_two_ref will run into overflow-related issues when the argument is 2^^31 or greater, it is perfectly fine for inputs smaller than 2^^31. We can encode such an assumption in SAW by adding a precondition. To do so, we write a slightly modified version of times_two_spec:
The most notable change is the mir_precond {{ x < 2^^31 }}; line. mir_precond (where “precond” is short for “precondition”) is a command that takes a Term argument that contains a boolean predicate, such as {{ x < 2^^31 }}. Declaring a precondition requires that this predicate must hold during verification, and any values of x that do not satisfy this predicate are not considered.
By doing this, we have limited the range of the function from 0 to 2^^31 - 1, which is exactly the range of values for which times_two_ref is well defined. SAW will confirm this if we run it:
We can add as many preconditions to a spec as we see fit. For instance, if we only want to verify times_two_ref for positive integers, we could add an additional assumption:
In addition to preconditions, SAW also supports postconditions. Whereas preconditions represent conditions that must hold before invoking a function, postconditions represent conditions that must hold after invoking a function. We have already seen one type of postcondition in the form of the mir_return command, which imposes a postcondition on what the return value must be equal to.
We can introduce additional postconditions with the mir_postcond command. For example, if we call times_two_ref with a positive argument, then it should be the case that the return value should be strictly greater than the argument value. We can check for this using mir_postcond like so:
An additional convenience that SAW offers is the mir_assert command. mir_assert has the same type as mir_precond and mir_postcond, but mir_assert can be used to declare both preconditions and postconditions. The difference is where mir_assert appears in a specification. If mir_assert is used before the call to mir_execute_func, then it declares a precondition. If mir_assert is used after the call to mir_execute_func, then it declares a postcondition.
For example, we can rewrite times_two_ref_positive_postcond_spec to use mir_asserts like so:
The choice of whether to use mir_precond/mir_postcond versus mir_assert is mostly a matter personal taste.
Reference types
All of the examples we have seen up to this point involve simple integer types such as u8 and u32. While these are useful, Rust’s type system features much more than just integers. A key part of Rust’s type system are its reference types. For example, in this read_ref function:
The function reads the value that r (of type &u32) points to and returns it. Writing SAW specifications involving references is somewhat trickier than with other types of values because we must also specify what memory the reference points to. SAW provides a special command for doing this called mir_alloc:
mir_alloc will allocate a reference value with enough space to hold a value of the given MIRType. Unlike mir_fresh_var, mir_alloc returns a MIRValue instead of a Term. We mentioned before that Terms are only a subset of MIRValues, and this is one of the reasons why. Cryptol does not have a notion of reference values, but MIRValues do. As a result, you cannot embed the result of a call to mir_alloc in a Cryptol expression.
mir_alloc must be used with some care. Here is a first, not-quite-correct attempt at writing a spec for read_ref using mir_alloc:
As the comment suggests, it’s not entirely clear what this spec should return. We can’t return r, since read_ref returns something of type u32, not &u32. On the other hand, we don’t have any values of type u32 lying around that are obviously the right thing to use here. Nevertheless, it’s not required for a SAW spec to include a mir_return statement, so let’s see what happens if we verify this as-is:
Clearly, SAW didn’t like what we gave it. The reason this happens is although we allocated memory for the reference r, we never told SAW what value should live in that memory. When SAW simulated the read_ref function, it attempted to dereference r, which pointed to uninitialized memory. This is constitutes an error in SAW, which is what this “attempted to read empty mux tree” business is about.
SAW provides a mir_points_to command to declare what value a reference should point to:
Here, the first MIRValue argument represents a reference value, and the second MIRValue argument represents the value that the reference should point to. In our spec for read_ref, we can declare that the reference should point to a symbolic u32 value like so:
We have renamed r to r_ref in this revised spec to more easily distinguish it from r_val, which is the value that r_ref is declared to point to using mir_points_to. In this version of the spec, it is clear that we should return r_val using mir_return, as r_val is exactly the value that will be computed by dereferencing r_ref.
This pattern, where a call to mir_alloc/mir_alloc_mut to followed by a call to mir_points_to, is common with function specs that involve references. Later in the tutorial, we will see other examples of mir_points_to where the reference argument does not come from mir_alloc/mir_alloc_mut.
The argument to read_ref is an immutable reference, so the implementation of the function is not allowed to modify the memory that the argument points to. Rust also features mutable references that do permit modifying the underlying memory, as seen in this swap function:
A corresponding spec for swap is:
There are two interesting things worth calling out in this spec:
Instead of allocating the reference values with
mir_alloc, we instead usemir_alloc_mut. This is a consequence of the fact that&mut u32is a different type from&mutin Rust (and in MIR), and and such, we need a separatemir_alloc_mutto get the types right.This spec features calls to
mir_points_tobefore and aftermir_execute_func. This is because the values thata_refandb_refpoint to before calling the function are different than the values that they point to after calling the function. The two uses tomir_points_toafter the function has been called swap the order ofa_valandb_val, reflecting the fact that theswapfunction itself swaps the values that the references point to.
Compound data types
Besides integer types and reference types, Rust also features a variety of other interesting data types. This part of the tutorial will briefly go over some of these data types and how to interface with them in SAW.
Array types
Rust includes array types where the length of the array is known ahead of time. For instance, this index function takes an arr argument that must contain exactly three u32 values:
While Rust is good at catching many classes of programmer errors at compile time, one thing that it cannot catch in general is out-of-bounds array accesses. In this index example, calling the function with a value of idx ranging from 0 to 2 is fine, but any other choice of idx will cause the program to crash, since the idx will be out of the bounds of arr.
SAW is suited to checking for these sorts of out-of-bound accesses. Let’s write an incorrect spec for index to illustrate this:
Before we run this with SAW, let’s highlight some of the new concepts that this spec uses:
The type of the
arrvariable is specified usingmir_array 3 mir_u32. Here, themir_arrayfunction takes the length of the array and the element type as arguments, just as in Rust.The spec declares the return value to be
{{ arr @ idx }}, where@is Cryptol’s indexing operator. Also note that it is completely valid to embed a MIR array type into a Cryptol expression, as Cryptol has a sequence type that acts much like arrays do in MIR.
As we hinted above, this spec is wrong, as it says that this should work for any possible values of idx. SAW will catch this mistake:
We can repair this spec by adding some preconditions:
An alternative way of writing this spec is by using SAW’s mir_array_value command:
Here, the MIRType argument represents the element type, and the list of MIRValue arguments are the element values of the array. We can rewrite index_spec using mir_array_value like so:
Here, [arr0, arr1, arr2] is Cryptol notation for constructing a length-3 sequence consisting of arr0, arr1, and arr2 as the elements. index_alt_spec is equivalent to index_spec, albeit more verbose. For this reason, it is usually preferable to use mir_fresh_var to create an entire symbolic array rather than creating separate symbolic values for each element and combining them with mir_array_value.
There are some situations where mir_array_value is the only viable choice, however. Consider this variant of the index function:
When writing a SAW spec for index_ref_arr, we can’t just create a symbolic variable for arr using mir_alloc (mir_array 3 ...), as the reference values in the array wouldn’t point to valid memory. Instead, we must individually allocate the elements of arr using separate calls to mir_alloc and then build up the array using mir_array_value. (As an exercise, try writing and verifying a spec for index_ref_arr).
Tuple types
Rust includes tuple types where the elements of the tuple can be of different types. For example:
SAW includes a mir_tuple function for specifying the type of a tuple value. In addition, one can embed MIR tuples into Cryptol, as Cryptol also includes tuple types whose fields can be indexed with .0, .1, etc. Here is a spec for flip that makes use of all these features:
SAW also includes a mir_tuple_value function for constructing a tuple value from other MIRValues:
mir_tuple_value plays a similar role for tuples as mir_array_value does for arrays.
Struct types
Rust supports the ability for users to define custom struct types. Structs are uniquely identified by their names, so if you have two structs like these:
Then even though the fields of the S and T structs are the same, they are not the same struct. This is a type system feature that Cryptol does not have, and for this reason, it is not possible to embed MIR struct values into Cryptol. It is also not possible to use mir_fresh_var to create a symbolic struct value. Instead, one can use the mir_struct_value command:
Like with mir_array_value and mir_tuple_value, the mir_struct_value function takes a list of MIRValues as arguments. What makes mir_struct_value unique is its MIRAdt argument, which we have not seen up to this point. In this context, “Adt” is shorthand for “algebraic data type”, and Rust’s structs are an example of ADTs. (Rust also supports enums, another type of ADT that we will see later in this tutorial.)
ADTs in Rust are named entities, and as such, they have unique identifiers in the MIR JSON file in which they are defined. Looking up these identifiers can be somewhat error-prone, so SAW offers a mir_find_adt command that computes an ADT’s identifier and returns the MIRAdt associated with it:
Here, MIRModule correspond to the MIR JSON file containing the ADT definition, and the String is the name of the ADT whose identifier we want to look up. The list of MIRTypes represent types to instantiate any type parameters to the struct (more on this in a bit).
As an example, we can look up the S and T structs from above like so:
We pass an empty list of MIRTypes to each use of mir_find_adt, as neither S nor T have any type parameters. An example of a struct that does include type parameters can be seen here:
As mentioned before, SAW doesn’t support generic definitions out of the box, so the only way that we can make use of the Foo struct is by looking up a particular instantiation of Foo’s type parameters. If we define a function like this, for example:
Then this function instantiates Foo’s A type parameter with u32 and the B type parameter with u64. We can use mir_find_adt to look up this particular instantiation of Foo like so:
In general, a MIR JSON file can have many separate instantiations of a single struct’s type parameters, and each instantiation must be looked up separately using mir_find_adt.
Having looked up Foo<u32, u64> using mir_find_adt, let’s use the resulting MIRAdt in a spec:
Note that we are directly writing out the values 27 and 42 in Cryptol. Cryptol’s numeric literals can take on many different types, so in order to disambiguate which type they should be, we give each numeric literal an explicit type annotation. For instance, the expression 27 : [32] means that 27 should be a 32-bit integer.
Symbolic structs
Let’s now verify a function that takes a struct value as an argument:
Moreover, let’s verify this function for all possible Bar values. One way to do this is to write a SAW spec that constructs a struct value whose fields are themselves symbolic:
This is a rather tedious process, however, as we had to repeatedly use mir_fresh_var to create a fresh, symbolic value for each field. Moreover, because mit_fresh_var does not work for structs, we had to recursively apply this process in order to create a fresh Foo value. It works, but it takes a lot of typing to accomplish.
To make this process less tedious, SAW offers a mir_fresh_expanded_value command that allows one to create symbolic values of many more types. While mir_fresh_var is limited to those MIR types that can be directly converted to Cryptol, mir_fresh_expanded_value can create symbolic structs by automating the process of creating fresh values for each field. This process also applies recursively for struct fields, such as the Foo field in Bar.
As an example, a much shorter way to write the spec above using mir_fresh_expanded_value is:
That’s it! Note that the string "b" is used as a prefix for all fresh names that mir_fresh_expanded_value generates, so if SAW produces a counterexample involving this symbolic struct value, one can expect to see names such as b_0, b_1, etc. for the fields of the struct.
mir_fresh_expanded_value makes it easier to construct large, compound values that consist of many smaller, inner values. The drawback is that you can’t refer to these inner values in the postconditions of a spec. As a result, there are some functions for which mir_fresh_expanded_value isn’t suitable, so keep this in mind before reaching for it.
Enum types
Besides structs, another form of ADT that Rust supports are enums. Each enum has a number of different variants that describe the different ways that an enum value can look like. A famous example of a Rust enum is the Option type, which is defined by the standard library like so:
Option is commonly used in Rust code to represent a value that may be present (Some) or absent (None). For this reason, we will use Option as our motivating example of an enum in this section.
First, let’s start by defining some functions that make use of Option’s variants:
Both functions return an Option<u32> value, but each function returns a different variant. In order to tell these variants apart, we need a SAW function which can construct an enum value that allows the user to pick which variant they want to construct. The `mir_enum_value function does exactly that:
Like mir_struct_value, mir_enum_value also requires a MIRAdt argument in order to discern which particular enum you want. Unlike mir_struct_value, however, it also requires a String which variant of the enum you want. In the case of Option, this String will either be "None" or "Some". Finally, the [MIRValue] arguments represent the fields of the enum variant.
Let’s now verify some enum-related code with SAW. First, we must look up the Option<u32> ADT, which works just as if you had a struct type:
Next, we can use this ADT to construct enum values. We shall use mir_enum_value to create a Some value in the spec for i_found_something:
Note that while we used the full identifier core::option::Option to look up the Option ADT, we do not need to use the core::option prefix when specifying the "Some" variant. This is because SAW already knows what the prefix should be from the option_u32 ADT, so the "Some" shorthand suffices.
Similarly, we can also write a spec for i_got_nothing, which uses the None variant:
Symbolic enums
In order to create a symbolic struct, one could create symbolic fields and pack them into a larger struct value using mir_struct_value. The same process is not possible with mir_enum_value, however, as a symbolic enum value would need to range over all possible variants in an enum.
Just as mir_fresh_expanded_value supports creating symbolic structs, mir_fresh_expanded_value also supports creating symbolic enum values. For example, given this function that accepts an Option<u32> value as an argument:
We can write a spec for this function that considers all possible Option<u32> values like so:
Here, o can be a None value, or it can be a Some value with a symbolic field.
Slices
Slices are a particular type of reference that allow referencing contiguous sequences of elements in a collection, such as an array. Unlike ordinary references (e.g., &u32), SAW does not permit allocating a slice directly. Instead, one must take a slice of an existing reference. To better illustrate this distinction, consider this function:
sum_of_prefix takes a slice to a sequence of u32s as an argument, indexes into the first two elements in the sequence, and adds them together. There are many possible ways we can write a spec for this function, as the slice argument may be backed by many different sequences. For example, the slice might be backed by an array whose length is exactly two:
We could also make a slice whose length is longer than two:
Alternatively, the slice might be a subset of an array whose length is longer than two:
All of these are valid ways of building the slice argument to sum_of_prefix. Let’s try to write SAW specifications that construct these different forms of slices. To do so, we will need SAW functions that take a reference to a collection (e.g., an array) and converts them into a slice reference. The mir_slice_value function is one such function:
mir_slice_value arr_ref is the SAW equivalent of writing arr_ref[..]. That is, if arr_ref is of type &[T; N], then mir_slice_value arr_ref is of type &[T]. Note that arr_ref must be a reference to an array, not an array itself.
Let’s use mir_slice_value to write a spec for sum_of_prefix when the slice argument is backed by an array of length two:
The first part of this spec allocates an array reference a_ref and declares that it points to a fresh array value a_val. The next part declares a slice s that is backed by the entirety of a_ref, which is then passed as an argument to the function itself. Finally, the return value is declared to be the sum of the first and second elements of a_val, which are the same values that back the slice s itself.
As noted above, the sum_of_prefix function can work with slices of many different lengths. Here is a slight modification to this spec that declares it to take a slice of length 5 rather than a slice of length 2:
Both of these examples declare a slice whose length matches the length of the underlying array. In general, there is no reason that these have to be the same, and it is perfectly fine for a slice’s length to be less than the the length of the underlying array. In Rust, for example, we can write a slice of a subset of an array by writing &arr_ref[0..2]. The SAW equivalent of this can be achieved with the mir_slice_range_value function:
mir_slice_range_value takes takes two additional Int arguments that represent (1) the index to start the slice from, and (2) the index at which the slice ends. For example, mir_slice_range_value arr_ref 0 2 creates a slice that is backed by the first element (index 0) and the second element (index 1) of arr_ref. Note that the range [0..2] is half-open, so this range does not include the third element (index 2).
For example, here is how to write a spec for sum_of_prefix where the slice is a length-2 subset of the original array:
Note that both Int arguments to mir_slice_range_value must be concrete (i.e., not symbolic). (See the section below if you want an explanation for why they are not allowed to be symbolic.)
Aside: slices of arbitrary length
After reading the section about slices above, one might reasonably wonder: is there a way to write a more general spec for sum_of_prefix: that covers all possible slice lengths n, where n is greater than or equal to 2? In this case, the answer is “no”.
This is a fundamental limitation of the way SAW’s symbolic execution works. The full reason for why this is the case is somewhat technical (keep reading if you want to learn more), but the short answer is that if SAW attempts to simulate code whose length is bounded by a symbolic integer, then SAW will go into an infinite loop. To avoid this pitfall, the mir_slice_range_value function very deliberately requires the start and end values to be concrete integers, as allowing these values to be symbolic would allow users to inadvertently introduce infinite loops in their specifications.
A longer answer as to why SAW loops forever on computations that are bounded by symbolic lengths: due to the way SAW’s symblolic execution works, it creates a complete model of the behavior of a function for all possible inputs. The way that SAW achieves this is by exploring all possible execution paths through a program. If a program involves a loop, for example, then SAW will unroll all iterations of the loop to construct a model of the loop’s behavior. Similarly, if a sequence (e.g., a slice or array) has an unspecified length, then SAW must consider all possible lengths of the array.
SAW’s ability to completely characterize the behavior of all paths through a function is one of its strengths, as this allows it to prove theorems that other program verification techniques would not. This strength is also a weakness, however. If a loop has a symbolic number of iterations, for example, then SAW will spin forever trying to unroll the loop. Similarly, if a slice were to have a symbolic length, then SAW would spin forever trying to simulate the program for all possible slice lengths.
In general, SAW cannot prevent users from writing programs whose length is bounded by a symbolic value. For now, however, SAW removes one potential footgun by requiring that slice values always have a concrete length.
Overrides and compositional verification
Up until this point, all uses of mir_verify in this tutorial have provided an empty list ([]) of overrides. This means that any time SAW has simulated a function which calls another function, it will step into the definition of the callee function and verify its behavior alongside the behavior of the callee function. This is a fine thing to do, but it can be inefficient. For example, consider a function like this:
Here, the caller function f invokes the callee function g three separate times. If we verify f with mir_verify as we have done up until this point, then SAW must analyze the behavior of g three separate times. This is wasteful, and especially so if g is a large and complicated function.
This is where compositional verification enters the picture. The idea behind compositional verification is that when we prove properties of a caller function, we can reuse properties that we have already proved about callee functions. These properties are captured as override specifications, which are also referred to by the shorthand term overrides. When a caller invokes a callee with a corresponding override specification, the override’s properties are applied without needing to re-simulate the entire function.
As it turns out, the command needed to produce an override specification is already familiar to us—it’s mir_verify! If you examine the type of this command:
The returned value is a MIRSpec, which captures the behavior of the function that was verified as an override spec. This override can then be passed to another call to mir_verify to use as part of a larger proof.
Let’s now try compositional verification in practice. To do so, we will first prove a spec for the g function above. For demonstration purposes, we will pick a simplistic implementation of g:
Note that we don’t really have to use compositional verification when g is this simple, as SAW is capable of reasoning about g’s behavior directly when proving a spec for f. It’s still worth going along with this exercise, however, as the same principles of compositional verification apply whether the implementation of g is small or large.
The first step of compositional verification is to prove a spec for g, the callee function:
There’s nothing that different about this particular proof from the proofs we’ve seen before. The only notable difference is that we bind the result of calling mir_verify to a MIRSpec value that we name g_ov (short for “g override”). This part is important, as we will need to use g_ov shortly.
The next step is to write a spec for f. Since g adds 1 to its argument, f will add 3 to its argument:
Again, nothing too surprising. Now let’s prove f against f_spec by using g_ov as a compositional override:
Here, note that instead of passing an empty list ([]) as we have done before, we now pass a list containing g_ov. This informs mir_verify that whenever it simulates a call to g, it should reuse the properties captured in g_ov. In general, we can pass as many overrides as we want (we will see examples of this later in the tutorial), but for now, one override will suffice.
Let’s run the proof of f against f_spec, making sure to pay attention to the output of SAW:
We’ve now proven f compositionally! The first two lines (“Verifying ...” and “Simulating ...”) and the last two lines (“Checking proof obligations ...” and “Proof succeeded! ...") are the same as before, but this time, we have some additional lines of output in between:
Whenever SAW prints “
Matching <N> overrides of <function>”, that’s when you know that SAW is about to simulate a call to<function>. At that point, SAW will check to see how many overrides (<N>) for<function>are available.Whenever SAW prints “
Brancing on <N> override variants of <function>", SAW is trying to figure out which of the` overrides to apply. In this example, there is only a single override, so the choice is easy. In cases where there are multiple overrides, however, SAW may have to work harder (possibly even consulting an SMT solver) to figure out which override to use.If SAW successfully picks an override to apply, it will print “
Applied override! ...”.
In the example above, we used a single g override that applies for all possible arguments. In general, however, there is no requirement that overrides must work for all arguments. In fact, it is quite common for SAW verification efforts to write different specifications for the same function, but with different arguments. We can then provide multiple overrides for the same function as part of a compositional verification, and SAW will be able to pick the right override depending on the shape of the argument when invoking the function being overridden.
For example, let’s suppose that we wrote different g specs, one where the argument to g is even, and another where the argument to g is odd:
We can then prove f compositionally by passing both of the g overrides to mir_verify:
Like before, this will successfully verify. The only different now is that SAW will print output involving two overrides instead of just one:
Keep in mind that if you provide at least one override for a function as part of a compositional verification, then SAW must apply an override whenever it invokes that function during simulation. If SAW cannot find a matching override, then the verification will fail. For instance, consider what would happen if you tried proving f like so:
This time, we supply one override for g that only matches when the argument is even. This is a problem, as SAW will not be able to find a matching override when the argument is odd. Indeed, SAW will fail to verify this:
Here, we can see that No override specification applies, and SAW also generates a counterexample of x: 1. Sure enough, 1 is an odd number!
Overrides and mutable references
Compositional overrides provide great power, as they effectively allow you to skip over certain functions when simulating them and replace them with simpler implementations. With great power comes great responsibility, however. In particular, one must be careful when using overrides for functions that modify mutable references. If an override does not properly capture the behavior of a mutable reference, it could potentially lead to incorrect proofs.
This is the sort of thing that is best explained with an example, so consider these two functions:
The side_effect function does not return anything interesting; it is only ever invoked to perform a side effect of changing the mutable reference a to point to 0. The foo function invokes side_effect, and as a result, it will always return 0, regardless of what the argument to foo is. No surprises just yet.
Now let’s make a first attempt at verifying foo using compositional verification. First, we will write a spec for side_effect:
side_effect_spec is somewhat odd. Although it goes through the effort of allocating a mutable reference a_ref and initializing it, nothing about this spec states that a_ref will point to 0 after the function has been invoked. This omission is strange, but not outright wrong—the spec just underspecifies what the behavior of the function is. Indeed, SAW will successfully verify this spec using mir_verify:
Next, let’s try to write a spec for foo:
At this point, alarm bells should be going off in your head. This spec incorrectly states that foo(x) should return x, but it should actually return 0! This looks wrong, but consider what would happen if you tried to verify this compositionally using our side_effect_ov override:
If SAW were to simulate foo(x), it would invoke create a temporary variable b and assign it to the value x, and then it would invoke side_effect(&mut b). At this point, the side_effect_ov override would apply. According to side_effect_spec, the argument to side_effect is not modified at all after the function returns. This means that when the foo function returns b, it will still retain its initial value of x. This shows that if we were to use side_effect_ov, we could prove something that’s blatantly false!
Now that we’ve made you sweat a little bit, it’s time for some good news: SAW won’t actually let you prove foo_spec. If you try this compositional proof in practice, SAW will catch your mistake:
The line of code that SAW points to in the “State of memory ...” error message is:
SAW informs us that although we allocated the mutable reference a_ref, we never indicated what it should point to after the function has returned. This is an acceptable (if somewhat unusual) thing to do when verifying side_effect_spec using mir_verify, but it is not acceptable to do this when using this spec as an override. To avoid unsound behavior like what is described above, any override that allocates a mutable reference in its preconditions must declare what its value should be in the postconditions, no exceptions.
Thankfully, repairing this spec is relatively straightforward. Simply add a mir_points_to statement in the postconditions of side_effect_spec:
Then use the correct return value in foo_spec:
And now the compositional proof of foo_spec works!
Unsafe overrides
Now that we’ve made it this far into the tutorial, it’s time to teach you a more advanced technique: unsafe overrides. Up until this point, we have relied on SAW to check all of our work, and this is usually what you’d want from a formal verification tool. In certain circumstances, however, it can be useful to say “I know what I’m doing, SAW—just believe me when I say this spec is valid!” In order to say this, you can use mir_unsafe_assume_spec:
mir_unsafe_assume_spec is mir_verify’s cousin who likes to live a little more dangerously. Unlike mir_verify, the specification that you pass to mir_unsafe_assume_spec (the MIRSetup () argument) is not checked for full correctness. That is, mir_unsafe_assume_spec will bypass SAW’s usual symbolic execution pipeline, which is why one does not need to pass a ProofScript argument (e.g., z3) to mir_unsafe_assume_spec. SAW will believe whatever spec you supply mir_unsafe_assume_spec to be valid, and the MIRSpec that mir_unsafe_assume_spec returns can then be used in later compositional verifications.
Why would you want to do this? The main reason is that writing proofs can be difficult, and sometimes, there are certain functions in a SAW verification effort that are disproportionately harder to write a spec for than others. It is tempting to write specs for each function in sequence, but this can run the risk of getting stuck on a particularly hard-to-verify function, blocking progress on other parts of the proofs.
In these situations, mir_unsafe_assume_spec can be a useful prototyping tool. One can use mir_unsafe_assume_spec to assume a spec for the hard-to-verify function and then proceed with the remaining parts of the proof. Of course, you should make an effort to go back and prove the hard-to-verify function’s spec later, but it can be nice to try something else first.
For example, here is how one can unsafely assume g_spec and use it in a compositional proof of f_spec:
It should be emphasized that when we say “unsafe”, we really mean it. mir_unsafe_assume_spec can be used to prove specs that are blatantly wrong, so use it with caution.
Static items
Sometimes, Rust code makes use of static items, which are definitions that are defined in a precise memory location for the entire duration of the program. As such, static items can be thought of as a form of global variables.
Immutable static items
There are two kinds of static items in Rust: mutable static items (which have a mut keyword) and immutable static items (which lack mut). Immutable static items are much easier to deal with, so let’s start by looking at an example of a program that uses immutable static data:
This function will return ANSWER, i.e., 42. We can write a spec that says as much:
This works, but it is somewhat unsatisfying, as it requires hard-coding the value of ANSWER into the spec. Ideally, we’d not have to think about the precise implementation of static items like ANSWER. Fortunately, SAW makes this possible by providing a mir_static_initializer function which computes the initial value of a static item at the start of the program:
In this case, mir_static_initializer "statics::ANSWER" is equivalent to writing mir_term {{ 42 : [32] }}, so this spec is also valid:
Like mir_verify, the mir_static_initializer function expects a full identifier as an argument, so we must write "statics::ANSWER" instead of just `“ANSWER”.
At the MIR level, there is a unique reference to every static item. You can obtain this reference by using the mir_static function:
Here is one situation in which you would need to use a reference to a static item (which mir_static computes) rather than the value of a static item (which mir_static_initializer computes):
A spec for this function would look like this:
That’s about all there is to say regarding immutable static items.
Mutable static items
Mutable static items are a particularly tricky aspect of Rust. Including a mutable static item in your program is tantamount to having mutable global state that any function can access and modify. They are so tricky, in fact, that Rust does not even allow you to use them unless you surround them in an unsafe block:
The mir_static_initializer and mut_static functions work both immutable and mutable static items, so we can write specs for mutable items using mostly the same techniques as for writing specs for immutable items. We must be careful, however, as SAW is pickier when it comes to specifying the initial values of mutable static items. For example, here is naĂŻve attempt at porting the spec for answer_to_the_ultimate_question over to its mutable static counterpart, mut_answer_to_the_ultimate_question:
This looks plausible, but SAW will fail to verify it:
Oh no! Recall that we have seen this “attempted to read empty mux tree” error message once before when discussing reference types. This error arose when we attempted to read from uninitialized memory from a reference value. The same situation applies here. A static item is backed by a reference, and SAW deliberately does not initialize the memory that a mutable static reference points to upon program startup. Since we did not initialize MUT_ANSWER’s reference value in the preconditions of the spec, SAW crashes at simulation time when it attempts to read from the uninitialized memory.
The solution to this problem is to perform this initialization explicitly using mir_points_to in the preconditions of the spec. For example, this is a valid spec:
We don’t necessarily have to use mir_static_initializer as the starting value for MUT_ANSWER, however. This spec, which uses 27 as the starting value, is equally valid:
At this point, you are likely wondering: why do we need to explicitly initialize mutable static references but not immutable static references? After all, when we wrote a spec for answer_to_the_ultimate_question earlier, we managed to get away with not initializing the reference for ANSWER (which is an immutable static item). The difference is that the value of a mutable static item can change over the course of a program, and SAW requires that you be very careful in specifying what a mutable static value is at the start of a function. For example, consider a slightly extended version of the earlier Rust code we saw:
Suppose someone were to ask you “what value does mut_answer_to_the_ultimate_question return?” This is not a straightforward question to answer, as the value that it returns depends on the surrounding context. If you were to call mut_answer_to_the_ultimate_question right as the program started, it would return 42. If you were to call mut_answer_to_the_ultimate_question as part of the implementation of alternate_universe, however, then it would return 27! This is an inherent danger of using mutable static items, as they can be modified at any time by any function. For this reason, SAW requires you to be explicit about what the initial values of mutable static items should be.
Mutable static items and compositional overrides
In the “Overrides and mutable references” section, we discussed the potential pitfalls of using mutable references in compositional overrides. Mutable static items are also mutable values that are backed by references, and as such, they are also subject to the same pitfalls. Let’s see an example of this:
The setup is almost the same, except that instead of passing a mutable reference as an argument to side_effect, we instead declare a mutable static item A that is shared between side_effect and foo. We could potentially write SAW specs for side_effect and foo like these:
Note that we have once again underspecified the behavior of side_effect, as we do not say what A’s value should be in the postconditions of side_effect_spec. Similarly, foo_spec is wrong, as it should return 0 rather than the initial value of A. By similar reasoning as before, we run the risk that using side_effect_ov could lead use to prove something incorrect. Thankfully, SAW can also catch this sort of mistake:
To repair this proof, add a mir_points_to statement in the postconditions of side_effect_spec:
And then correct the behavior of foo_spec:
Be warned that if your program declares any mutable static items, then any compositional override must state what the value of each mutable static item is in its postconditions. This applies even if the override does not directly use the mutable static items. For example, if we had declared a second mutable static item alongside A:
Then side_effect_spec would need an additional mir_points_to statement involving B to satisfy this requirement. This requirement is somewhat heavy-handed, but it is necessary in general to avoid unsoundness. Think carefully before you use mutable static items!
Case study: Salsa20
If you’ve made it this far into the tutorial, congrats! You’ve now been exposed to all of the SAW fundamentals that you need to verify Rust code found in the wild. Of course, talking about verifying real-world code is one thing, but actually doing the verification is another thing entirely. Making the jump from the small examples to “industrial-strength” code can be intimidating.
To make this jump somewhat less frightening, the last part of this tutorial will consist of a case study in using SAW to verify a non-trivial piece of Rust code. In particular, we will be looking at a Rust implementation of the Salsa20 stream cipher. We do not assume any prior expertise in cryptography or stream ciphers in this tutorial, so don’t worry if you are not familiar with Salsa20.
More than anything, this case study is meant to emphasize that verification is an iterative process. It’s not uncommon to try something with SAW and encounter an error message. That’s OK! We will explain what can go wrong when verifying Salsa20 and how to recover from these mistakes. Later, if you encounter similar issues when verifying your own code with SAW, the experience you have developed when developing these proofs can inform you of possible ways to fix the issues.
The salsa20 crate
salsa20 crateThe code for this Salsa20 implementation we will be verifying can be found under the code/salsa20 subdirectory. This code is adapted from version 0.3.0 of the salsa20 crate, which is a part of the stream-ciphers project. The code implements Salsa20 as well as variants such as HSalsa20 and XSalsa20, but we will only be focusing on the original Salsa20 cipher in this tutorial.
The parts of the crate that are relevant for our needs are mostly contained in the src/core.rs file, as well as some auxiliary definitions in the src/rounds.rs and src/lib.rs files. You can take a look at these files if you’d like, but you don’t need to understand everything in them just yet. We will introduce the relevant parts of the code in the tutorial as they come up.
Salsa20 preliminaries
Salsa20 is a stream cipher, which is a cryptographic technique for encrypting and decrypting messages. A stream cipher encrypts a message by combining it with a keystream to produce a ciphertext (the encrypted message). Moreover, the same keystream can then be combined with the ciphertext to decrypt it back into the original message.
The original author of Salsa20 has published a specification for Salsa20 here. This is a great starting point for a formal verification project, as this gives us a high-level description of Salsa20’s behavior that will guide us in proving the functional correctness of the salsa20 crate. When we say that salsa20 is functionally correct, we really mean “proven correct with respect to the Salsa20 specification”.
The first step in our project would be to port the Salsa20 spec to Cryptol code, as we will need to use this code when writing SAW proofs. The process of transcribing an English-language specification to executable Cryptol code is interesting in its own right, but it is not the primary focus of this tutorial. As such, we will save you some time by providing a pre-baked Cryptol implementation of the Salsa20 spec here. (This implementation is adapted from the cryptol-specs repo.)
Writing the Cryptol version of the spec is only half the battle, however. We still have to prove that the Rust implementation in the salsa20 crate adheres to the behavior prescribed by the spec, which is where SAW enters the picture. As we will see shortly, the code in salsa20 is not a direct port of the pseudocode shown in the Salsa20 spec, as it is somewhat more low-level. SAW’s role is to provide us assurance that the behavior of the low-level Rust code and the high-level Cryptol code coincide.
A note about cryptographic security
As noted in the previous section, our goal is to prove that the behavior of salsa20 functions is functionally correct. This property should not be confused with cryptographic security. While functional correctness is an important aspect of cryptographic security, a full cryptographic security audit would encompass additional properties such as whether the code runs in constant time on modern CPUs. As such, the SAW proofs we will write would not constitute a full security audit (and indeed, the salsa20 README states that the crate has never received such an audit).
An overview of the salsa20 code
salsa20 codeBefore diving into proofs, it will be helpful to have a basic understanding of the functions and data types used in the salsa20 crate. Most of the interesting code lives in src/core.rs. At the top of this file, we have the Core struct:
Let’s walk through this:
The
statefield is an array that isSTATE_WORDSelements long, whereSTATE_WORDSis a commonly used alias for16:The
roundsfield is of typePhantomData<R>. If you haven’t seen it before,PhantomData<R>is a special type that tells the Rust compiler to pretend as though the struct is storing something of typeR, even though aPhantomDatavalue will not take up any space at runtime.
The reason that Core needs a PhantomData<R> field is because R implements the Rounds trait:
A core operation in Salsa20 is hashing its input through a series of rounds. The COUNT constant indicates how many rounds should be performed. The Salsa20 spec assumes 20 rounds:
However, there are also reduced-round variants that perform 8 and 12 rounds, respectively: