fix: type inconsistencies in CBMC proof harnesses

These changes add necessary forward declarations (or system headers
includes) and address inconsistencies in how we invoke functions from
CBMC proof harnesses as compared to their original signatures.

Author: tautschnig

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,6 @@ 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,17 @@ 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,24 @@ 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,10 @@
 #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,16 @@ 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 +419,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.