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

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

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

pub struct Core<R: Rounds> {
    /// Internal state of the core function
    state: [u32; STATE_WORDS],

    /// Number of rounds to perform
    rounds: PhantomData<R>,
}

Let’s walk through this:

The state field is an array that is STATE_WORDS elements long, where STATE_WORDS is a commonly used alias for 16:
```
/// Number of 32-bit words in the Salsa20 state
const STATE_WORDS: usize = 16;
```
The rounds field is of type PhantomData<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 type R, even though a PhantomData value will not take up any space at runtime.

The reason that Core needs a PhantomData<R> field is because R implements the Rounds trait:

//! Numbers of rounds allowed to be used with a Salsa20 family stream cipher

pub trait Rounds: Copy {
    const COUNT: usize;
}

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:

/// 20-rounds (Salsa20/20)
#[derive(Copy, Clone)]
pub struct R20;

impl Rounds for R20 {
    const COUNT: usize = 20;
}

However, there are also reduced-round variants that perform 8 and 12 rounds, respectively:

/// 8-rounds (Salsa20/8)
#[derive(Copy, Clone)]
pub struct R8;

impl Rounds for R8 {
    const COUNT: usize = 8;
}

/// 12-rounds (Salsa20/12)
#[derive(Copy, Clone)]
pub struct R12;

impl Rounds for R12 {
    const COUNT: usize = 12;
}

Each number of rounds has a corresponding struct whose names begins with the letter R. For instance, a Core<R20> value represents a 20-round Salsa20 cipher. Here is the typical use case for a Core value:

A Core value is created using the new function:
```
    pub fn new(key: &Key, iv: &Nonce) -> Self {
```
We’ll omit the implementation for now. This function takes a secret Key value and a unique Nonce value and uses them to produce the initial state in the Core value.
After creating a Core value, the counter_setup and rounds functions are used to produce the Salsa20 keystream:
```
    pub(crate) fn counter_setup(&mut self, counter: u64) {
```
```
    fn rounds(&mut self, state: &mut [u32; STATE_WORDS]) {
```
We’ll have more to say about these functions later.
The pièce de résistance is the apply_keystream function. This takes a newly created Core value, produces its keystream, and applies it to a message to produce the output:
```
    pub fn apply_keystream(&mut self, counter: u64, output: &mut [u8]) {
```

Our ultimate goal is to verify the apply_keystream function, which is the Rust equivalent of the Salsa20 encryption function described in the spec.

Building `salsa20`

The next step is to build the salsa20 crate. Unlike the examples we have seen up to this point, which have been self-contained Rust files, salsa20 is a cargo-based project. As such, we will need to build it using cargo saw-build, an extension to the cargo package manager that integrates with mir-json. Before you proceed, make sure that you have defined the SAW_RUST_LIBRARY_PATH environment variable as described in this section.

To build the salsa20 crate, perform the following steps:

$ cd code/salsa20/
$ cargo saw-build

Near the end of the build output, you will see a line that looks like this:

linking 9 mir files into <...>/saw-script/doc/rust-tutorial/code/salsa20/target/x86_64-unknown-linux-gnu/debug/deps/salsa20-dd0d90f28492b9cb.linked-mir.json

This is the location of the MIR JSON file that we will need to provide to SAW. (When we tried it, the hash in the file name was dd0d90f28492b9cb, but it could very well be different on your machine.) Due to how cargo works, the location of this file is in a rather verbose, hard-to-remember location. For this reason, we recommend copying this file to a different path, e.g.,

$ cp <...>/saw-script/doc/rust-tutorial/code/salsa20/target/x86_64-unknown-linux-gnu/debug/deps/salsa20-dd0d90f28492b9cb.linked-mir.json code/salsa20/salsa20.linked-mir.json

As a safeguard, we have also checked in a compressed version of this MIR JSON file as code/salsa20/salsa/salsa20.linked-mir.json.gz. In a pinch, you can extract this archive to obtain a copy of the MIR JSON file, which is approximately 4.6 megabytes when uncompressed.

Getting started with SAW

Now that we’ve built the salsa20 crate, it’s time to start writing some proofs! Let’s start a new code/salsa20/salsa20.saw file as fill it in with the usual preamble:

enable_experimental;

m <- mir_load_module "salsa20.linked-mir.json";

We are also going to need to make use of the Cryptol implementation of the Salsa20 spec, which is defined in code/salsa20/Salsa20.cry. SAW allows you to import standalone Cryptol .cry files by using the import command:

import "Salsa20.cry";

As an aside, note that we have also checked in a code/salsa20/salsa20-reference.saw, which contains a complete SAW file. We encourage you not to look at this file for now, since following along with the tutorial is meant to illustrate the “a-ha moments” that one would have in the process of writing the proofs. In you become stuck while following along and absolutely need a hint, however, then this file can help you become unstuck.

Verifying our first `salsa20` function

Now it’s time to start verifying some salsa20 code. But where do we start? It’s tempting to start with apply_keystream, which is our end goal. This is likely going to be counter-productive, however, as apply_keystream is a large function with several moving parts. Throwing SAW at it immediately is likely to cause it to spin forever without making any discernible progress.

For this reason, we will instead take the approach of working from the bottom-up. That is, we will first verify the functions that apply_keystream transitively invokes, and then leverage compositional verification to verify a proof of apply_keystream using overrides. This approach naturally breaks up the problem into smaller pieces that are easier to understand in isolation.

If we look at the implementation of apply_keystream, we see that it invokes the round function, which in turn invokes the quarter_round function:

pub(crate) fn quarter_round(
    a: usize,
    b: usize,
    c: usize,
    d: usize,
    state: &mut [u32; STATE_WORDS],
) {
    let mut t: u32;

    t = state[a].wrapping_add(state[d]);
    state[b] ^= t.rotate_left(7) as u32;

    t = state[b].wrapping_add(state[a]);
    state[c] ^= t.rotate_left(9) as u32;

    t = state[c].wrapping_add(state[b]);
    state[d] ^= t.rotate_left(13) as u32;

    t = state[d].wrapping_add(state[c]);
    state[a] ^= t.rotate_left(18) as u32;
}

quarter_round is built on top of the standard library functions wrapping_add and rotate_left, so we have finally reached the bottom of the call stack. This makes quarter_round a good choice for the first function to verify.

The implementation of the Rust quarter_round function is quite similar to the Cryptol quarterround function in Salsa20.cry:

