HMAC.saw

/* 
 * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 * SPDX-License-Identifier: Apache-2.0
*/

enable_experimental;

// The following lists are used to compute identifiers for digest functions
// and structs. Using parallel lists is the simplest way to do this in SAW.
// The lists below must be kept in sync.
let MDS = ["SHA256", "SHA1", "SHA384", "SHA512", "MD5", "SHA224", "SHA512_256"];
let EVP_MDS = ["EVP_sha256", "EVP_sha1", "EVP_sha384", "EVP_sha512", "EVP_md5", "EVP_sha224", "EVP_sha512_256"];
let MD_INDICES = [0, 1, 2, 3, 4, 5, 6];

let HMAC_MD = (nth MDS HMAC_MD_INDEX);
let HMAC_MD_TRAMPOLINE = (str_concat "AWS_LC_TRAMPOLINE_" HMAC_MD);
let HMAC_MD_INIT = (str_concat HMAC_MD_TRAMPOLINE "_Init");
let HMAC_MD_UPDATE = (str_concat HMAC_MD_TRAMPOLINE "_Update");
let HMAC_MD_FINAL = (str_concat HMAC_MD_TRAMPOLINE "_Final");

let md_storage index = (str_concat (nth EVP_MDS index) "_storage");
let md_once index = (str_concat (nth EVP_MDS index) "_once");
let md_init index = (str_concat (nth EVP_MDS index) "_init");

let HMAC_METHODS = "AWSLC_hmac_in_place_methods";
let HMAC_METHODS_STORAGE = (str_concat HMAC_METHODS "_storage");
let HMAC_METHODS_ONCE = (str_concat HMAC_METHODS "_once");
let HMAC_METHODS_INIT = (str_concat HMAC_METHODS "_init");

// The specs for the globals used with digests and CRYPTO_once
// For the digest that is being verified, this spec states that 
// "storage" global is set correctly after the function returns.
// The init functions are verified, and then we assume a similar
// spec on CRYPTO_once.

// The init function spec states that the function produces the 
// correct struct for the digests used with HMAC. For other digests,
// the spec says nothing about the content of the struct.
let evp_md_methods_init_spec index = do {

  crucible_alloc_global (md_storage index);
  crucible_alloc_global (md_once index);
  
  crucible_execute_func [];

  if (eval_bool {{`index == `HMAC_MD_INDEX}}) then do {
    points_to_env_md_st (crucible_global (md_storage index));
  } else do {
    return ();
  };
};

// This is the spec for the invocation of CRYPTO_once that produces
// the digest structs. It matches the spec of the init function.
let evp_md_methods_spec index = do {
  crucible_alloc_global (md_storage index);
  crucible_alloc_global (md_once index);
  crucible_execute_func
    [ (crucible_global (md_once index))
    , (crucible_global (md_init index))
    ];

  if (eval_bool {{`index == `HMAC_MD_INDEX}}) then do {
    points_to_env_md_st (crucible_global (md_storage index));
  } else do {
    return ();
  };
  
};

// Prove that the init function used to produce each MD struct is correct.
let evp_methods_init_ov index = do { 
  llvm_verify m (md_init index)
    []
    true
    (evp_md_methods_init_spec index)
    (w4_unint_z3 []);
};
for MD_INDICES evp_methods_init_ov;

// Assume that MD struct produced/returned by CRYPTO_once is correct.
let evp_methods_ov index = do { 
  llvm_unsafe_assume_spec
    m
    "CRYPTO_once"
    (evp_md_methods_spec index);
};
evp_methods_ovs <- for MD_INDICES evp_methods_ov;

let points_to_md_methods md ptr md_ptr = do {

  crucible_points_to (crucible_elem ptr 0) md_ptr;

  if md then do {
    crucible_points_to (crucible_elem ptr 1) (crucible_global HMAC_MD_INIT);
    crucible_points_to (crucible_elem ptr 2) (crucible_global HMAC_MD_UPDATE);
    crucible_points_to (crucible_elem ptr 3) (crucible_global HMAC_MD_FINAL);
  } else do {
    return ();
  };
};


