Proof Maintenance Exercises: Solutions

This section provides a detailed solution to the two exercises in Proof Maintenance Exercises: s2n HMAC.

Updating the Cryptol Specification

The Cryptol type corresponding to the updated state container must, like the C structure, be augmented with an outer_just_key field that has the appropriate type, like so:

type HMAC_c_state =
  { alg                     : [32]
  , hash_block_size         : [16]
  , currently_in_hash_block : [32]
  , block_size              : [16]
  , digest_size             : [8]
  , inner                   : SHA512_c_state
  , inner_just_key          : SHA512_c_state
  , outer                   : SHA512_c_state
  , outer_just_key          : SHA512_c_state
  , xor_pad                 : [128][8]
  , digest_pad              : [SHA512_DIGEST_LENGTH][8]
  }

This very clearly corresponds to the change to the s2n_hmac_state structure in the C implementation, other than the specialization to SHA512. In the C implementation, the code is abstracted over the chosen hashing algorithm.

Here is a sample of how the functions that use the HMAC_c_state type must change:

hmac_init_c_state :
     { key_size, block_size, hash_block_size, digest_size }
     ( fin key_size
     , 64 >= width (8*key_size)
     , 16 >= width hash_block_size
     , 16 >= width block_size
     , 8 >= width digest_size
     , 128 >= block_size
     , 64 >= digest_size )
  => HMAC_c_state
  -> [32]
  -> [key_size][8]
  -> HMAC_c_state
hmac_init_c_state st0 alg key =
  { alg                     = alg
  , hash_block_size         = `hash_block_size
  , currently_in_hash_block = currently_in_hash_block
  , block_size              = `block_size
  , digest_size             = `digest_size

  , inner                   = inner
  , inner_just_key          = inner_just_key
  , outer                   = outer
  , outer_just_key          = outer_just_key
  , xor_pad                 = xor_pad
  , digest_pad              = digest_pad
  }
  where
    currently_in_hash_block = 0

    k0 : [block_size][8]
    (outer, digest_pad, k0) =
      key_init_c_state `{digest_size=digest_size} st0.outer st0.digest_pad key
    ikey = [ k ^ 0x36 | k <- k0 ]
    okey = [ k ^ 0x6a | k <- ikey ]

    inner_just_key = hash_update_c_state
      (hash_init_c_state st0.inner_just_key) ikey
    inner          = inner_just_key
    outer_just_key = hash_update_c_state
      (hash_init_c_state st0.outer_just_key) okey
    xor_pad = zero //okey # drop st0.xor_pad

Take note of how similar these changes are to those in the analogous C code; this is true more generally, as can be seen in the complete diff between HMAC_iterative_old.cry and HMAC_iterative_new.cry:

--- /Users/atomb/galois/saw-training/downloads/examples/hmac/HMAC_iterative_old.cry
+++ /Users/atomb/galois/saw-training/downloads/examples/hmac/HMAC_iterative_new.cry
@@ -81,6 +81,7 @@
   , inner                   : SHA512_c_state
   , inner_just_key          : SHA512_c_state
   , outer                   : SHA512_c_state
+  , outer_just_key          : SHA512_c_state
   , xor_pad                 : [128][8]
   , digest_pad              : [SHA512_DIGEST_LENGTH][8]
   }
@@ -193,7 +194,7 @@
   , inner                   = inner
   , inner_just_key          = inner_just_key
   , outer                   = outer
-
+  , outer_just_key          = outer_just_key
   , xor_pad                 = xor_pad
   , digest_pad              = digest_pad
   }
@@ -209,8 +210,9 @@
     inner_just_key = hash_update_c_state
       (hash_init_c_state st0.inner_just_key) ikey
     inner          = inner_just_key
-
-    xor_pad = okey # drop st0.xor_pad
+    outer_just_key = hash_update_c_state
+      (hash_init_c_state st0.outer_just_key) okey
+    xor_pad = zero //okey # drop st0.xor_pad
 
 
 hmac_update_c_state : {msg_size} (32 >= width msg_size) =>
@@ -228,6 +230,7 @@
   , digest_size     = s.digest_size
   , inner_just_key  = s.inner_just_key
   , outer           = s.outer
+  , outer_just_key  = s.outer_just_key
   , xor_pad         = s.xor_pad
   , digest_pad      = s.digest_pad
   }
@@ -277,9 +280,7 @@
     //outer = SHA256Update SHA256Init (okey # hin)
     //
     // with:
-    outer = hash_update_c_state
-      (hash_update_c_state (hash_init_c_state s.outer) okey)
-      hin
+    outer = hash_update_c_state s.outer_just_key hin
     inner = s.inner
 
     out = join (hash_digest_c_state outer)
