evp-function-specs.saw

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


let EVP_DigestSignVerifyInit_spec is_sign = do {
  crucible_alloc_global "EVP_MD_pctx_ops_storage";
  crucible_alloc_global "EVP_MD_pctx_ops_once";
  crucible_alloc_global "EVP_PKEY_rsa_pkey_meth_storage";
  crucible_alloc_global "EVP_PKEY_rsa_pss_pkey_meth_storage";
  crucible_alloc_global "EVP_PKEY_ec_pkey_meth_storage";
  crucible_alloc_global "EVP_PKEY_hkdf_pkey_meth_storage";
  crucible_alloc_global "EVP_PKEY_hmac_pkey_meth_storage";
  crucible_alloc_global "EVP_PKEY_rsa_pkey_meth_once";
  crucible_alloc_global "EVP_PKEY_rsa_pss_pkey_meth_once";
  crucible_alloc_global "EVP_PKEY_ec_pkey_meth_once";
  crucible_alloc_global "EVP_PKEY_hkdf_pkey_meth_once";
  crucible_alloc_global "EVP_PKEY_hmac_pkey_meth_once";
  crucible_alloc_global "AWSLC_fips_evp_pkey_methods_storage.0.0";
  crucible_alloc_global "AWSLC_fips_evp_pkey_methods_storage.0.1";
  crucible_alloc_global "AWSLC_fips_evp_pkey_methods_storage.0.2";
  crucible_alloc_global "AWSLC_fips_evp_pkey_methods_storage.0.3";
  crucible_alloc_global "AWSLC_fips_evp_pkey_methods_storage.0.4";
  crucible_alloc_global "AWSLC_fips_evp_pkey_methods_once";

  ctx_ptr <- crucible_alloc (llvm_struct "struct.env_md_ctx_st");
  points_to_env_md_ctx_st ctx_ptr crucible_null crucible_null crucible_null;

  type_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st");
  points_to_env_md_st type_ptr;

  pkey_ptr <- crucible_alloc (llvm_struct "struct.evp_pkey_st");
  ec_group_ptr <- pointer_to_fresh_ec_group_st;
  (ec_key_ptr, _pub_key, _priv_key) <- pointer_to_fresh_ec_key_st ec_group_ptr is_sign;
  points_to_evp_pkey_st pkey_ptr ec_key_ptr;

  crucible_execute_func [ctx_ptr, crucible_null, type_ptr, crucible_null, pkey_ptr];

  points_to_evp_md_pctx_ops (crucible_global "EVP_MD_pctx_ops_storage");

  sha512_state_ptr <- crucible_alloc (llvm_struct "struct.sha512_state_st");
  res_block <- crucible_fresh_cryptol_var "res_block" {| ByteArray |};
  points_to_sha512_state_st_array_n32 sha512_state_ptr
    {{ { h = SHAInit_Array.h, block = res_block, n = SHAInit_Array.n, sz = SHAInit_Array.sz } }};
  evp_pkey_ctx_ptr <- crucible_alloc (llvm_struct "struct.evp_pkey_ctx_st");
  points_to_EVP_PKEY_ec_pkey_meth (crucible_global "EVP_PKEY_ec_pkey_meth_storage");
  ec_pkey_ctx_ptr <- crucible_alloc (llvm_struct "struct.EC_PKEY_CTX");
  points_to_EC_PKEY_CTX ec_pkey_ctx_ptr type_ptr;
  points_to_evp_pkey_ctx_st evp_pkey_ctx_ptr (crucible_global "EVP_PKEY_ec_pkey_meth_storage") pkey_ptr crucible_null (if is_sign then EVP_PKEY_OP_SIGN else EVP_PKEY_OP_VERIFY) ec_pkey_ctx_ptr;
  points_to_env_md_ctx_st_with_pctx ctx_ptr type_ptr sha512_state_ptr evp_pkey_ctx_ptr (crucible_global "EVP_MD_pctx_ops_storage") (crucible_global SHA_UPDATE);

  crucible_return (crucible_term {{ 1 : [32] }});
};