let alloc_md_global index = do {
  crucible_alloc_global (md_storage index);
  crucible_alloc_global (md_once index);
};

let alloc_md_globals = do {
  for MD_INDICES alloc_md_global;
};

let alloc_hmac_globals = do {
  crucible_alloc_global HMAC_METHODS_STORAGE;
  crucible_alloc_global HMAC_METHODS_ONCE;
};

let points_to_md_methods_index ptr index = do {
  points_to_md_methods 
    (eval_bool {{`index == `HMAC_MD_INDEX}}) 
    (crucible_elem ptr index) 
    (crucible_global (md_storage index));
};

let points_to_hmac_in_place_methods ptr = do {

  // The global for the digest that is actually used is correct
  points_to_env_md_st (crucible_global (md_storage HMAC_MD_INDEX)); 

  // The evp_md pointers are used as identifiers, and we search through them in order.
  // So we need a spec stating that the pointer values do not equal
  // the value for which we are searching.
  // Because these pointers have separate allocations, they must have different values.

  for MD_INDICES (\x -> points_to_md_methods_index ptr x);
  return ();

};

// The spec of the init function that produces the HMAC in place methods struct
let hmac_in_place_methods_init_spec = do {

  alloc_md_globals;
  alloc_hmac_globals;

  crucible_execute_func [];

  points_to_hmac_in_place_methods (crucible_elem (crucible_global HMAC_METHODS_STORAGE) 0);
};

// The spec for the invocation of CRYPTO_once that produces the HMAC in place
// methods struct. This spec matches the spec for the init function that
// produces this struct.
let hmac_in_place_methods_spec = do {
  alloc_md_globals;
  alloc_hmac_globals;

  crucible_execute_func
    [ (crucible_global HMAC_METHODS_ONCE)
    , (crucible_global HMAC_METHODS_INIT)
    ];
  points_to_hmac_in_place_methods (crucible_elem (crucible_global HMAC_METHODS_STORAGE) 0);
};

// Prove that the init function that produces the HMAC in place methods struct
// is correct.
llvm_verify m HMAC_METHODS_INIT
  evp_methods_ovs
  true
  hmac_in_place_methods_init_spec
  (w4_unint_z3 []);

// Assume that the the HMAC in place methods struct produced/returned by
// CRYPTO_once is correct.
hmac_in_place_methods_ov <- llvm_unsafe_assume_spec
  m
  "CRYPTO_once"
  hmac_in_place_methods_spec;

let global_md_methods = (crucible_elem (crucible_field (crucible_global HMAC_METHODS_STORAGE) "methods") HMAC_MD_INDEX);

let points_to_AWSLC_hmac_in_place_methods md_ptr = do {
  points_to_md_methods true global_md_methods md_ptr;
};

let GetInPlaceMethods_spec = do {

  alloc_md_globals;
  alloc_hmac_globals;

  crucible_execute_func [(crucible_global (md_storage HMAC_MD_INDEX))];

  points_to_hmac_in_place_methods (crucible_elem (crucible_global HMAC_METHODS_STORAGE) 0);

  crucible_return global_md_methods;
};

GetInPlaceMethods_ov <- llvm_verify
  m
  "GetInPlaceMethods"
  [hmac_in_place_methods_ov]
  true
  GetInPlaceMethods_spec
  (w4_unint_z3 []);

// Size of the hmac_ctx_st struct
let HMAC_CTX_SIZE = llvm_sizeof m (llvm_struct "struct.hmac_ctx_st");

// Allocate state structs for `i_ctx`, `o_ctx`, and `md_ctx` fields in an
// `hmac_ctx_st`
let alloc_sha512_state_sts = do {
  i_ctx_ptr <- crucible_alloc (llvm_struct "struct.sha512_state_st");
  o_ctx_ptr <- crucible_alloc (llvm_struct "struct.sha512_state_st");
  md_ctx_ptr <- crucible_alloc (llvm_struct "struct.sha512_state_st");
  return (i_ctx_ptr, o_ctx_ptr, md_ctx_ptr);
};