@@ -287,7 +288,7 @@
     sout : HMAC_c_state
     sout =
       { inner      = inner
-      , outer      = outer
+      , outer      = s.outer_just_key
       , digest_pad = digest_pad
 
       // Rest unchanged.

Updating the SAW Specifications

Using the hint given in the exercise, a search for the term “outer” in HMAC_old.saw reveals not only where memory layouts are specified, but embedded Cryptol terms of the type adjusted in the previous section. One of the memory layout specifications found through this search looks like this:

    // ...
    crucible_points_to (crucible_elem pstate 0) (crucible_term alg0);
    crucible_points_to (crucible_elem pstate 1) (crucible_term hash_block_size0);
    crucible_points_to (crucible_elem pstate 2) (crucible_term currently_in_hash_block0);
    crucible_points_to (crucible_elem pstate 3) (crucible_term block_size0);
    crucible_points_to (crucible_elem pstate 4) (crucible_term digest_size0);
    inner0 <- setup_hash_state (crucible_elem pstate 5);
    inner_just_key0 <- setup_hash_state (crucible_elem pstate 6);
    outer0 <- setup_hash_state (crucible_elem pstate 7);
    crucible_points_to (crucible_elem pstate 8) (crucible_term xor_pad0);
    crucible_points_to (crucible_elem pstate 9) (crucible_term digest_pad0);
    // ...

Another improvement that can be made to this code is to use the crucible_field primitive instead of crucible_elem, which allows reference to structure fields by name rather than by index. This, and the necessary change to memory layout, appear below.

    // ...
    crucible_points_to (crucible_field pstate "alg") (crucible_term alg0);
    crucible_points_to (crucible_field pstate "hash_block_size") (crucible_term hash_block_size0);
    crucible_points_to (crucible_field pstate "currently_in_hash_block") (crucible_term currently_in_hash_block0);
    crucible_points_to (crucible_field pstate "xor_pad_size") (crucible_term block_size0);
    crucible_points_to (crucible_field pstate "digest_size") (crucible_term digest_size0);
    inner0 <- setup_hash_state (crucible_field pstate "inner");
    inner_just_key0 <- setup_hash_state (crucible_field pstate "inner_just_key");
    outer_just_key0 <- setup_hash_state (crucible_field pstate "outer_just_key");
    outer0 <- setup_hash_state (crucible_field pstate "outer");
    crucible_points_to (crucible_field pstate "xor_pad") (crucible_term xor_pad0);
    crucible_points_to (crucible_field pstate "digest_pad") (crucible_term digest_pad0);
    // ...

The other change necessary is the aforementioned update to embedded Cryptol terms using the HMAC_c_state type augmented in the previous section. The original code found by searching looks like this:

    // ...
    let st0 = {{
        { alg                     = alg0
        , hash_block_size         = hash_block_size0
        , currently_in_hash_block = currently_in_hash_block0
        , block_size              = block_size0
        , digest_size             = digest_size0
        , inner                   = inner0
        , inner_just_key          = inner_just_key0
        , outer                   = outer0
        , xor_pad                 = xor_pad0
        , digest_pad              = digest_pad0
        }
      }};
    // ...

And the update corresponds exactly to the one in the Cryptol specification:

    // ...
    let st0 = {{
        { alg                     = alg0
        , hash_block_size         = hash_block_size0
        , currently_in_hash_block = currently_in_hash_block0
        , block_size              = block_size0
        , digest_size             = digest_size0
        , inner                   = inner0
        , inner_just_key          = inner_just_key0
        , outer                   = outer0
        , outer_just_key          = outer_just_key0
        , xor_pad                 = xor_pad0
        , digest_pad              = digest_pad0
        }
      }};
    // ...

The complete set of changes to the SAW specification can be seen in the diff between HMAC_old.saw and HMAC_new.saw:

--- /Users/atomb/galois/saw-training/downloads/examples/hmac/HMAC_old.saw
+++ /Users/atomb/galois/saw-training/downloads/examples/hmac/HMAC_new.saw
@@ -3,7 +3,7 @@
 //
 // Authors:
 //      Aaron Tomb : atomb@galois.com
-//  Nathan Collins : conathan@galois.com
+//	Nathan Collins : conathan@galois.com
 //      Joey Dodds : jdodds@galois.com
 //
 // Licensed under the Apache License, Version 2.0 (the "License").
@@ -19,7 +19,7 @@
 //
 ////////////////////////////////////////////////////////////////
 
-import "HMAC_iterative_old.cry";
+import "HMAC_iterative_new.cry";
 import "Hashing.cry";
 
 ////////////////////////////////////////////////////////////////
@@ -162,16 +162,17 @@
     digest_pad0 <- crucible_fresh_var "digest_pad" (llvm_array digest_size (llvm_int 8));
 
     // ...
-    crucible_points_to (crucible_elem pstate 0) (crucible_term alg0);
-    crucible_points_to (crucible_elem pstate 1) (crucible_term hash_block_size0);
-    crucible_points_to (crucible_elem pstate 2) (crucible_term currently_in_hash_block0);
-    crucible_points_to (crucible_elem pstate 3) (crucible_term block_size0);
-    crucible_points_to (crucible_elem pstate 4) (crucible_term digest_size0);
-    inner0 <- setup_hash_state (crucible_elem pstate 5);
-    inner_just_key0 <- setup_hash_state (crucible_elem pstate 6);
-    outer0 <- setup_hash_state (crucible_elem pstate 7);
-    crucible_points_to (crucible_elem pstate 8) (crucible_term xor_pad0);
-    crucible_points_to (crucible_elem pstate 9) (crucible_term digest_pad0);
+    crucible_points_to (crucible_field pstate "alg") (crucible_term alg0);
+    crucible_points_to (crucible_field pstate "hash_block_size") (crucible_term hash_block_size0);
+    crucible_points_to (crucible_field pstate "currently_in_hash_block") (crucible_term currently_in_hash_block0);
+    crucible_points_to (crucible_field pstate "xor_pad_size") (crucible_term block_size0);
+    crucible_points_to (crucible_field pstate "digest_size") (crucible_term digest_size0);
+    inner0 <- setup_hash_state (crucible_field pstate "inner");
+    inner_just_key0 <- setup_hash_state (crucible_field pstate "inner_just_key");
+    outer_just_key0 <- setup_hash_state (crucible_field pstate "outer_just_key");
+    outer0 <- setup_hash_state (crucible_field pstate "outer");
+    crucible_points_to (crucible_field pstate "xor_pad") (crucible_term xor_pad0);
+    crucible_points_to (crucible_field pstate "digest_pad") (crucible_term digest_pad0);
     // ...
 
     // ...
@@ -184,6 +185,7 @@
         , inner                   = inner0
         , inner_just_key          = inner_just_key0
         , outer                   = outer0
+        , outer_just_key          = outer_just_key0
         , xor_pad                 = xor_pad0
         , digest_pad              = digest_pad0
         }
