# Proof Maintenance Exercises: s2n HMAC¶

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

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

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

## Background: The Updates to the Implementation¶

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

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

struct s2n_hmac_state {
s2n_hmac_algorithm alg;

uint16_t hash_block_size;
uint32_t currently_in_hash_block;
uint8_t digest_size;

struct s2n_hash_state inner;
struct s2n_hash_state inner_just_key;
struct s2n_hash_state outer;
struct s2n_hash_state outer_just_key;

/* key needs to be as large as the biggest block size */

/* For storing the inner digest */
};


The addition of this new field saw corresponding changes to the implementation code, which can be found in s2n_hmac_new.c. These changes included memory allocations, initializations, updates, and frees. The following code sample gives a good sense of the types of changes involved:

static int s2n_tls_hmac_init(struct s2n_hmac_state *state, s2n_hmac_algorithm alg, const void *key, uint32_t klen)
{
s2n_hash_algorithm hash_alg;
GUARD(s2n_hmac_hash_alg(alg, &hash_alg));

GUARD(s2n_hash_init(&state->inner, hash_alg));
GUARD(s2n_hash_init(&state->inner_just_key, hash_alg));
GUARD(s2n_hash_init(&state->outer, hash_alg));
GUARD(s2n_hash_init(&state->outer_just_key, hash_alg));

uint32_t copied = klen;
GUARD(s2n_hash_update(&state->outer, key, klen));

copied = state->digest_size;
} else {
}

for (int i = 0; i < copied; i++) {
}
for (int i = copied; i < state->xor_pad_size; i++) {
}

/* 0x36 xor 0x5c == 0x6a */
for (int i = 0; i < state->xor_pad_size; i++) {
}

return s2n_hmac_reset(state);
}


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

--- /Users/atomb/galois/saw-training/downloads/examples/hmac/s2n_hmac_old.c
@@ -18,7 +18,7 @@

#include "s2n_errno.h"

-#include "s2n_hmac_old.h"
+#include "s2n_hmac_new.h"
#include "s2n_hash.h"
#include "s2n_fips.h"

@@ -94,11 +94,15 @@
hash_alg = S2N_HASH_SHA1;
}

+    GUARD(s2n_hash_init(&state->inner, hash_alg));
+    GUARD(s2n_hash_init(&state->inner_just_key, hash_alg));
+    GUARD(s2n_hash_init(&state->outer, hash_alg));
+    GUARD(s2n_hash_init(&state->outer_just_key, hash_alg));
+
for (int i = 0; i < state->xor_pad_size; i++) {
}

-    GUARD(s2n_hash_init(&state->inner_just_key, hash_alg));
GUARD(s2n_hash_update(&state->inner_just_key, key, klen));

@@ -106,9 +110,9 @@
}

-    GUARD(s2n_hash_init(&state->outer, hash_alg));
GUARD(s2n_hash_update(&state->outer, key, klen));

/* Copy inner_just_key to inner */
return s2n_hmac_reset(state);
@@ -123,14 +127,15 @@
return s2n_hash_digest(&state->inner, out, size);
}

-
static int s2n_tls_hmac_init(struct s2n_hmac_state *state, s2n_hmac_algorithm alg, const void *key, uint32_t klen)
{
s2n_hash_algorithm hash_alg;
GUARD(s2n_hmac_hash_alg(alg, &hash_alg));

+    GUARD(s2n_hash_init(&state->inner, hash_alg));
GUARD(s2n_hash_init(&state->inner_just_key, hash_alg));
GUARD(s2n_hash_init(&state->outer, hash_alg));
+    GUARD(s2n_hash_init(&state->outer_just_key, hash_alg));

uint32_t copied = klen;
@@ -156,6 +161,9 @@
for (int i = 0; i < state->xor_pad_size; i++) {
}
+

return s2n_hmac_reset(state);
}
@@ -201,6 +209,7 @@
GUARD(s2n_hash_new(&state->inner));
GUARD(s2n_hash_new(&state->inner_just_key));
GUARD(s2n_hash_new(&state->outer));
+    GUARD(s2n_hash_new(&state->outer_just_key));

return 0;
}
@@ -269,8 +278,7 @@
}

-    GUARD(s2n_hash_reset(&state->outer));
+    GUARD(s2n_hash_copy(&state->outer, &state->outer_just_key));

return s2n_hash_digest(&state->outer, out, size);
@@ -303,6 +311,7 @@
GUARD(s2n_hash_free(&state->inner));
GUARD(s2n_hash_free(&state->inner_just_key));
GUARD(s2n_hash_free(&state->outer));
+    GUARD(s2n_hash_free(&state->outer_just_key));

return 0;
}
@@ -333,6 +342,8 @@
GUARD(s2n_hash_copy(&to->inner, &from->inner));
GUARD(s2n_hash_copy(&to->inner_just_key, &from->inner_just_key));
GUARD(s2n_hash_copy(&to->outer, &from->outer));
+    GUARD(s2n_hash_copy(&to->outer_just_key, &from->outer_just_key));
+



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

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

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

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

Take note of the similarities to the rotr3 example in Exercise: Swapping and Rotating; these kinds of update are ubiquitous when working on proof maintenance tasks. It will help to review that section before completing these exercises.

## Exercise: Update the Cryptol Specification¶

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

Your task is to perform these updates in HMAC_iterative_old.cry. Use the bullet points above as a rough guide, and if you get stuck, there is a complete solution presented on the next page.

## Exercise: Update the SAW Specifications¶

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

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

Note

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

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