// Specify that the fields of an `hmac_ctx_st` are null
let zeroed_hmac_ctx_st ptr = do {
  crucible_points_to (crucible_field ptr "md") crucible_null;
  crucible_points_to (crucible_field ptr "methods") crucible_null;

  crucible_points_to (crucible_field ptr "state") (crucible_term {{0:[8]}});
};

// Specify the relation between hmac_ctx_st and HMACState
let points_to_hmac_ctx_st ptr context num = do {
  // Check that `i_ctx`, `o_ctx`, and `md_ctx` match the spec.  We set the
  // `num` argument for `i_ctx` and `o_ctx` to 0 because HMAC_Init_ex pads or
  // hashes the key to make it exactly 128 bytes, so the `block` field of these
  // structs is uninitialized by the digest update function.  No other function
  // modifies `i_ctx` or `o_ctx`.

  let i_ctx_ptr = llvm_cast_pointer (llvm_field ptr "i_ctx") (llvm_alias "struct.sha512_state_st");
  let o_ctx_ptr = llvm_cast_pointer (llvm_field ptr "o_ctx") (llvm_alias "struct.sha512_state_st");
  let md_ctx_ptr = llvm_cast_pointer (llvm_field ptr "md_ctx") (llvm_alias "struct.sha512_state_st");

  points_to_sha512_state_st i_ctx_ptr {{ context.i_ctx }} 0;
  points_to_sha512_state_st o_ctx_ptr {{ context.o_ctx }} 0;
  points_to_sha512_state_st md_ctx_ptr {{ context.md_ctx }} num;

  // Specify that `ptr.md` points to the correct global MD struct
  crucible_points_to (crucible_field ptr "md") (crucible_global (md_storage HMAC_MD_INDEX));

  // Methods struct is correct
  crucible_alloc_global HMAC_METHODS_STORAGE;
  points_to_AWSLC_hmac_in_place_methods (crucible_global (md_storage HMAC_MD_INDEX));
  crucible_points_to (crucible_field ptr "methods") global_md_methods;

};

// Create a Cryptol HMACState
let fresh_hmac_state_st name num = do {
  // Create Cryptol SHAStates.  We set `n` to 0 for `i_ctx` and `o_ctx`
  // because the init function always sets `n` to 0.
  i_ctx <- fresh_sha512_state_st (str_concat name ".i_ctx") 0;
  o_ctx <- fresh_sha512_state_st (str_concat name ".o_ctx") 0;
  md_ctx <- fresh_sha512_state_st (str_concat name ".md_ctx") num;

  // Build the HMACState record
  return {{ { i_ctx = i_ctx, o_ctx = o_ctx, md_ctx = md_ctx } }};
};

// Specification of the HMAC_CTX_init function
let HMAC_CTX_init_spec = do {
  // Precondition: `hmac_ctx_ptr` points to an `hmac_ctx_st` struct
  hmac_ctx_ptr <- crucible_alloc (llvm_struct "struct.hmac_ctx_st");

  // Call function with `hmac_ctx_ptr`
  crucible_execute_func [hmac_ctx_ptr];

  // Postcondition: The struct pointed to by `hmac_ctx_ptr` has been zeroed out
  zeroed_hmac_ctx_st hmac_ctx_ptr;
};