let EVP_DigestSignVerifyUpdate_spec is_sign = do {
  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};

  ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_ctx_st");

  digest_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st");
  points_to_env_md_st digest_ptr;

  (sha512_state, sha512_state_ptr) <- pointer_to_fresh_sha512_state_st_array_n32 "sha512_state";
  crucible_precond {{ sha512_state.n < `SHA512_CBLOCK }};

  evp_pkey_ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_pkey_ctx_st");
  pmeth_ptr <- pointer_to_evp_pkey_method_st;
  pkey_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_pkey_st");
  ec_group_ptr <- pointer_to_fresh_ec_group_st;
  (ec_key_ptr, _pub_key, _priv_key) <- pointer_to_fresh_ec_key_st ec_group_ptr is_sign;
  points_to_evp_pkey_st pkey_ptr ec_key_ptr;
  ec_pkey_ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.EC_PKEY_CTX");
  points_to_EC_PKEY_CTX ec_pkey_ctx_ptr digest_ptr;
  points_to_evp_pkey_ctx_st evp_pkey_ctx_ptr pmeth_ptr pkey_ptr crucible_null (if is_sign then EVP_PKEY_OP_SIGN else EVP_PKEY_OP_VERIFY) ec_pkey_ctx_ptr;

  pctx_ops_ptr <- pointer_to_evp_md_pctx_ops;

  points_to_env_md_ctx_st_with_pctx ctx_ptr digest_ptr sha512_state_ptr evp_pkey_ctx_ptr pctx_ops_ptr (crucible_global SHA_UPDATE);

  len <- crucible_fresh_var "len" i64;
  (data, data_ptr) <- ptr_to_fresh_array_readonly "data" len;

  crucible_execute_func [ctx_ptr, data_ptr, (crucible_term len)];

  global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};

  let res = {{ ECDSA_SignVerify_Update sha512_state data len }};
  res_block <- crucible_fresh_cryptol_var "res_block" {| ByteArray |};
  points_to_sha512_state_st_array_n32 sha512_state_ptr {{ { h = res.h, block = res_block, n = res.n, sz = res.sz } }};
  crucible_postcond {{ arrayRangeEq res_block 0 res.block 0 `SHA512_CBLOCK }};
  crucible_postcond {{ res.n < `SHA512_CBLOCK }};

  crucible_return (crucible_term {{ 1 : [32] }});
};

let EVP_DigestSignFinal_spec = do {
  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
  alloc_p384_felem_methods_globals;

  ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_ctx_st");

  digest_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st");
  points_to_env_md_st digest_ptr;

  (sha512_state, sha512_state_ptr) <- pointer_to_fresh_sha512_state_st_array_n32 "sha512_state";
  crucible_precond {{ sha512_state.n < `SHA512_CBLOCK }};

  evp_pkey_ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_pkey_ctx_st");
  pmeth_ptr <- pointer_to_evp_pkey_method_st;
  pkey_ptr <- crucible_alloc (llvm_struct "struct.evp_pkey_st");
  ec_group_ptr <- pointer_to_fresh_ec_group_st;
  (ec_key_ptr, _pub_key, priv_key) <- pointer_to_fresh_ec_key_st ec_group_ptr true;
  points_to_evp_pkey_st pkey_ptr ec_key_ptr;
  ec_pkey_ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.EC_PKEY_CTX");
  points_to_EC_PKEY_CTX ec_pkey_ctx_ptr digest_ptr;
  points_to_evp_pkey_ctx_st evp_pkey_ctx_ptr pmeth_ptr pkey_ptr crucible_null EVP_PKEY_OP_SIGN ec_pkey_ctx_ptr;

  pctx_ops_ptr <- pointer_to_evp_md_pctx_ops;

  points_to_env_md_ctx_st_with_pctx ctx_ptr digest_ptr sha512_state_ptr evp_pkey_ctx_ptr pctx_ops_ptr (crucible_global SHA_UPDATE);

  out_sig_ptr <- crucible_alloc (llvm_array max_sig_len i8);
  out_sig_len_ptr <- crucible_alloc i64;
  crucible_points_to out_sig_len_ptr (crucible_term {{ `max_sig_len : [64] }});

  // the symbolic integer to be used as the random integer `k` by the sign
  // operation
  k <- nondeterministic_valid_k priv_key {{ sha512_state }} false;

  crucible_execute_func [ctx_ptr, out_sig_ptr, out_sig_len_ptr];

  global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};

  (r, s) <- points_to_fresh_asn1_sig out_sig_ptr;

  crucible_points_to out_sig_len_ptr (crucible_term {{ `sig_len : [64] }});

  let res = {{ ECDSA_Sign_Final priv_key sha512_state k }};
  crucible_postcond {{ join r == scalarToBV res.r }};
  crucible_postcond {{ join s == scalarToBV res.s }};

  crucible_return (crucible_term {{ 1 : [32] }});
};