quarterround : [4][32] -> [4][32]
quarterround [y0, y1, y2, y3] = [z0, z1, z2, z3]
  where
    z1 = y1 ^ ((y0 + y3) <<< 0x7)
    z2 = y2 ^ ((z1 + y0) <<< 0x9)
    z3 = y3 ^ ((z2 + z1) <<< 0xd)
    z0 = y0 ^ ((z3 + z2) <<< 0x12)

The Cryptol quarterround function doesn’t have anything like the state argument in the Rust quarter_round function, but let’s not fret about that too much yet. Our SAW spec is going to involve quarterround somehow—we just have to figure out how to make it fit.

Let’s start filling out the SAW spec for quarter_round:

let quarter_round_spec = do {

We are going to need some fresh variables for the a, b, c, and d arguments:

  a <- mir_fresh_var "a" mir_usize;
  b <- mir_fresh_var "b" mir_usize;
  c <- mir_fresh_var "c" mir_usize;
  d <- mir_fresh_var "d" mir_usize;

We will also need to allocate a reference for the state argument. The reference’s underlying type is STATE_WORDS (16) elements long:

  state_ref <- mir_alloc_mut (mir_array STATE_WORDS mir_u32);
  state_arr <- mir_fresh_var "state" (mir_array STATE_WORDS mir_u32);
  mir_points_to state_ref (mir_term state_arr);

Finally, we will need to pass these arguments to the function:

  mir_execute_func [ mir_term a
                   , mir_term b
                   , mir_term c
                   , mir_term d
                   , state_ref
                   ];
};

With that, we have a spec for quarter_round! It’s not very interesting just yet, as we don’t specify what state_ref should point to after the function has returned. But that’s fine for now. When developing a SAW proof, it can be helpful to first write out the “skeleton” of a function spec that only contains the call to mir_execute_func, without any additional preconditions or postconditions. We can add those later after ensuring that the skeleton works as expected.

Let’s check our progress thus far by running this through SAW:

$ saw salsa20.saw
...
[23:16:05.080] Type errors:
  salsa20.saw:12:39-12:68: Unbound variable: "STATE_WORDS" (salsa20.saw:12:49-12:60)
Note that some built-in commands are available only after running
either `enable_deprecated` or `enable_experimental`.

  salsa20/salsa20.saw:11:31-11:60: Unbound variable: "STATE_WORDS" (salsa20.saw:11:41-11:52)
Note that some built-in commands are available only after running
either `enable_deprecated` or `enable_experimental`.

We’ve already run into some type errors. Not too surprising, considering this was our first attempt. The error message contains that STATE_WORDS is unbound. This makes sense if you think about it, as STATE_WORDS is defined in the Rust code, but not in the SAW file itself. Let’s fix that by adding this line to salsa20.saw:

let STATE_WORDS = 16;

That change fixes the type errors in quarter_round_spec. Hooray! Let’s press on.

Next, we need to add a call to mir_verify. In order to do this, we need to know what the full identifier for the quarter_round function is. Because it is defined in the salsa20 crate and in the core.rs file, so we would expect the identifier to be named salsa20::core::quarter_round:

quarter_round_ov <-
  mir_verify m "salsa20::core::quarter_round" [] false quarter_round_spec z3;

However, SAW disagrees:

[00:22:56.970] Stack trace:
"mir_verify" (salsa20.saw:26:3-26:13)
Couldn't find MIR function named: salsa20::core::quarter_round

Ugh. This is a consequence of how mir-json disambiguates identifiers. Because there is a separate core crate in the Rust standard libraries, mir-json uses “core#1”, a distinct name, to refer to the core.rs file. You can see this for yourself by digging around in the MIR JSON file, if you’d like. (In a future version of SAW, one will be able to look this name up more easily.)

Once we change the identifier:

quarter_round_ov <-
  mir_verify m "salsa20::core#1::quarter_round" [] false quarter_round_spec z3;

We can run SAW once more. This time, SAW complains about a different thing:

[01:00:19.697] Verifying salsa20/10e438b3::core#1[0]::quarter_round[0] ...
[01:00:19.714] Simulating salsa20/10e438b3::core#1[0]::quarter_round[0] ...
[01:00:19.717] Checking proof obligations salsa20/10e438b3::core#1[0]::quarter_round[0] ...
[01:00:19.739] Subgoal failed: salsa20/10e438b3::core#1[0]::quarter_round[0] index out of bounds: the length is move _10 but the index is _9
[01:00:19.739] SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = 53}
[01:00:19.739] ----------Counterexample----------
[01:00:19.739]   a: 2147483648

Here, SAW complains that we have an index out of bounds. Recall that we are indexing into the state array, which is of length 16, using the a/b/c/d arguments. Each of these arguments are of type usize, and because we are declaring these to be symbolic, it is quite possible for each argument to be 16 or greater, which would cause the index into state to be out of bounds.

In practice, however, the only values of a/b/c/d that we will use are less than 16. We can express this fact as a precondition:

  mir_precond {{ a < `STATE_WORDS /\
                 b < `STATE_WORDS /\
                 c < `STATE_WORDS /\
                 d < `STATE_WORDS }};

That is enough to finally get SAW to verify this very stripped-down version of quarter_round_spec. Some good progress! But we aren’t done yet, as we don’t yet say what happens to the value that state points to after the function returns. This will be a requirement if we want to use quarter_round_spec in compositional verification (and we do want this), so we should address this shortly.

Recall that unlike the Rust quarter_round function, the Cryptol quarterround function doesn’t have a state argument. This is because the Rust function does slightly more than what the Cryptol function does. The Rust function will look up elements of the state array, use them to perform the computations that the Cryptol function does, and then insert the new values back into the state array. To put it another way: the Rust function can be thought of as a wrapper around the Cryptol function that also performs an in-place bulk update of the state array.

In Cryptol, one can look up elements of an array using the (@@) function, and one can perform in-place array updates using the updates function. This translates into a postcondition that looks like this:

  let indices = {{ [a, b, c, d] }};
  let state_arr' = {{ updates state_arr indices (quarterround (state_arr @@ indices)) }};
  mir_points_to state_ref (mir_term state_arr');

What does SAW think of this? Someone surprisingly, SAW finds a counterexample:

[01:43:30.065] Verifying salsa20/10e438b3::core#1[0]::quarter_round[0] ...
[01:43:30.078] Simulating salsa20/10e438b3::core#1[0]::quarter_round[0] ...
[01:43:30.084] Checking proof obligations salsa20/10e438b3::core#1[0]::quarter_round[0] ...
[01:43:30.801] Subgoal failed: salsa20/10e438b3::core#1[0]::quarter_round[0] Literal equality postcondition

[01:43:30.801] SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = 1999}
[01:43:30.802] ----------Counterexample----------
[01:43:30.802]   a: 13
[01:43:30.802]   b: 3
[01:43:30.802]   c: 0
[01:43:30.802]   d: 0
[01:43:30.802]   state: [3788509705, 0, 0, 3223325776, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1074561051, 0, 0]