// Specification of the HMAC_Init_ex function
let HMAC_Init_ex_spec key_len = do {
  // Precondition: The function uses the AVX+shrd code path
  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};

  // Precondition: The digest and hmac globals are allocated
  alloc_md_globals;
  alloc_hmac_globals;

  // Precondition: `hmac_ctx_ptr` points to a zeroed out `hmac_ctx_st`
  hmac_ctx_ptr <- crucible_alloc (llvm_struct "struct.hmac_ctx_st");
  zeroed_hmac_ctx_st hmac_ctx_ptr;

  // Precondition: `key` is an array of `key_len` bytes.  `key_ptr` points to
  // `key`.
  (key, key_ptr) <- ptr_to_fresh_readonly "key" (llvm_array key_len (llvm_int 8));

  // Precondition: the global digest struct holds the correct values
  points_to_env_md_st (crucible_global (md_storage HMAC_MD_INDEX));

  // Call function with `hmac_ctx_ptr`, `key_ptr`, `key_len`, the global digest struct pointer, and NULL
  crucible_execute_func
    [ hmac_ctx_ptr
    , key_ptr
    , crucible_term {{ `key_len : [64] }}
    , (crucible_global (md_storage HMAC_MD_INDEX))
    , crucible_null
    ];

  // Postcondition: The function has not changed the variable that decides the
  // AVX+shrd code path
  global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};

  // Postcondition: The data pointed to by `hmac_ctx_ptr` matches the context
  // returned by the cryptol function `HMACInit` when applied to `key`.
  points_to_hmac_ctx_st hmac_ctx_ptr {{ HMACInit key }} 0;

  // Postcondition: The function returns 1
  crucible_return (crucible_term {{ 1 : [32] }});
};

let hmac_ctx_is_initialized ptr = do {
  state <- crucible_fresh_var "state" (llvm_int 8);
  crucible_precond {{state == 1 \/ state == 2}};
  crucible_points_to (crucible_field ptr "state") (crucible_term state);

};

// Specification of the HMAC_Update function
let HMAC_Update_spec num len = do {
  // Precondition: The function uses the AVX+shrd code path
  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};

  // Precondition: The global digest struct is allocated and holds the correct values
  alloc_md_globals;
  points_to_env_md_st (crucible_global (md_storage HMAC_MD_INDEX));

  // Precondition: `hmac_ctx_ptr` is a pointer to an `hmac_ctx_st`
  hmac_ctx_ptr <- crucible_alloc (llvm_struct "struct.hmac_ctx_st");
  // Precondition: `hmac_ctx` is a fresh Cryptol HMACState
  hmac_ctx <- fresh_hmac_state_st "hmac_ctx" num;
  // Precondition: `hmac_ctx_ptr` matches `hmac_ctx`
  points_to_hmac_ctx_st hmac_ctx_ptr hmac_ctx num;

  // Precondition: state must be initialized
  hmac_ctx_is_initialized hmac_ctx_ptr;

  // Precondition: `data` is an array of `len` bytes.  `data_ptr` points
  // to `data`.
  (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array len (llvm_int 8));

  // Call function with `hmac_ctx_ptr`, `data_ptr`, and `len`
  crucible_execute_func [ hmac_ctx_ptr , data_ptr , crucible_term {{ `len : [64] }} ];

  // Postcondition: The function has not changed the variable that decides the
  // AVX+shrd code path
  global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};

  // Postcondition: The data pointed to by `hmac_ctx_ptr` matches the context
  // returned by the cryptol function `HMACInit` when applied to `hmac_ctx` and
  // `data`.
  points_to_hmac_ctx_st hmac_ctx_ptr {{ HMACUpdate hmac_ctx data }} (eval_size {| (num + len) % SHA512_CBLOCK |});

  // Postcondition: The function returns 1
  crucible_return (crucible_term {{ 1 : [32] }});
};

// Specification of the HMAC_Final function
let HMAC_Final_spec withLength num = do {
  // Precondition: The function uses the AVX+shrd code path
  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};

  // Precondition: The global digest struct is allocated and holds the correct values
  alloc_md_globals;
  points_to_env_md_st (crucible_global (md_storage HMAC_MD_INDEX));

  // Precondition: `hmac_ctx_ptr` is a pointer to an `hmac_ctx_st`
  hmac_ctx_ptr <- crucible_alloc (llvm_struct "struct.hmac_ctx_st");
  // Precondition: `hmac_ctx` is a fresh Cryptol HMACState
  hmac_ctx <- fresh_hmac_state_st "hmac_ctx" num;
  // Precondition: `hmac_ctx_ptr` matches `hmac_ctx`
  points_to_hmac_ctx_st hmac_ctx_ptr hmac_ctx num;
  // Precondition: state must be initialized
  hmac_ctx_is_initialized hmac_ctx_ptr;


  // Precondition: out_ptr is allocated and correct length, and 
  // out_len_ptr is null or points to an int.
  (out_ptr, out_len_ptr) <- digestOut_pre withLength;

  // Call function with `hmac_ctx_ptr`, `out_ptr`, and `out_len_ptr`
  crucible_execute_func [ hmac_ctx_ptr , out_ptr , out_len_ptr ];

  // Postcondition: The function has not changed the variable that decides the
  // AVX+shrd code path
  global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};

  // Postcondition: The contents of the array pointed to by `out_ptr` match the
  // result returned by the HMACFinal cryptol spec.
  // If length output is used, out_len_ptr points to correct length.
  digestOut_post withLength out_ptr out_len_ptr (crucible_term {{ HMACFinal hmac_ctx }});

  // Postcondition: The function returns 1
  crucible_return (crucible_term {{ 1 : [32] }});
};

