Fix type inconsistencies in CBMC proof harnesses

verification/cbmc/include/make_common_data_structures.h

@@ -19,6 +19,7 @@
 #include <aws/cryptosdk/materials.h>
 #include <aws/cryptosdk/private/framefmt.h>
 #include <aws/cryptosdk/private/header.h>
+#include <aws/cryptosdk/private/hkdf.h>
 #include <proof_helpers/make_common_data_structures.h>
 #include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
@@ -114,4 +115,5 @@ struct aws_cryptosdk_enc_request *ensure_enc_request_attempt_allocation(const si
 struct aws_cryptosdk_enc_materials *ensure_enc_materials_attempt_allocation();
 
 /* Allocates the members of the default_cmm and ensures that internal pointers are pointing to the correct objects. */
-struct aws_cryptosdk_cmm *ensure_default_cmm_attempt_allocation(const struct aws_cryptosdk_keyring_vt *vtable);
+struct aws_cryptosdk_cmm *ensure_default_cmm_attempt_allocation(
+    const struct aws_cryptosdk_cmm_vt *cmm_vtable, const struct aws_cryptosdk_keyring_vt *vtable);

verification/cbmc/include/openssl/evp.h

@@ -62,6 +62,7 @@ EVP_MD_CTX *EVP_MD_CTX_new(void);
 int EVP_MD_CTX_size(const EVP_MD_CTX *ctx);
 void EVP_MD_CTX_free(EVP_MD_CTX *ctx);
 int EVP_DigestInit_ex(EVP_MD_CTX *ctx, const EVP_MD *type, ENGINE *impl);
+int EVP_DigestInit(EVP_MD_CTX *ctx, const EVP_MD *type);
 int EVP_DigestUpdate(EVP_MD_CTX *ctx, const void *d, size_t cnt);
 int EVP_DigestFinal_ex(EVP_MD_CTX *ctx, unsigned char *md, unsigned int *s);
 int EVP_DigestFinal(EVP_MD_CTX *ctx, unsigned char *md, unsigned int *s);

verification/cbmc/include/openssl/rand.h

@@ -14,4 +14,4 @@
  * permissions and limitations under the License.
  */
 
-/* Empty header. Necessary just because it is included in cipher.c */
+int RAND_bytes(unsigned char *buf, int num);

verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/aws_cryptosdk_cmm_decrypt_materials_harness.c

@@ -120,7 +120,7 @@ void aws_cryptosdk_cmm_decrypt_materials_harness() {
     */
     __CPROVER_assume(aws_cryptosdk_dec_request_is_valid(request));
 
-    struct aws_cryptosdk_enc_materials **output = can_fail_malloc(sizeof(*output));
+    struct aws_cryptosdk_dec_materials **output = can_fail_malloc(sizeof(*output));
     __CPROVER_assume(output);
 
     // Run the function under test.

verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/aws_cryptosdk_edk_list_copy_all_harness.c

@@ -17,6 +17,7 @@
  */
 
 #include <aws/cryptosdk/edk.h>
+#include <aws/cryptosdk/list_utils.h>
 #include <make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
 #include <proof_helpers/proof_allocators.h>
@@ -65,14 +66,15 @@ const size_t g_item_size = sizeof(struct aws_cryptosdk_edk);
  * These stubs capture the key aspect of checking that the element is allocated.
  * It writes/reads a magic constant to ensure that we only ever _clean_up() data that we cloned
  */
-int aws_cryptosdk_edk_init_clone(struct aws_allocator *alloc, void *dest, void *src) {
+int aws_cryptosdk_edk_init_clone(
+    struct aws_allocator *alloc, struct aws_cryptosdk_edk *dest, const struct aws_cryptosdk_edk *src) {
     assert(AWS_MEM_IS_READABLE(src, g_item_size));
     uint8_t *d = (uint8_t *)dest;
     *d         = 0xab;
     return nondet_int();
 }
 
-void aws_cryptosdk_edk_clean_up(void *p) {
+void aws_cryptosdk_edk_clean_up(struct aws_cryptosdk_edk *p) {
     uint8_t *d = (uint8_t *)p;
     assert(*d == 0xab);
 }

verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/aws_cryptosdk_enc_ctx_clear_harness.c

@@ -31,5 +31,5 @@ void aws_cryptosdk_enc_ctx_clear_harness() {
     aws_cryptosdk_enc_ctx_clear(&map);
     assert(aws_hash_table_is_valid(&map));
     struct hash_table_state *impl = map.p_impl;
-    assert_all_zeroes(&impl->slots[0], impl->size * sizeof(impl->slots[0]));
+    assert_all_zeroes((const uint8_t *)&impl->slots[0], impl->size * sizeof(impl->slots[0]));
 }

verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/aws_cryptosdk_enc_ctx_deserialize_harness.c

@@ -16,6 +16,7 @@
 #include <aws/common/hash_table.h>
 #include <aws/common/private/hash_table_impl.h>
 #include <aws/cryptosdk/enc_ctx.h>
+#include <aws/cryptosdk/private/enc_ctx.h>
 #include <proof_helpers/make_common_data_structures.h>
 #include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>

verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/aws_cryptosdk_enc_ctx_serialize_harness.c

@@ -16,6 +16,7 @@
 #include <aws/common/hash_table.h>
 #include <aws/common/private/hash_table_impl.h>
 #include <aws/cryptosdk/enc_ctx.h>
+#include <aws/cryptosdk/private/enc_ctx.h>
 #include <proof_helpers/make_common_data_structures.h>
 #include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>

verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/aws_cryptosdk_enc_ctx_size_harness.c

@@ -16,6 +16,7 @@
 #include <aws/common/hash_table.h>
 #include <aws/common/private/hash_table_impl.h>
 #include <aws/cryptosdk/enc_ctx.h>
+#include <aws/cryptosdk/private/enc_ctx.h>
 #include <proof_helpers/make_common_data_structures.h>
 #include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>

verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/aws_cryptosdk_enc_materials_new_harness.c

@@ -32,7 +32,7 @@ void aws_cryptosdk_enc_materials_new_harness() {
     __CPROVER_assume(aws_allocator_is_valid(alloc));
 
     /* Operation under verification. */
-    struct aws_cryptosdk_dec_materials *enc_mat = aws_cryptosdk_enc_materials_new(alloc, alg);
+    struct aws_cryptosdk_enc_materials *enc_mat = aws_cryptosdk_enc_materials_new(alloc, alg);
 
     /* Post-conditions. */
     if (enc_mat != NULL) {

verification/cbmc/proofs/aws_cryptosdk_hkdf/aws_cryptosdk_hkdf_harness.c

@@ -15,9 +15,17 @@
 
 #include <aws/cryptosdk/cipher.h>
 #include <aws/cryptosdk/private/cipher.h>
+#include <aws/cryptosdk/private/hkdf.h>
 
 #include <make_common_data_structures.h>
 
+int aws_cryptosdk_hkdf(
+    struct aws_byte_buf *okm,
+    enum aws_cryptosdk_sha_version which_sha,
+    const struct aws_byte_buf *salt,
+    const struct aws_byte_buf *ikm,
+    const struct aws_byte_buf *info);
+
 void aws_cryptosdk_hkdf_harness() {
     /* arguments */
 
@@ -58,7 +66,7 @@ void aws_cryptosdk_hkdf_harness() {
     struct store_byte_from_buffer old_byte_from_info;
     save_byte_from_array(info.buffer, info.len, &old_byte_from_info);
 
-    aws_cryptosdk_hkdf(&okm, alg_id, &salt, &ikm, &info);
+    aws_cryptosdk_hkdf(&okm, which_sha, &salt, &ikm, &info);
 
     /* assertions */
     assert(aws_byte_buf_is_valid(&salt));

verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/aws_cryptosdk_keyring_trace_copy_all_harness.c

@@ -17,6 +17,7 @@
  */
 
 #include <aws/cryptosdk/keyring_trace.h>
+#include <aws/cryptosdk/list_utils.h>
 #include <make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
 #include <proof_helpers/proof_allocators.h>
@@ -96,14 +97,17 @@ const size_t g_item_size = sizeof(struct aws_cryptosdk_keyring_trace_record);
  * These stubs capture the key aspect of checking that the element is allocated.
  * It writes/reads a magic constant to ensure that we only ever _clean_up() data that we cloned
  */
-int aws_cryptosdk_keyring_trace_record_init_clone(struct aws_allocator *alloc, void *dest, const void *src) {
+int aws_cryptosdk_keyring_trace_record_init_clone(
+    struct aws_allocator *alloc,
+    struct aws_cryptosdk_keyring_trace_record *dest,
+    const struct aws_cryptosdk_keyring_trace_record *src) {
     assert(AWS_MEM_IS_READABLE(src, g_item_size));
     uint8_t *d = (uint8_t *)dest;
     *d         = 0xab;
     return nondet_int();
 }
 
-void aws_cryptosdk_keyring_trace_record_clean_up(void *p) {
+void aws_cryptosdk_keyring_trace_record_clean_up(struct aws_cryptosdk_keyring_trace_record *p) {
     uint8_t *d = (uint8_t *)p;
     assert(*d == 0xab);
 }

verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/aws_cryptosdk_multi_keyring_add_child_harness.c

@@ -39,7 +39,7 @@ void aws_cryptosdk_multi_keyring_add_child_harness() {
      * structure must have as base member the static aws_cryptosdk_keyring_vt (vt) defined
      * in the multi_keyring.c file.
      */
-    struct multi_keyring *multi = aws_cryptosdk_multi_keyring_new(alloc, &generator);
+    struct aws_cryptosdk_keyring *multi = aws_cryptosdk_multi_keyring_new(alloc, &generator);
     __CPROVER_assume(aws_cryptosdk_multi_keyring_is_valid(multi));
 
     const struct aws_cryptosdk_keyring_vt vtable_child = { .vt_size    = sizeof(struct aws_cryptosdk_keyring_vt),
@@ -52,13 +52,13 @@ void aws_cryptosdk_multi_keyring_add_child_harness() {
     __CPROVER_assume(aws_cryptosdk_keyring_is_valid(&child));
 
     /* save current state of the data structure */
-    struct aws_array_list old = multi->children;
+    struct aws_array_list old = ((struct multi_keyring *)multi)->children;
 
     /* Operation under verification. */
     if (aws_cryptosdk_multi_keyring_add_child(multi, &child) == AWS_OP_SUCCESS) {
-        assert(multi->children.length == (old.length + 1));
+        assert(((struct multi_keyring *)multi)->children.length == (old.length + 1));
     } else {
-        assert(multi->children.length == old.length);
+        assert(((struct multi_keyring *)multi)->children.length == old.length);
     }
 
     /* Post-conditions. */

verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/aws_cryptosdk_private_derive_key_v1_harness.c

@@ -19,6 +19,12 @@
 #include <make_common_data_structures.h>
 #include <utils.h>
 
+int __CPROVER_file_local_cipher_c_aws_cryptosdk_private_derive_key_v1(
+    const struct aws_cryptosdk_alg_properties *props,
+    struct content_key *content_key,
+    const struct data_key *data_key,
+    const struct aws_byte_buf *message_id);
+
 void aws_cryptosdk_private_derive_key_v1_harness() {
     struct aws_cryptosdk_alg_properties *props = ensure_alg_properties_attempt_allocation(MAX_STRING_LEN);
     struct content_key *content_key            = ensure_content_key_attempt_allocation();

verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/aws_cryptosdk_private_derive_key_v2_harness.c

@@ -18,6 +18,13 @@
 #include <aws/cryptosdk/private/hkdf.h>
 #include <make_common_data_structures.h>
 
+int __CPROVER_file_local_cipher_c_aws_cryptosdk_private_derive_key_v2(
+    const struct aws_cryptosdk_alg_properties *props,
+    struct content_key *content_key,
+    const struct data_key *data_key,
+    struct aws_byte_buf *commitment,
+    const struct aws_byte_buf *message_id);
+
 void aws_cryptosdk_private_derive_key_v2_harness() {
     struct aws_cryptosdk_alg_properties *props = ensure_alg_properties_attempt_allocation(MAX_STRING_LEN);
     struct content_key *content_key            = ensure_content_key_attempt_allocation();

verification/cbmc/proofs/aws_cryptosdk_transfer_list/aws_cryptosdk_transfer_list_harness.c

@@ -17,6 +17,7 @@
  */
 
 #include <aws/cryptosdk/edk.h>
+#include <aws/cryptosdk/list_utils.h>
 #include <proof_helpers/cryptosdk/make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
 #include <proof_helpers/proof_allocators.h>

verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

@@ -20,6 +20,11 @@
 #include <aws/cryptosdk/materials.h>
 #include <make_common_data_structures.h>
 
+int generate_enc_materials(
+    struct aws_cryptosdk_cmm *cmm,
+    struct aws_cryptosdk_enc_materials **output,
+    struct aws_cryptosdk_enc_request *request);
+
 int on_encrypt(
     struct aws_cryptosdk_keyring *keyring,
     struct aws_allocator *request_alloc,
@@ -29,14 +34,25 @@ int on_encrypt(
     const struct aws_hash_table *enc_ctx,
     enum aws_cryptosdk_alg_id alg);
 
+int __CPROVER_file_local_default_cmm_c_default_cmm_generate_enc_materials(
+    struct aws_cryptosdk_cmm *cmm,
+    struct aws_cryptosdk_enc_materials **output,
+    struct aws_cryptosdk_enc_request *request);
+
 void default_cmm_generate_enc_materials_harness() {
+    const struct aws_cryptosdk_cmm_vt cmm_vtable = { .vt_size = nondet_size_t(),
+                                                     .name    = ensure_c_str_is_allocated(SIZE_MAX),
+                                                     .destroy = nondet_voidp(),
+                                                     .generate_enc_materials =
+                                                         nondet_bool() ? NULL : generate_enc_materials,
+                                                     .decrypt_materials = nondet_voidp() };
     const struct aws_cryptosdk_keyring_vt vtable = { .vt_size    = nondet_size_t(),
                                                      .name       = ensure_c_str_is_allocated(SIZE_MAX),
                                                      .destroy    = nondet_voidp(),
                                                      .on_encrypt = nondet_bool() ? NULL : on_encrypt,
                                                      .on_decrypt = nondet_voidp() };
     /* Nondet input */
-    struct aws_cryptosdk_cmm *cmm              = ensure_default_cmm_attempt_allocation(&vtable);
+    struct aws_cryptosdk_cmm *cmm              = ensure_default_cmm_attempt_allocation(&cmm_vtable, &vtable);
     struct aws_cryptosdk_enc_materials *output = ensure_enc_materials_attempt_allocation();
     struct aws_cryptosdk_enc_request *request  = ensure_enc_request_attempt_allocation(MAX_TABLE_SIZE);
 

verification/cbmc/proofs/derive_data_key/derive_data_key_harness.c

@@ -23,6 +23,9 @@
 #include <aws/cryptosdk/session.h>
 #include <make_common_data_structures.h>
 
+int __CPROVER_file_local_session_decrypt_c_derive_data_key(
+    struct aws_cryptosdk_session *session, struct aws_cryptosdk_dec_materials *materials);
+
 void derive_data_key_harness() {
     /* Setup functions include nondet. allocation and common assumptions */
     struct aws_cryptosdk_session *session =

verification/cbmc/proofs/list_copy_all/list_copy_all_harness.c

@@ -59,6 +59,13 @@ bool aws_array_list_is_valid_deep(const struct aws_array_list *AWS_RESTRICT list
 typedef int (*clone_item_fn)(struct aws_allocator *, void *, const void *);
 typedef void (*clean_up_item_fn)(void *);
 
+int __CPROVER_file_local_list_utils_c_list_copy_all(
+    struct aws_allocator *alloc,
+    struct aws_array_list *dest,
+    const struct aws_array_list *src,
+    clone_item_fn cloner,
+    clean_up_item_fn cleaner);
+
 size_t g_item_size;
 
 /**

verification/cbmc/proofs/sign_header/sign_header_harness.c

@@ -20,6 +20,8 @@
 #include <make_common_data_structures.h>
 #include <proof_helpers/make_common_data_structures.h>
 
+int __CPROVER_file_local_session_encrypt_c_sign_header(struct aws_cryptosdk_session *session);
+
 /**
  * A generator function as described in the comment in aws_cryptosdk_hash_elems_array_init_stub.c.
  * Also see DEFINES += -DAWS_CRYPTOSDK_HASH_ELEMS_ARRAY_INIT_GENERATOR=array_list_item_generator

verification/cbmc/sources/make_common_data_structures.c

@@ -38,6 +38,7 @@ struct default_cmm {
     struct aws_cryptosdk_keyring *kr;
     /* Invariant: this is either DEFAULT_ALG_UNSET or is a valid algorithm ID */
     enum aws_cryptosdk_alg_id default_alg;
+    bool default_alg_is_set;
 };
 
 const EVP_MD *nondet_EVP_MD_ptr(void);
@@ -46,10 +47,10 @@ const EVP_CIPHER *nondet_EVP_CIPHER_ptr(void);
 struct aws_cryptosdk_alg_impl *ensure_impl_attempt_allocation(const size_t max_len) {
     struct aws_cryptosdk_alg_impl *impl = malloc(sizeof(struct aws_cryptosdk_alg_impl));
     if (impl) {
-        *(const EVP_MD **)(&impl->md_ctor)         = (nondet_bool()) ? NULL : &nondet_EVP_MD_ptr;
-        *(const EVP_MD **)(&impl->sig_md_ctor)     = (nondet_bool()) ? NULL : &nondet_EVP_MD_ptr;
-        *(const EVP_CIPHER **)(&impl->cipher_ctor) = (nondet_bool()) ? NULL : &nondet_EVP_CIPHER_ptr;
-        *(const char **)(&impl->curve_name)        = ensure_c_str_is_allocated(max_len);
+        impl->md_ctor     = (nondet_bool()) ? NULL : &nondet_EVP_MD_ptr;
+        impl->sig_md_ctor = (nondet_bool()) ? NULL : &nondet_EVP_MD_ptr;
+        impl->cipher_ctor = (nondet_bool()) ? NULL : &nondet_EVP_CIPHER_ptr;
+        impl->curve_name  = ensure_c_str_is_allocated(max_len);
     }
     return impl;
 }
@@ -398,14 +399,15 @@ struct aws_cryptosdk_enc_materials *ensure_enc_materials_attempt_allocation() {
     if (materials) {
         materials->alloc   = nondet_bool() ? NULL : can_fail_allocator();
         materials->signctx = ensure_nondet_sig_ctx_has_allocated_members();
-        ensure_byte_buf_has_allocated_buffer_member(&materials->encrypted_data_keys);
+        ensure_array_list_has_allocated_data_member(&materials->encrypted_data_keys);
         ensure_array_list_has_allocated_data_member(&materials->keyring_trace);
         ensure_array_list_has_allocated_data_member(&materials->encrypted_data_keys);
     }
     return materials;
 }
 
-struct aws_cryptosdk_cmm *ensure_default_cmm_attempt_allocation(const struct aws_cryptosdk_keyring_vt *vtable) {
+struct aws_cryptosdk_cmm *ensure_default_cmm_attempt_allocation(
+    const struct aws_cryptosdk_cmm_vt *cmm_vtable, const struct aws_cryptosdk_keyring_vt *vtable) {
     /* Nondet input required to init cmm */
     struct aws_cryptosdk_keyring *keyring = malloc(sizeof(*keyring));
 
@@ -416,7 +418,7 @@ struct aws_cryptosdk_cmm *ensure_default_cmm_attempt_allocation(const struct aws
 
     struct aws_cryptosdk_cmm *cmm = malloc(sizeof(struct default_cmm));
     if (cmm) {
-        cmm->vtable = vtable;
+        cmm->vtable = cmm_vtable;
     }
 
     struct default_cmm *self = NULL;

verification/cbmc/sources/openssl/asn1_override.c

@@ -32,6 +32,8 @@ void ASN1_STRING_clear_free(ASN1_STRING *a) {
     free(a);
 }
 
+bool asn1_integer_is_valid(ASN1_INTEGER *ai);
+
 /*
  * Description: ASN1_INTEGER_to_BN() converts ASN1_INTEGER ai into a BIGNUM. If bn is NULL a new BIGNUM structure is
  * returned. If bn is not NULL then the existing structure will be used instead. Return values: ASN1_INTEGER_to_BN() and

verification/cbmc/sources/openssl/bio_override.c

@@ -43,16 +43,16 @@ BIO *BIO_new_mem_buf(const void *buf, signed int len) {
  * SubjectPublicKeyInfo structure.
  */
 EVP_PKEY *PEM_read_bio_PUBKEY(BIO *bp, EVP_PKEY **x, pem_password_cb *cb, void *u) {
-    x = EVP_PKEY_new();
-    return x;
+    *x = EVP_PKEY_new();
+    return *x;
 }
 
 /*
  * Read a private key from a BIO.
  */
 EVP_PKEY *PEM_read_bio_PrivateKey(BIO *bp, EVP_PKEY **x, pem_password_cb *cb, void *u) {
-    x = EVP_PKEY_new();
-    return x;
+    *x = EVP_PKEY_new();
+    return *x;
 }
 
 /*

verification/cbmc/sources/openssl/ec_override.c

@@ -59,6 +59,8 @@ void EC_GROUP_set_point_conversion_form(EC_GROUP *group, point_conversion_form_t
     group->asn1_form = form;
 }
 
+bool ec_group_is_valid(EC_GROUP *group);
+
 /*
  * Return values: EC_GROUP_get0_order() returns an internal pointer to the group order.
  */
@@ -283,6 +285,8 @@ struct ECDSA_SIG_st {
     BIGNUM *s;
 };
 
+bool ecdsa_sig_is_valid(ECDSA_SIG *sig);
+
 /*
  * Description: ECDSA_SIG_get0() returns internal pointers the r and s values contained in sig and stores them in *pr
  * and *ps, respectively. The pointer pr or ps can be NULL, in which case the corresponding value is not returned.

verification/cbmc/sources/openssl/err_override.c

@@ -13,6 +13,7 @@
  * permissions and limitations under the License.
  */
 
+#include <assert.h>
 #include <openssl/err.h>
 
 void ERR_print_errors_fp(FILE *fp) {