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;
uint16_t xor_pad_size;
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 */
uint8_t xor_pad[128];
/* For storing the inner digest */
uint8_t digest_pad[SHA512_DIGEST_LENGTH];
};
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;
if (klen > state->xor_pad_size) {
GUARD(s2n_hash_update(&state->outer, key, klen));
GUARD(s2n_hash_digest(&state->outer, state->digest_pad, state->digest_size));
memcpy_check(state->xor_pad, state->digest_pad, state->digest_size);
copied = state->digest_size;
} else {
memcpy_check(state->xor_pad, key, klen);
}
for (int i = 0; i < copied; i++) {
state->xor_pad[i] ^= 0x36;
}
for (int i = copied; i < state->xor_pad_size; i++) {
state->xor_pad[i] = 0x36;
}
GUARD(s2n_hash_update(&state->inner_just_key, state->xor_pad, state->xor_pad_size));
/* 0x36 xor 0x5c == 0x6a */
for (int i = 0; i < state->xor_pad_size; i++) {
state->xor_pad[i] ^= 0x6a;
}
GUARD(s2n_hash_update(&state->outer_just_key, state->xor_pad, state->xor_pad_size));
memset(&state->xor_pad, 0, sizeof(state->xor_pad));
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
+++ /Users/atomb/galois/saw-training/downloads/examples/hmac/s2n_hmac_new.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++) {
state->xor_pad[i] = 0x36;
}
- GUARD(s2n_hash_init(&state->inner_just_key, hash_alg));
GUARD(s2n_hash_update(&state->inner_just_key, key, klen));
GUARD(s2n_hash_update(&state->inner_just_key, state->xor_pad, state->xor_pad_size));
@@ -106,9 +110,9 @@
state->xor_pad[i] = 0x5c;
}
- GUARD(s2n_hash_init(&state->outer, hash_alg));
GUARD(s2n_hash_update(&state->outer, key, klen));
GUARD(s2n_hash_update(&state->outer, state->xor_pad, state->xor_pad_size));
+ memset(&state->xor_pad, 0, sizeof(state->xor_pad));
/* 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;
if (klen > state->xor_pad_size) {
@@ -156,6 +161,9 @@
for (int i = 0; i < state->xor_pad_size; i++) {
state->xor_pad[i] ^= 0x6a;
}
+
+ GUARD(s2n_hash_update(&state->outer_just_key, state->xor_pad, state->xor_pad_size));
+ memset(&state->xor_pad, 0, sizeof(state->xor_pad));
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_digest(&state->inner, state->digest_pad, state->digest_size));
- GUARD(s2n_hash_reset(&state->outer));
- GUARD(s2n_hash_update(&state->outer, state->xor_pad, state->xor_pad_size));
+ GUARD(s2n_hash_copy(&state->outer, &state->outer_just_key));
GUARD(s2n_hash_update(&state->outer, state->digest_pad, state->digest_size));
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));
+
memcpy_check(to->xor_pad, from->xor_pad, sizeof(to->xor_pad));
memcpy_check(to->digest_pad, from->digest_pad, sizeof(to->digest_pad));
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.