// Specification of the HMAC function
let HMAC_spec withLength key_len data_len = do {
  // Precondition: The function uses the AVX+shrd code path
  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};

  // Precondition: The digest globals and global hmac methods storage are allocated
  alloc_md_globals;
  alloc_hmac_globals;

  // Precondition: The global digest struct holds the corerct values
  points_to_env_md_st (crucible_global (md_storage HMAC_MD_INDEX));

  // Precondition: `key` is a fresh const array of `key_len` bytes, and
  // `key_ptr` points to `key`
  (key, key_ptr) <- ptr_to_fresh_readonly "key" (llvm_array key_len i8);

  // Precondition: `data` is a fresh const array of `data_len` bytes, and
  // `data_ptr` points to `data`.
  (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array data_len i8);

  // Precondition: md_out_ptr is allocated and correct length, and 
  // md_out_len_ptr is null or points to an int.
  (md_out_ptr, md_out_len_ptr) <- digestOut_pre withLength;

  // Call function with arguments the global digest struct pointer, `key_ptr`, `key_len`, 
  // `data_ptr`, `data_len`, `md_out_ptr`, and `md_out_len_ptr`
  crucible_execute_func
    [ (crucible_global (md_storage HMAC_MD_INDEX))
    , key_ptr
    , crucible_term {{ `key_len : [64] }}
    , data_ptr
    , crucible_term {{ `data_len : [64] }}
    , md_out_ptr
    , md_out_len_ptr
    ];

  // Postcondition: The function has not changed the variable that decides the AVX+shrd code path
  global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};

  // Postcondition: The contents of the array pointed to by `md_out_ptr` match
  // the result returned by the HMACFinal cryptol spec.
  // If length output is used, md_out_len_ptr points to correct length
  digestOut_post withLength md_out_ptr md_out_len_ptr (crucible_term {{ HMAC key data }});
  
  // Postcondition: The function returns `md_out_ptr`
  crucible_return md_out_ptr;
};


// Verify the `HMAC_CTX_init` C function satisfies the `HMAC_CTX_init_spec`
// specification
crucible_llvm_verify m "HMAC_CTX_init"
  []
  true
  HMAC_CTX_init_spec
  (w4_unint_yices []);

let verify_HMAC_Init_ex_spec key_len = do {
  print (str_concat "Verifying HMAC_Init_ex_spec at key_len=" (show key_len));
  crucible_llvm_verify m "HMAC_Init_ex"
    [ sha512_block_data_order_ov
    , OPENSSL_malloc_ov
    , OPENSSL_free_nonnull_ov
    , OPENSSL_free_null_ov
    , OPENSSL_cleanse_ov
    , GetInPlaceMethods_ov
    ]
    true
    (HMAC_Init_ex_spec key_len)
    (w4_unint_yices []);
};

// Verify the `HMAC_Init_ex` C function satisfies the `HMAC_Init_ex_spec` specification.  
// There are two cases to consider.
// Case 1: key_len=128 covers the case where the key is less than or equal to 128
// bytes long and will be used as-is when XORed to create the pad inputs to
// the SHA384 update function calls
// Case 2: key_len=129 covers the case where the key is greater than 128 bytes long
// and will be hashed before being XORed to create the pad inputs to the
// SHA384 update function calls
for [128, 129] verify_HMAC_Init_ex_spec;