Note that in this counterexample, the values of c and d are the same. In the Rust version of the function, each element in state is updated sequentially, so if two of the array indices are the same, then the value that was updated with the first index will later be overwritten by the value at the later index. In the Cryptol version of the function, however, all of the positions in the array are updated simultaneously. This implicitly assumes that all of the array indices are disjoint from each other, an assumption that we are not encoding into quarter_round_spec’s preconditions.

At this point, it can be helpful to observe how the quarter_round function is used in practice. The call sites are found in the rounds function:

            // column rounds
            quarter_round(0, 4, 8, 12, state);
            quarter_round(5, 9, 13, 1, state);
            quarter_round(10, 14, 2, 6, state);
            quarter_round(15, 3, 7, 11, state);

            // diagonal rounds
            quarter_round(0, 1, 2, 3, state);
            quarter_round(5, 6, 7, 4, state);
            quarter_round(10, 11, 8, 9, state);
            quarter_round(15, 12, 13, 14, state);

Here, we can see that the values of a/b/c/d will only ever be chosen from a set of eight possible options. We can take advantage of this fact to constrain the possible set of values for a/b/c/d. The latest iteration of the quarter_round_spec is now:

let quarter_round_spec = do {
  a <- mir_fresh_var "a" mir_usize;
  b <- mir_fresh_var "b" mir_usize;
  c <- mir_fresh_var "c" mir_usize;
  d <- mir_fresh_var "d" mir_usize;
  let indices = {{ [a, b, c, d] }};
  mir_precond {{    indices == [0, 1, 2, 3]
                 \/ indices == [5, 6, 7, 4]
                 \/ indices == [10, 11, 8, 9]
                 \/ indices == [15, 12, 13, 14]
                 \/ indices == [0, 4, 8, 12]
                 \/ indices == [5, 9, 13, 1]
                 \/ indices == [10, 14, 2, 6]
                 \/ indices == [15, 3, 7, 11]
              }};
  state_ref <- mir_alloc_mut (mir_array STATE_WORDS mir_u32);
  state_arr <- mir_fresh_var "state" (mir_array STATE_WORDS mir_u32);
  mir_points_to state_ref (mir_term state_arr);

Note that:

The indices value is constrained (via a precondition) to be one of the set of values that is chosen in the rounds function. (Note that \/ is the logical-or function in Cryptol.) Each of these are concrete values that are less than STATE_WORDS (16), so we no longer need a precondition stating a < `STATE_WORDS /\ ....
Because we now reference indices in the preconditions, we have moved its definition up. (Previously, it was defined in the postconditions section.)

With this in place, will SAW verify quarter_round_spec now?

[02:14:02.037] Verifying salsa20/10e438b3::core#1[0]::quarter_round[0] ...
[02:14:02.051] Simulating salsa20/10e438b3::core#1[0]::quarter_round[0] ...
[02:14:02.057] Checking proof obligations salsa20/10e438b3::core#1[0]::quarter_round[0] ...
[02:14:18.616] Proof succeeded! salsa20/10e438b3::core#1[0]::quarter_round[0]

At long last, it succeeds. Hooray! SAW does have to think for a while, however, as this proof takes about 17 seconds to complete. It would be unfortunate to have to wait 17 seconds on every subsequent invocation of SAW, and since we still have other functions to verify, this is a very real possibility. For this reason, it can be helpful to temporarily turn this use of mir_verify into a mir_unsafe_assume_spec:

quarter_round_ov <-
  mir_unsafe_assume_spec m "salsa20::core#1::quarter_round" quarter_round_spec;
  // Temporarily commented out to save time:
  //
  // mir_verify m "salsa20::core#1::quarter_round" [] false quarter_round_spec z3;

Once we are done with the entire proof, we can come back and remove this use of mir_unsafe_assume_spec, as we’re only using it as a time-saving measure.

Verifying the `rounds` function

Now that we’ve warmed up, let’s try verifying the rounds function, which is where quarter_round is invoked. Here is the full definition of rounds:

    fn rounds(&mut self, state: &mut [u32; STATE_WORDS]) {
        for _ in 0..(R::COUNT / 2) {
            // column rounds
            quarter_round(0, 4, 8, 12, state);
            quarter_round(5, 9, 13, 1, state);
            quarter_round(10, 14, 2, 6, state);
            quarter_round(15, 3, 7, 11, state);

            // diagonal rounds
            quarter_round(0, 1, 2, 3, state);
            quarter_round(5, 6, 7, 4, state);
            quarter_round(10, 11, 8, 9, state);
            quarter_round(15, 12, 13, 14, state);
        }

        for (s1, s0) in state.iter_mut().zip(&self.state) {
            *s1 = s1.wrapping_add(*s0);
        }
    }

First, rounds performs COUNT rounds on the state argument. After this, it takes each element of self.state and adds it to the corresponding element in state.

Linking back at the Salsa20 spec, we can see that the rounds function is almost an implementation of the Salsa20(x) hash function. The only notable difference is that while the Salsa20(x) hash function converts the results to little-endian form, the rounds function does not. Salsa20.cry implements this part of the spec here:

Salsa20 : [32] -> [64][8] -> [64][8]
Salsa20 count xs = littleendian_state_inverse (Salsa20_rounds count xw xw)
  where
    xw = littleendian_state xs

Salsa20_rounds : [32] -> [16][32] -> [16][32] -> [16][32]
Salsa20_rounds count xw xw' = xw + zs@(count/2)
  where
    zs = [xw'] # [ doubleround zi | zi <- zs ]

Where Salsa20 is the hash function, and Salsa20_rounds is the part of the hash function that excludes the little-endian conversions. In other words, Salsa20_rounds precisely captures the behavior of the Rust rounds function.

One aspect of the rounds function that will make verifying it slightly different from verifying quarter_rounds is that rounds is defined in an impl block for the Core struct. This means that the &mut self argument in rounds has the type &mut Core<R>. As such, we will have to look up the Core ADT in SAW using mir_find_adt.

This raises another question, however: when looking up Core<R>, what type should we use to instantiate R? As noted above, our choices are R8, R12, and R20, depending on how many rounds you want. For now, we’ll simply hard-code it so that R is instantiated to be R8, but we will generalize this a bit later.

Alright, enough chatter—time to start writing a proof. First, let’s look up the R8 ADT. This is defined in the salsa20 crate in the rounds.rs file, so its identifier becomes salsa20::rounds::R8:

let r_adt = mir_find_adt m "salsa20::rounds::R8" [];

Next, we need to look up the PhantomData<R8> ADT, which is used in the rounds field of the Core<R8> struct. This is defined in core::marker:

let phantom_data_adt = mir_find_adt m "core::marker::PhantomData" [mir_adt r_adt];

Finally, we must look up Core<R8> itself. Like quarter_round, the Core struct is defined in salsa20::core#1:

let core_adt = mir_find_adt m "salsa20::core#1::Core" [mir_adt r_adt];

Now that we have the necessary prerequisites, let’s write a spec for the rounds function. First, we need to allocate a reference for the self argument:

let rounds_spec = do {
  self_ref <- mir_alloc_mut (mir_adt core_adt);

Next, we need to create symbolic values for the fields of the Core struct, which self_ref will point to. The self.state field will be a fresh array, and the self.rounds field will be a simple, empty struct value:

  self_state <- mir_fresh_var "self_state" (mir_array STATE_WORDS mir_u32);
  let self_rounds = mir_struct_value phantom_data_adt [];

Finally, putting all of the self values together:

  let self_val = mir_struct_value core_adt [mir_term self_state, self_rounds];
  mir_points_to self_ref self_val;

Next, we need a state argument (not to be confused with the self.state field in Core). This is handled much the same as it was in quarter_round_spec:

  state_ref <- mir_alloc_mut (mir_array STATE_WORDS mir_u32);
  state_arr <- mir_fresh_var "state" (mir_array STATE_WORDS mir_u32);
  mir_points_to state_ref (mir_term state_arr);

Lastly, we cap it off with a call to mir_execute_func:

  mir_execute_func [self_ref, state_ref];
};

(Again, we’re missing some postconditions describing what self_ref and state_ref point to after the function returns, but we’ll return to that in a bit.)

If we run SAW at this point, we see that everything in rounds_spec typechecks, so we’re off to a good start. Let’s keep going and add a mir_verify call.

Here, we are faced with an interesting question: what is the identifier for rounds::<R8>? The rounds function is defined using generics, so we can’t verify it directly—we must instead verify a particular instantiation of rounds. At present, there isn’t a good way to look up what the identifiers for instantiations of generic functions are (there will be in the future), but it turns out that the identifier for rounds::<R8> is this:

rounds_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::rounds::_inst6e4a2d7250998ef7" [quarter_round_ov] false rounds_spec z3;

Note that we are using quarter_round_ov as a compositional override. Once again, SAW is happy with our work thus far:

[03:12:35.990] Proof succeeded! salsa20/10e438b3::core#1[0]::{impl#0}[0]::rounds[0]::_inst6e4a2d7250998ef7[0]

Nice. Now let’s go back and fill in the missing postconditions in rounds_spec. In particular, we must declare what happens to both self_ref and state_ref. A closer examination of the code in the Rust rounds function reveals that the self argument is never modified at all, so that part is easy:

  mir_points_to self_ref self_val;

The state argument, on the other hand, is modified in-place. This time, our job is made easier by the fact that Salsa20_rounds implements exactly what we need. Because we are instantiating rounds at type R8, we must explicitly state that we are using 8 rounds:

  mir_points_to state_ref (mir_term {{ Salsa20_rounds 8 self_state state_arr }});

Once again, SAW is happy with our work. We’re on a roll!

Now let’s address the fact that we are hard-coding everything to R8, which is somewhat uncomfortable. We can make things better by allowing the user to specify the number of rounds. The first thing that we will need to change is the r_adt definition, which is response for looking up R8. We want to turn this into a function that, depending on the user input, will look up R8, R12, or R20:

let r_adt num_rounds = mir_find_adt m (str_concat "salsa20::rounds::R" (show num_rounds)) [];

Where str_concat is a SAW function for concatenating strings together:

sawscript> :type str_concat
String -> String -> String

We also want to parameterize phantom_data_adt and core_adt:

let phantom_data_adt r = mir_find_adt m "core::marker::PhantomData" [mir_adt r];
let core_adt r = mir_find_adt m "salsa20::core#1::Core" [mir_adt r];

Next, we need to parameterize rounds_spec by the number of rounds. This will require changes in both the preconditions and postconditions. On the preconditions side, we must pass the number of rounds to the relevant functions:

let rounds_spec num_rounds = do {
  let r = r_adt num_rounds;
  let core_adt_inst = core_adt r;
  self_ref <- mir_alloc_mut (mir_adt core_adt_inst);
  self_state <- mir_fresh_var "self_state" (mir_array STATE_WORDS mir_u32);
  let self_rounds = mir_struct_value (phantom_data_adt r) [];
  let self_val = mir_struct_value core_adt_inst [mir_term self_state, self_rounds];

And on the postconditions side, we must pass the number of rounds to the Cryptol Salsa20_rounds function:

  mir_points_to state_ref (mir_term {{ Salsa20_rounds `num_rounds self_state state_arr }});
};