let EVP_DigestVerifyFinal_spec = do {
  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
  alloc_p384_felem_methods_globals;

  ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_ctx_st");

  digest_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st");
  points_to_env_md_st digest_ptr;

  (sha512_state, sha512_state_ptr) <- pointer_to_fresh_sha512_state_st_array_n32 "sha512_state";
  crucible_precond {{ sha512_state.n < `SHA512_CBLOCK }};

  evp_pkey_ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_pkey_ctx_st");
  pmeth_ptr <- pointer_to_evp_pkey_method_st;
  pkey_ptr <- crucible_alloc (llvm_struct "struct.evp_pkey_st");
  ec_group_ptr <- pointer_to_fresh_ec_group_st;
  (ec_key_ptr, pub_key, _priv_key) <- pointer_to_fresh_ec_key_st ec_group_ptr false;
  points_to_evp_pkey_st pkey_ptr ec_key_ptr;
  ec_pkey_ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.EC_PKEY_CTX");
  points_to_EC_PKEY_CTX ec_pkey_ctx_ptr digest_ptr;
  points_to_evp_pkey_ctx_st evp_pkey_ctx_ptr pmeth_ptr pkey_ptr crucible_null EVP_PKEY_OP_VERIFY ec_pkey_ctx_ptr;

  pctx_ops_ptr <- pointer_to_evp_md_pctx_ops;

  points_to_env_md_ctx_st_with_pctx ctx_ptr digest_ptr sha512_state_ptr evp_pkey_ctx_ptr pctx_ops_ptr (crucible_global SHA_UPDATE);

  sig_ptr <- crucible_alloc_readonly (llvm_array sig_len i8);
  (r, s) <- points_to_fresh_asn1_sig sig_ptr;

  crucible_precond {{ is_num_bits_bn`{r_bits} (join r) }};
  crucible_precond {{ is_num_bits_bn`{s_bits} (join s) }};

  crucible_execute_func [ctx_ptr, sig_ptr, (crucible_term {{ `sig_len : [64] }})];

  global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};

  let ret = {{ ECDSA_Verify_Final pub_key sha512_state r s }};
  crucible_return (crucible_term {{ if ret then 1 : [32] else 0 }});
};