// Verify the `HMAC_Update` C function satisfies the `HMAC_Update_spec`
// specification.  There are 3 cases to consider to ensure the proof covers all
// possible code paths through the update function.
// Input length and buffer position are not exercised exhaustively, because this
// is done in the proof of the underlying hash function.
crucible_llvm_verify m "HMAC_Update"
  [ sha512_block_data_order_ov
  , OPENSSL_malloc_ov
  , OPENSSL_free_nonnull_ov
  , OPENSSL_free_null_ov
  , OPENSSL_cleanse_ov
  ]
  true
  // num=0, len=240 covers the case with one call to the block function, on one
  // block from data, and the rest of data copied in hmac_ctx->md_ctx->data
  (HMAC_Update_spec 0 240)
  (w4_unint_yices ["processBlock_Common"]);
crucible_llvm_verify m "HMAC_Update"
  [ sha512_block_data_order_ov
  , OPENSSL_malloc_ov
  , OPENSSL_free_nonnull_ov
  , OPENSSL_free_null_ov
  , OPENSSL_cleanse_ov
  ]
  true
  // num=0, len=127 covers the case without any calls to the block function,
  // and data copied in ctx->md_ctx->data
  (HMAC_Update_spec 0 127)
  (w4_unint_yices ["processBlock_Common"]);
crucible_llvm_verify m "HMAC_Update"
  [sha512_block_data_order_ov]
  true
  // num=127, len=241 covers the case with two calls to the block function,
  // the first one on ctx->md_ctx->data, the second one on one block from data,
  // and the rest of data copied in ctx->md_ctx->data
  (HMAC_Update_spec 127 241)
  (w4_unint_yices ["processBlock_Common"]);

// Verify the `HMAC_Final` C function satisfies the `HMAC_Final_spec`
// specification.
let HMAC_Final_ovs =
  [ sha512_block_data_order_ov
  , OPENSSL_malloc_ov
  , OPENSSL_free_nonnull_ov
  , OPENSSL_free_null_ov
  , OPENSSL_cleanse_ov
  ];

let verify_HMAC_Final_spec withLength num = do {
  print (str_concat "Verifying HMAC_Final_spec at num=" (show num));
  crucible_llvm_verify m "HMAC_Final"
    HMAC_Final_ovs
    true
    (HMAC_Final_spec withLength num)
    (w4_unint_yices ["processBlock_Common"]);
};

let verify_final_with_length withLength = do {
  // There are 2 cases to consider to ensure the proof covers all possible code
  // paths through the update function
  // Case 1: num=111 covers the case with one call to the block function
  (verify_HMAC_Final_spec withLength 111);
  // Case 2: num=112 covers the case with two calls to the block function
  (verify_HMAC_Final_spec withLength 112);
};

let verify_final_with_num target_num = do {
  (verify_HMAC_Final_spec false target_num);
  (verify_HMAC_Final_spec true target_num);
};

// Checking all buffer positions does not take that long, so this is done
// in select check, even though similar checks are done when verifying the
// underlying hash function.
if HMAC_quick_check then do {
  for [false, true] verify_final_with_length;
  return();
} else do {
  // range of valid indices in the internal block ([0 .. (SHA512_CBLOCK - 1)])
  nums <- for (eval_list {{ [0 .. (SHA512_CBLOCK - 1)] : [SHA512_CBLOCK][64] }})
    (\x -> (return (eval_int x)) : (TopLevel Int));
  for nums verify_final_with_num;
  return();
};

let verify_hmac_with_length withLength = do {
  // Verify the `HMAC` C function satisfies the `HMAC_spec` specification
  crucible_llvm_verify m "HMAC"
    [ sha512_block_data_order_ov
    , OPENSSL_malloc_ov
    , OPENSSL_free_nonnull_ov
    , OPENSSL_free_null_ov
    , OPENSSL_cleanse_ov
    , GetInPlaceMethods_ov
    ]
    true
    (HMAC_spec withLength 240 240)
    (w4_unint_yices ["processBlock_Common"]);
};
for [false, true] verify_hmac_with_length;