Finally, we must adjust the call to rounds_spec in the context of mir_verify so that we pick 8 as the number of rounds:

rounds_8_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::rounds::_inst6e4a2d7250998ef7" [quarter_round_ov] false (rounds_spec 8) z3;

SAW is happy with this generalization. To demonstrate that we have generalized things correctly, we can also verify the same function at R20 instead of R8:

rounds_20_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::rounds::_instfa33e77d840484a0" [quarter_round_ov] false (rounds_spec 20) z3;

The only things that we had to change were the identifier and the argument to rounds_spec. Not bad!

Verifying the `counter_setup` function

We’re very nearly at the point of being able to verify apply_keystream. Before we do, however, there is one more function that apply_keystream calls, which we ought to verify first: counter_setup. Thankfully, the implementation of counter_setup is short and sweet:

    pub(crate) fn counter_setup(&mut self, counter: u64) {
        self.state[8] = (counter & 0xffff_ffff) as u32;
        self.state[9] = ((counter >> 32) & 0xffff_ffff) as u32;
    }

This updates the elements of the state array at indices 8 and 9 with the lower 32 bits and the upper 32 bits of the counter argument, respecitvely. At a first glance, there doesn’t appear to be any function in Salsa20.cry that directly corresponds to what counter_setup does. This is a bit of a head-scratcher, but the answer to this mystery will become more apparent as we get further along in the proof.