let EVP_DigestSign_spec = do {
  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
  alloc_p384_felem_methods_globals;

  ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_ctx_st");

  digest_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st");
  points_to_env_md_st digest_ptr;

  (sha512_state, sha512_state_ptr) <- pointer_to_fresh_sha512_state_st_array_n32 "sha512_state";
  crucible_precond {{ sha512_state.n < `SHA512_CBLOCK }};

  evp_pkey_ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_pkey_ctx_st");
  pmeth_ptr <- pointer_to_evp_pkey_method_st;
  pkey_ptr <- crucible_alloc (llvm_struct "struct.evp_pkey_st");
  ec_group_ptr <- pointer_to_fresh_ec_group_st;
  (ec_key_ptr, _pub_key, priv_key) <- pointer_to_fresh_ec_key_st ec_group_ptr true;
  points_to_evp_pkey_st pkey_ptr ec_key_ptr;
  ec_pkey_ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.EC_PKEY_CTX");
  points_to_EC_PKEY_CTX ec_pkey_ctx_ptr digest_ptr;
  points_to_evp_pkey_ctx_st evp_pkey_ctx_ptr pmeth_ptr pkey_ptr crucible_null EVP_PKEY_OP_SIGN ec_pkey_ctx_ptr;

  pctx_ops_ptr <- pointer_to_evp_md_pctx_ops;

  points_to_env_md_ctx_st_with_pctx ctx_ptr digest_ptr sha512_state_ptr evp_pkey_ctx_ptr pctx_ops_ptr (crucible_global SHA_UPDATE);

  out_sig_ptr <- crucible_alloc (llvm_array max_sig_len i8);
  out_sig_len_ptr <- crucible_alloc i64;
  crucible_points_to out_sig_len_ptr (crucible_term {{ `max_sig_len : [64] }});

  data_len <- crucible_fresh_var "data_len" i64;
  (data, data_ptr) <- ptr_to_fresh_array_readonly "data" data_len;

  // the symbolic integer to be used as the random integer `k` by the sign
  // operation
  k <- nondeterministic_valid_k priv_key {{ ECDSA_SignVerify_Update sha512_state data data_len }} false;

  crucible_execute_func [ctx_ptr, out_sig_ptr, out_sig_len_ptr, data_ptr, (crucible_term data_len)];

  global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};

  (r, s) <- points_to_fresh_asn1_sig out_sig_ptr;

  crucible_points_to out_sig_len_ptr (crucible_term {{ `sig_len : [64] }});

  let res = {{ ECDSA_Sign_Final priv_key (ECDSA_SignVerify_Update sha512_state data data_len) k }};
  crucible_postcond {{ join r == scalarToBV res.r }};
  crucible_postcond {{ join s == scalarToBV res.s }};

  crucible_return (crucible_term {{ 1 : [32] }});
};

let EVP_DigestVerify_spec = do {
  global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
  alloc_p384_felem_methods_globals;

  ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_ctx_st");

  digest_ptr <- crucible_alloc_readonly (llvm_struct "struct.env_md_st");
  points_to_env_md_st digest_ptr;

  (sha512_state, sha512_state_ptr) <- pointer_to_fresh_sha512_state_st_array_n32 "sha512_state";
  crucible_precond {{ sha512_state.n < `SHA512_CBLOCK }};

  evp_pkey_ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_pkey_ctx_st");
  pmeth_ptr <- pointer_to_evp_pkey_method_st;
  pkey_ptr <- crucible_alloc (llvm_struct "struct.evp_pkey_st");
  ec_group_ptr <- pointer_to_fresh_ec_group_st;
  (ec_key_ptr, pub_key, _priv_key) <- pointer_to_fresh_ec_key_st ec_group_ptr false;
  points_to_evp_pkey_st pkey_ptr ec_key_ptr;
  ec_pkey_ctx_ptr <- crucible_alloc_readonly (llvm_struct "struct.EC_PKEY_CTX");
  points_to_EC_PKEY_CTX ec_pkey_ctx_ptr digest_ptr;
  points_to_evp_pkey_ctx_st evp_pkey_ctx_ptr pmeth_ptr pkey_ptr crucible_null EVP_PKEY_OP_VERIFY ec_pkey_ctx_ptr;

  pctx_ops_ptr <- pointer_to_evp_md_pctx_ops;

  points_to_env_md_ctx_st_with_pctx ctx_ptr digest_ptr sha512_state_ptr evp_pkey_ctx_ptr pctx_ops_ptr (crucible_global SHA_UPDATE);

  len <- crucible_fresh_var "len" i64;
  (data, data_ptr) <- ptr_to_fresh_array_readonly "data" len;

  sig_ptr <- crucible_alloc_readonly (llvm_array sig_len i8);
  (r, s) <- points_to_fresh_asn1_sig sig_ptr;

  crucible_precond {{ is_num_bits_bn`{r_bits} (join r) }};
  crucible_precond {{ is_num_bits_bn`{s_bits} (join s) }};

  crucible_execute_func [ctx_ptr, sig_ptr, (crucible_term {{ `sig_len : [64] }}), data_ptr, (crucible_term len)];

  global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};

  let ret = {{ ECDSA_Verify_Final pub_key (ECDSA_SignVerify_Update sha512_state data len) r s }};
  crucible_return (crucible_term {{ if ret then 1 : [32] else 0 }});
};