@@ -193,19 +195,20 @@
 };
 
 let check_hmac_state pstate st = do {
-    crucible_points_to (crucible_elem pstate 0) (crucible_term {{ st.alg }});
-    crucible_points_to (crucible_elem pstate 1) (crucible_term {{ st.hash_block_size }});
-    crucible_points_to (crucible_elem pstate 2) (crucible_term {{ st.currently_in_hash_block }});
-    crucible_points_to (crucible_elem pstate 3) (crucible_term {{ st.block_size }});
-    crucible_points_to (crucible_elem pstate 4) (crucible_term {{ st.digest_size }});
-    update_hash_state (crucible_elem pstate 5) {{ st.inner }};
-    update_hash_state (crucible_elem pstate 6) {{ st.inner_just_key }};
+    crucible_points_to (crucible_field pstate "alg") (crucible_term {{ st.alg }});
+    crucible_points_to (crucible_field pstate "hash_block_size") (crucible_term {{ st.hash_block_size }});
+    crucible_points_to (crucible_field pstate "currently_in_hash_block") (crucible_term {{ st.currently_in_hash_block }});
+    crucible_points_to (crucible_field pstate "xor_pad_size") (crucible_term {{ st.block_size }});
+    crucible_points_to (crucible_field pstate "digest_size") (crucible_term {{ st.digest_size }});
+    update_hash_state (crucible_field pstate "inner") {{ st.inner }};
+    update_hash_state (crucible_field pstate "inner_just_key") {{ st.inner_just_key }};
 
     // XXX: Don't care about 'outer' because it gets overwritten by
     // 's2n_hash_reset' before use in 's2n_hmac_digest'.
     //
     //update_hash_state (crucible_elem pstate 7) {{ st.outer }};
-    crucible_points_to (crucible_elem pstate 8) (crucible_term {{ st.xor_pad }});
+    update_hash_state (crucible_field pstate "outer_just_key") ({{ st.outer_just_key }});
+    crucible_points_to (crucible_field pstate "xor_pad") (crucible_term {{ st.xor_pad }});
 
     // Don't care about 'digest_pad', because it gets overwritten
     // using 's2n_hash_digest' before use in 's2n_hmac_digest'.

With this, the specifications have been updated to account for the changes to the implementation, and verification via SAW will go through as intended.