For now, we should take matters into our own hands and write our own Cryptol spec for counter_setup. To do this, we will create a new Cryptol file named Salsa20Extras.cry, which imports from Salsa20.cry:

module Salsa20Extras where

import Salsa20

The Cryptol implementation of counter_setup will need arrays of length STATE_WORDS, so we shall define STATE_WORDS first:

type STATE_WORDS = 16

Note that we preceded this definition with the type keyword. In Cryptol, sequence lengths are encoded at the type level, so if we want to use STATE_WORDS at the type level, we must declare it as a type.

Finally, we can write a Cryptol version of counter_setup using our old friend updates to perform a bulk sequence update:

counter_setup : [STATE_WORDS][32] -> [64] -> [STATE_WORDS][32]
counter_setup state counter =
  updates state [8, 9] [drop counter, drop (counter >> 32)]

Note that counter is a 64-bit word, but the elements of the state sequence are 32-bit words. As a result, we have to explicitly truncate counter and counter >> 32 to 32-bit words by using the drop function, which drops the first 32 bits from each word.

Returning to salsa20.saw, we must now make use of our new Cryptol file by importing it at the top:

import "Salsa20Extras.cry";

With the counter_setup Cryptol implementation in scope, we can now write a spec for the Rust counter_setup function. There’s not too much to remark on here, as the spec proves relatively straightforward to write:

let counter_setup_spec num_rounds = do {
  let r = r_adt num_rounds;
  let core_adt_inst = core_adt r;
  self_ref <- mir_alloc_mut (mir_adt core_adt_inst);
  self_state <- mir_fresh_var "self_state" (mir_array STATE_WORDS mir_u32);
  let self_rounds = mir_struct_value (phantom_data_adt r) [];
  let self_val = mir_struct_value core_adt_inst [mir_term self_state, self_rounds];
  mir_points_to self_ref self_val;

  counter <- mir_fresh_var "counter" mir_u64;

  mir_execute_func [self_ref, mir_term counter];

  let self_state' = {{ counter_setup self_state counter }};
  let self_val' = mir_struct_value core_adt_inst [mir_term self_state', self_rounds];
  mir_points_to self_ref self_val';
};

We can now verify counter_setup against counter_setup_spec at lengths 8 and 20:

counter_setup_8_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::counter_setup::_inst6e4a2d7250998ef7" [] false (counter_setup_spec 8) z3;
counter_setup_20_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::counter_setup::_instfa33e77d840484a0" [] false (counter_setup_spec 20) z3;

That wasn’t so bad. It’s a bit unsatisfying that we had to resort to writing a Cryptol function not found in Salsa20.cry, but go along with this for now—it will become apparent later why this needed to be done.

Verifying the `apply_keystream` function (first attempt)

It’s time. Now that we’ve verified rounds and counter_setup, it’s time to tackle the topmost function in the call stack: apply_keystream:

    pub fn apply_keystream(&mut self, counter: u64, output: &mut [u8]) {
        debug_assert_eq!(output.len(), BLOCK_SIZE);
        self.counter_setup(counter);

        let mut state = self.state;
        self.rounds(&mut state);

        for (i, chunk) in output.chunks_mut(4).enumerate() {
            for (a, b) in chunk.iter_mut().zip(&state[i].to_le_bytes()) {
                *a ^= *b;
            }
        }
    }

There aren’t that many lines of code in this function, but there is still quite a bit going on. Let’s walk through apply_keystream in more detail:

The output argument represents the message to encrypt (or decrypt). output is a slice of bytes, so in principle, output can have an arbitrary length. That being said, the first line of apply_keystream’s implementation checks that output’s length is equal to BLOCK_SIZE:
```
        debug_assert_eq!(output.len(), BLOCK_SIZE);
```
Where BLOCK_SIZE is defined here:
```
/// Size of a Salsa20 block in bytes
pub const BLOCK_SIZE: usize = 64;
```
So in practice, output must have exactly 64 elements.
Next, apply_keystream invokes the counter_setup and rounds functions to set up the keystream (the local state variable).
Finally, apply_keystream combines the keystream with output. It does so by chunking output into a sequence of 4 bytes, and then it XOR’s the value of each byte in-place with the corresponding byte from the keystream. This performs little-endian conversions as necessary.

The fact that we are XOR’ing bytes strongly suggests that this is an implementation of the Salsa20 encryption function from the spec. There is an important difference between how the Salsa20 spec defines the encryption function versus how apply_keystream defines it, however. In the Salsa20 spec, encryption is a function of a key, nonce, and a message. apply_keystream, on the other hand, is a function of self’s internal state, a counter, and a message. The two aren’t quite the same, which is makes it somewhat tricky to describe one in terms of the other.

Salsa20.cry defines a straightforward Cryptol port of the Salsa20 encryption function from the spec, named Salsa20_encrypt. Because it takes a key and a nonce as an argument, it’s not immediately clear how we’d tie this back to apply_keystream. But no matter: we can do what we did before and define our own Cryptol version of apply_keystream in Salsa20Extras.cry:

apply_keystream : [32] -> [STATE_WORDS][32] -> [64] -> [BLOCK_SIZE][8] -> [BLOCK_SIZE][8]
apply_keystream count state0 counter output =
    output ^ littleendian_state_inverse state2
  where
    state1 = counter_setup state0 counter
    state2 = Salsa20_rounds count state1 state1

This implementation builds on top of the Cryptol counter_setup and Salsa20_rounds functions, which we used as the reference implementations for the Rust counter_setup and rounds functions, respectively. We also make sure to define a BLOCK_SIZE type alias at the top of the file:

type BLOCK_SIZE = 64

Now let’s write a SAW spec for apply_keystream. Once again, we will need to reference BLOCK_SIZE when talking about the output-related parts of the spec, so make sure to define BLOCK_SIZE at the top of the .saw file:

let BLOCK_SIZE = 64;

First, we need to declare all of our arguments, which proceeds as you would expect:

let apply_keystream_spec num_rounds = do {
  let r = r_adt num_rounds;
  let core_adt_inst = core_adt r;
  self_ref <- mir_alloc_mut (mir_adt core_adt_inst);
  self_state <- mir_fresh_var "self_state" (mir_array STATE_WORDS mir_u32);
  let self_rounds = mir_struct_value (phantom_data_adt r) [];
  let self_val = mir_struct_value core_adt_inst [mir_term self_state, self_rounds];
  mir_points_to self_ref self_val;

  counter <- mir_fresh_var "counter" mir_u64;

  output_arr <- mir_fresh_var "output_arr" (mir_array BLOCK_SIZE mir_u8);
  output_ref <- mir_alloc_mut (mir_array BLOCK_SIZE mir_u8);
  mir_points_to output_ref (mir_term output_arr);
  let output = mir_slice_value output_ref;

  mir_execute_func [self_ref, mir_term counter, output];

What about the postconditions? We have two mutable references to contend with: self_ref and output_ref. The postcondition for self_ref is fairly straightforward: the only time it is ever modified is when counter_setup is called. This means that after the apply_keystream function has returned, self_ref will point to the results of calling the counter_setup Cryptol function:

  let self_state' = {{ counter_setup self_state counter }};
  let self_val' = mir_struct_value core_adt_inst [mir_term self_state', self_rounds];
  mir_points_to self_ref self_val';

output_ref is where the interesting work happenings. After the Rust apply_keystream function has returned, it will point to the results of calling the Cryptol apply_keystream function that we just defined:

  mir_points_to output_ref (mir_term {{ apply_keystream `num_rounds self_state counter output_arr }});
};

Finally, we can put this all together and verify apply_keystream against apply_keystream_spec at lengths 8 and 20:

apply_keystream_8_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::apply_keystream::_inst6e4a2d7250998ef7" [counter_setup_8_spec_ov, rounds_8_spec_ov] false (apply_keystream_spec 8) z3;
apply_keystream_20_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::apply_keystream::_instfa33e77d840484a0" [counter_setup_20_spec_ov, rounds_20_spec_ov] false (apply_keystream_spec 20) z3;

SAW will successfully verify these. We’ve achieved victory… or have we? Recall that we had to tailor the Cryptol apply_keystream function to specifically match the behavior of the corresponding Rust code. This makes the proof somewhat underwhelming, since the low-level implementation is nearly identical to the high-level spec.

A more impressive proof would require linking apply_keystream to a Cryptol function in the Salsa20.cry file, which was developed independently of the Rust code. As we mentioned before, however, doing so will force us to reconcile the differences in the sorts of arguments that each function takes, as apply_keystream doesn’t take a key or nonce argument. Time to think for a bit.

Verifying the `new_raw` function

At this point, we should ask ourselves: why doesn’t apply_keystream take a key or nonce argument? The reason lies in the fact that the salsa20 crate implements Salsa20 in a stateful way. Specifically, the Core struct stores internal state that is used to compute the keystream to apply when hashing. In order to use this internal state, however, we must first initialize it. The new function that is responsible for this initialization:

    /// Initialize core function with the given key and IV
    pub fn new(key: &Key, iv: &Nonce) -> Self {
        Self::new_raw(key.as_ref(), iv.as_ref())
    }

Sure enough, this function takes a key and a nonce as an argument! This is a critical point that we overlooked. When using the salsa20 crate, you wouldn’t use the apply_keystream function in isolation. Instead, you would create an initial Core value using new, and then you would invoke apply_keystream. The Salsa20 spec effectively combines both of these operations in is encryption function, whereas the salsa20 splits these two operations into separate functions altogether.

Strictly speaking, we don’t need to verify new in order to verify apply_keystream, as the latter never invokes the former. Still, it will be a useful exercise to verify new, as the insights we gain when doing so will help us write a better version of apply_keystream_spec.

All that being said, we probably to verify new_raw (a lower-level helper function) rather than new itself. This is because the definitions of Key and Nonce are somewhat involved. For instance, Key is defined as:

pub type Key = cipher::generic_array::GenericArray<u8, U32>;

GenericArray is a somewhat complicated abstraction. Luckily, we don’t really need to deal with it, since new_raw deals with simple array references rather than GenericArrays:

    /// Initialize core function with the given key and IV
    pub fn new_raw(key: &[u8; 32], iv: &[u8; 8]) -> Self {

The full implementation of new_raw is rather long, so we won’t inline the whole thing here. At a high level, it initializes the state array of a Core value by populating each element of the array with various things. Some elements of the array are populated with key, some parts are populated with iv (i.e., the nonce), and other parts are populated with an array named CONSTANTS:

/// State initialization constant ("expand 32-byte k")
const CONSTANTS: [u32; 4] = [0x6170_7865, 0x3320_646e, 0x7962_2d32, 0x6b20_6574];

The comment about "expand 32-byte k" is a strong hint that new_raw is implementing a portion of the Salsa20 expansion function from the spec. (No really, the spec literally says to use the exact string "expand 32-byte k"—look it up!) The Salsa20.cry Cryptol file has an implementation of this portion of the expansion function, which is named Salsa20_init:

Salsa20_init : {a} (a >= 1, 2 >= a) => ([16*a][8], [16][8]) -> [64][8]
Salsa20_init(k, n) = x
  where
    [s0, s1, s2, s3] = split "expand 32-byte k" : [4][4][8]
    [t0, t1, t2, t3] = split "expand 16-byte k" : [4][4][8]
    x = if(`a == 2) then s0 # k0 # s1 # n # s2 # k1 # s3
                    else t0 # k0 # t1 # n # t2 # k0 # t3
    [k0, k1] = (split(k#zero)):[2][16][8]

Note that we were careful to say a portion of the Salsa20 expansion function. There is also a Cryptol implementation of the full expansion function, named Salsa20_expansion:

Salsa20_expansion : {a} (a >= 1, 2 >= a) => ([32], [16*a][8], [16][8]) -> [64][8]
Salsa20_expansion(count, k, n) = Salsa20 count (Salsa20_init(k, n))

This calls Salsa20_init followed by Salsa20, the latter of which performs hashing. Importantly, new_raw does not do any hashing on its own, just initialization. For this reason, we want to use Salsa20_init as the reference implementation of new_raw, not Salsa20_expansion.

Alright, time to write a SAW spec. The first part of the spec is straightforward:

let new_raw_spec num_rounds = do {
  key_ref <- mir_alloc (mir_array 32 mir_u8);
  key_arr <- mir_fresh_var "key_arr" (mir_array 32 mir_u8);
  mir_points_to key_ref (mir_term key_arr);

  nonce_ref <- mir_alloc (mir_array 8 mir_u8);
  nonce_arr <- mir_fresh_var "nonce" (mir_array 8 mir_u8);
  mir_points_to nonce_ref (mir_term nonce_arr);

  mir_execute_func [key_ref, nonce_ref];

As is usually the case, the postconditions are the tricky part. We know that the behavior of new_raw will roughly coincide with the Salsa20_init function, so let’s try that first:

  let r = r_adt num_rounds;
  let self_state = {{ Salsa20_init(key_arr, nonce_arr) }};
  let self_rounds = mir_struct_value (phantom_data_adt r) [];
  let self_val = mir_struct_value (core_adt r) [mir_term self_state, self_rounds];
  mir_return self_val;

If we attempt to verify this using mir_verify:

new_raw_8_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::new_raw::_inst6e4a2d7250998ef7" [] false (new_raw_spec 8) z3;
new_raw_20_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::new_raw::_instfa33e77d840484a0" [] false (new_raw_spec 20) z3;

SAW complains thusly:

Cryptol error:
[error] at salsa20.saw:109:45--109:54:
  Type mismatch:
    Expected type: 16
    Inferred type: 8
    Context: [ERROR] _
    When checking type of 2nd tuple field

Here, the 2nd tuple field is the nonce_arr in Salsa20_init(key_arr, nonce_arr). And sure enough, Salsa20_init expects the 2nd tuple field to be a sequence of 16 elements, but nonce_arr only has 8 elements. Where do we get the remaining 8 elements from?

The answer to this question can be found by looking at the implementation of new_raw more closely. Let’s start at this code:

        for (i, chunk) in iv.chunks(4).enumerate() {
            state[6 + i] = u32::from_le_bytes(chunk.try_into().unwrap());

This will chunk up iv (the nonce) into two 4-byte chunks and copies them over to the elements of state array at indices 6 and 7. This is immediately followed by two updates at indices 8 and 9, which are updated to be 0:

        state[8] = 0;
        state[9] = 0;

If you take the two 4-bytes chunks of iv and put two 4-byte 0 values after them, then you would have a total of 16 bytes. This suggests that the nonce value that Salsa20_init expects is actually this:

nonce_arr # zero : [16][8]

Where zero : [8][8] is a Cryptol expression that returns all zeroes, and (#) is the Cryptol operator for concatenating two sequences together. Let’s update new_raw_spec to reflect this:

  let self_state = {{ Salsa20_init(key_arr, nonce_arr # zero) }};

This is closer to what we want, but not quite. SAW still complains:

could not match specified value with actual value:
  ...
  type of actual value:    [u32; 16]
  type of specified value: [u8; 64]

This is because Salsa20_init returns something of type [64][8], which corresponds to the Rust type [u8; 64]. self.state, on the other hand, is of type [u32; 16]. These types are very close, as they both contain the same number of bytes, but they are chunked up differently. Recall the code that copies the nonce value over to self.state:

        for (i, chunk) in iv.chunks(4).enumerate() {
            state[6 + i] = u32::from_le_bytes(chunk.try_into().unwrap());

In order to resolve the type differences between iv and state, this code needed to explicitly convert iv to little-endian form using the u32::from_le_bytes function. There is a similar Cryptol function in Salsa20.cry named littleendian_state:

littleendian_state : [64][8] -> [16][32]
littleendian_state b = [littleendian xi | xi <- split b]

Note that [64][8] is the Cryptol equivalent of [u8; 64], and [16][32] is the Cryptol equivalent of [u32; 16]. As such, this is exactly the function that we need to resolve the differences in types:

  let self_state = {{ littleendian_state (Salsa20_init(key_arr, nonce_arr # zero)) }};

With that change, SAW is finally happy with new_raw_spec and successfully verifies it.

There is an interesting connection between the new_raw and counter_setup functions. Both functions perform in-place updates on state at indices 8 and 9. Whereas new_raw always sets these elements of state to 0, counter_setup will set them to the bits of the counter argument (after converting counter to little-endian form). This means that if you invoke counter_setup right after new_raw, then counter_setup would overwrite the 0 values with the counter argument. In order words, it would be tantamount to initializing state like so:

littleendian_state (Salsa20_init(key, nonce # littleendian_inverse counter))

Where littleendian_inverse (a sibling of littleendian_state) converts a [64] value to a [8][8] one. This pattern is a curious one…

Verifying the `apply_keystream` function (second attempt)

Let’s now return to the problem of linking apply_keystream up to Salsa20_encrypt. In particular, let’s take a closer look at the definition of Salsa20_encrypt itself:

Salsa20_encrypt : {a, l} (a >= 1, 2 >= a, l <= 2^^70) => ([32], [16*a][8], [8][8], [l][8]) -> [l][8]
Salsa20_encrypt(count, k, v, m) = c
  where
    salsa = take (join [ Salsa20_expansion(count, k, v#(littleendian_inverse i)) | i <- [0, 1 ... ] ])

Does anything about this definition strike you as interesting? Take a look at the v#(littleendian_inverse i) part—we just saw a use of littleendian_inverse earlier in our discussion about initializing the state! Moreover, v is the nonce argument, so it is becoming clearer that Sals20_encrypt is creating an initial state is much the same way that new_raw is.

A related question: what is the i value? The answer is somewhat technical: the Salsa20 encryption function is designed to work with messages with differing numbers of bytes (up to 2^^70 bytes, to be exact). Each 8-byte chunk in the message will be encrypted with a slightly difference nonce. For instance, the first 8-byte chunk’s nonce will have its lower 32 bits set to 0, the second 8-byte chunk’s nonce will have its lower 32 bits set to 1, and so on. In general, the ith 8-byte chunk’s nonce will have its lower 32 bits set to i, and this corresponds exactly to the i in the expression littleendian_inverse i.

Note, however, that apply_keystream only ever uses a message that consists of exactly eight 8-byte chunks. This means that Salsa20_encrypt will only ever invoke Salsa20_expansion once with a nonce value where the lower 32 bits are set to 0. That is, it will perform encryption with an initial state derived from:

Salsa20_init(k, v#(littleendian_inverse zero))

Which can be further simplified to Salsa20_init(k, v # zero). This is very nearly what we want, as this gives us the behavior of the Rust new_raw function. There’s just one problem though: it doesn’t take the behavior of counter_setup into account. How do we go from zero to littleendian_inverse counter?

While Salsa20_encrypt doesn’t take counters into account at all, it is not too difficult to generalize Salsa20_encrypt in this way. There is a variant of Salsa20_encrypt in the same file named Salsa20_encrypt_with_offset, where the offset argument o serves the same role that counter does in counter_setup:

Salsa20_encrypt_with_offset : {a, l} (a >= 1, 2 >= a, l <= 2^^70) =>
    ([32], [16*a][8], [8][8], [64], [l][8]) -> [l][8]
Salsa20_encrypt_with_offset(count, k, v, o, m) = c
  where
    salsa = take (join [ Salsa20_expansion(count, k, v#(littleendian_inverse (o + i))) | i <- [0, 1 ... ] ])
    c = m ^ salsa

(Observe that Salsa20_encrypt(count, k, v, m) is equivalent to Salsa20_encrypt_with_offset(count, k, v, 0, m).)

At long last, we have discovered the connection between apply_keystream and the Salsa20 spec. If you assume that you invoke new_raw beforehand, then the behavior of apply_keystream corresponds exactly to that of Salsa20_encrypt_with_offset. This insight will inform us how to write an alternative SAW spec for apply_keystream:

let apply_keystream_alt_spec num_rounds = do {
  key <- mir_fresh_var "key" (mir_array 32 mir_u8);
  nonce <- mir_fresh_var "nonce" (mir_array 8 mir_u8);
  counter <- mir_fresh_var "counter" mir_u64;

  let r = r_adt num_rounds;
  let core_adt_inst = core_adt r;
  self_ref <- mir_alloc_mut (mir_adt core_adt_inst);
  let self_state = {{ littleendian_state (Salsa20_init(key, nonce # littleendian_inverse counter)) }};
  let self_rounds = mir_struct_value (phantom_data_adt r) [];
  let self_val = mir_struct_value core_adt_inst [mir_term self_state, self_rounds];
  mir_points_to self_ref self_val;

Observe the following differences between apply_keystream_alt_spec and our earlier apply_keystream_spec:

In apply_keystream_alt_spec, we declare fresh key and nonce values, which weren’t present at all in apply_keystream_spec.
In apply_keystream_alt_spec, we no longer make self_state a fresh, unconstrained value. Instead, we declare that it must be the result of calling Salsa20_init on the key, nonce, and counter values. This is the part that encodes the assumption that new_raw was invoked beforehand.

The parts of the spec relating to output remain unchanged:

  output_arr <- mir_fresh_var "output_arr" (mir_array BLOCK_SIZE mir_u8);
  output_ref <- mir_alloc_mut (mir_array BLOCK_SIZE mir_u8);
  mir_points_to output_ref (mir_term output_arr);
  let output = mir_slice_value output_ref;

  mir_execute_func [self_ref, mir_term counter, output];

The postconditions are slightly different in apply_keystream_alt_spec. While the parts relating to self_ref remain unchanged, we now have output_ref point to the results of calling Salsa20_encrypt_with_offset:

  let self_state' = {{ counter_setup self_state counter }};
  let self_val' = mir_struct_value core_adt_inst [mir_term self_state', self_rounds];
  mir_points_to self_ref self_val';
  mir_points_to output_ref (mir_term {{ Salsa20_encrypt_with_offset(`num_rounds, key, nonce, counter, output_arr) }});

Tying this all together, we call mir_verify, making sure to use compositional overrides involving counter_setup and rounds:

apply_keystream_alt_8_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::apply_keystream::_inst6e4a2d7250998ef7" [counter_setup_8_spec_ov, rounds_8_spec_ov] false (apply_keystream_alt_spec 8) z3;
apply_keystream_alt_20_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::apply_keystream::_instfa33e77d840484a0" [counter_setup_20_spec_ov, rounds_20_spec_ov] false (apply_keystream_alt_spec 20) z3;

At long last, it is time to run SAW on this. When we do, we see this:

[15:11:44.576] Checking proof obligations salsa20/10e438b3::core#1[0]::{impl#0}[0]::apply_keystream[0]::_inst6e4a2d7250998ef7[0] ...

After this, SAW loops forever. Oh no! While somewhat disheartening, this is a reality of SMT-based verification that we must content with. SMT solvers are extremely powerful, but their performance can sometimes be unpredictable. The task of verifying apply_keystream_alt_spec is just complicated enough that Z3 cannot immediately figure out that the proof is valid, so it resorts to much slower algorithms to solve proof goals.

We could try waiting for Z3 to complete, but we’d be waiting for a long time. It’s not unheard of for SMT solvers to take many hours on especially hard problems, but we don’t have that many hours to spare. We should try a slightly different approach instead.

When confronted with an infinite loop in SAW, there isn’t a one-size-fits-all solution that will cure the problem. Sometimes, it is worth stating your SAW spec in a slightly different way such that the SMT solver can spot patterns that it couldn’t before. Other times, it can be useful to try and break the problem up into smaller functions and use compositional verification to handle the more complicated subfunctions. As we mentioned before, the performance of SMT solvers in unpredictable, and it’s not always obvious what the best solution is.

In this example, however, the problem lies with Z3 itself. As it turns out, Yices (a different SMT solver) can spot the patterns needed to prove apply_keystream_alt_spec immediately. Fortunately, SAW includes support for both Z3 and Yices. In order to switch from Z3 to Yices, swap out the z3 proof script with yices:

apply_keystream_alt_8_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::apply_keystream::_inst6e4a2d7250998ef7" [counter_setup_8_spec_ov, rounds_8_spec_ov] false (apply_keystream_alt_spec 8) yices;
apply_keystream_alt_20_spec_ov <-
  mir_verify m "salsa20::core#1::{impl#0}::apply_keystream::_instfa33e77d840484a0" [counter_setup_20_spec_ov, rounds_20_spec_ov] false (apply_keystream_alt_spec 20) yices;

After doing this, SAW is leverage Yices to solve the proof goals almost immediately:

[15:22:00.745] Proof succeeded! salsa20/10e438b3::core#1[0]::{impl#0}[0]::apply_keystream[0]::_instfa33e77d840484a0[0]

And with that, we’re finally done! You’ve successfully completed a non-trivial SAW exercise in writing some interesting proofs. Give yourself a well-deserved pat on the back.

The process of developing these proofs was bumpy at times, but that is to be expected. You very rarely get a proof correct on the very first try, and when SAW doesn’t accept your proof, it is important to be able to figure out what went wrong and how to fix it. This is a skill that takes some time to grow, but with enough time and experience, you will be able to recognize common pitfalls. This case study showed off some of these pitfalls, but there are likely others.

Case study: Salsa20

The salsa20 crate

Salsa20 preliminaries

A note about cryptographic security

An overview of the salsa20 code

Building salsa20

Getting started with SAW

Verifying our first salsa20 function

Verifying the rounds function

Verifying the counter_setup function

Verifying the apply_keystream function (first attempt)

Verifying the new_raw function

Verifying the apply_keystream function (second attempt)