diff --git a/verification/cbmc/include/make_common_data_structures.h b/verification/cbmc/include/make_common_data_structures.h index bc327a3bf..abb390b95 100644 --- a/verification/cbmc/include/make_common_data_structures.h +++ b/verification/cbmc/include/make_common_data_structures.h @@ -19,6 +19,7 @@ #include #include #include +#include #include #include #include @@ -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); diff --git a/verification/cbmc/include/openssl/evp.h b/verification/cbmc/include/openssl/evp.h index c925856df..9d9b33293 100644 --- a/verification/cbmc/include/openssl/evp.h +++ b/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); diff --git a/verification/cbmc/include/openssl/rand.h b/verification/cbmc/include/openssl/rand.h index 22b4b15be..cdfac91ea 100644 --- a/verification/cbmc/include/openssl/rand.h +++ b/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); diff --git a/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/aws_cryptosdk_cmm_decrypt_materials_harness.c b/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/aws_cryptosdk_cmm_decrypt_materials_harness.c index f5a76141b..e2c2508cc 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_cmm_decrypt_materials/aws_cryptosdk_cmm_decrypt_materials_harness.c +++ b/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. diff --git a/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/aws_cryptosdk_edk_list_copy_all_harness.c b/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/aws_cryptosdk_edk_list_copy_all_harness.c index 73e9878af..6b74aaa01 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/aws_cryptosdk_edk_list_copy_all_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_edk_list_copy_all/aws_cryptosdk_edk_list_copy_all_harness.c @@ -17,6 +17,7 @@ */ #include +#include #include #include #include @@ -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); } diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/aws_cryptosdk_enc_ctx_clear_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/aws_cryptosdk_enc_ctx_clear_harness.c index e504833cd..124188f74 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_clear/aws_cryptosdk_enc_ctx_clear_harness.c +++ b/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])); } diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/aws_cryptosdk_enc_ctx_deserialize_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/aws_cryptosdk_enc_ctx_deserialize_harness.c index dba79f5e8..fb7f17bdd 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/aws_cryptosdk_enc_ctx_deserialize_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_deserialize/aws_cryptosdk_enc_ctx_deserialize_harness.c @@ -16,6 +16,7 @@ #include #include #include +#include #include #include #include diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/aws_cryptosdk_enc_ctx_serialize_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/aws_cryptosdk_enc_ctx_serialize_harness.c index aeda45b42..c64db09f2 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/aws_cryptosdk_enc_ctx_serialize_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_serialize/aws_cryptosdk_enc_ctx_serialize_harness.c @@ -16,6 +16,7 @@ #include #include #include +#include #include #include #include diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/aws_cryptosdk_enc_ctx_size_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/aws_cryptosdk_enc_ctx_size_harness.c index 0445e024c..df20c7e64 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/aws_cryptosdk_enc_ctx_size_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_enc_ctx_size/aws_cryptosdk_enc_ctx_size_harness.c @@ -16,6 +16,7 @@ #include #include #include +#include #include #include #include diff --git a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/aws_cryptosdk_enc_materials_new_harness.c b/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/aws_cryptosdk_enc_materials_new_harness.c index 1b6542ff3..f62a063f0 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_enc_materials_new/aws_cryptosdk_enc_materials_new_harness.c +++ b/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) { diff --git a/verification/cbmc/proofs/aws_cryptosdk_hkdf/aws_cryptosdk_hkdf_harness.c b/verification/cbmc/proofs/aws_cryptosdk_hkdf/aws_cryptosdk_hkdf_harness.c index f8f1c9560..2c29ae3b7 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_hkdf/aws_cryptosdk_hkdf_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_hkdf/aws_cryptosdk_hkdf_harness.c @@ -15,9 +15,17 @@ #include #include +#include #include +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)); diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/aws_cryptosdk_keyring_trace_copy_all_harness.c b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/aws_cryptosdk_keyring_trace_copy_all_harness.c index 7fb8a4fd4..76eb8c7b8 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/aws_cryptosdk_keyring_trace_copy_all_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/aws_cryptosdk_keyring_trace_copy_all_harness.c @@ -17,6 +17,7 @@ */ #include +#include #include #include #include @@ -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); } diff --git a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/aws_cryptosdk_multi_keyring_add_child_harness.c b/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/aws_cryptosdk_multi_keyring_add_child_harness.c index f8bc1767e..baf7fa640 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_multi_keyring_add_child/aws_cryptosdk_multi_keyring_add_child_harness.c +++ b/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. */ diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/aws_cryptosdk_private_derive_key_v1_harness.c b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/aws_cryptosdk_private_derive_key_v1_harness.c index ffa0c83f3..9ccf93a0b 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/aws_cryptosdk_private_derive_key_v1_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v1/aws_cryptosdk_private_derive_key_v1_harness.c @@ -19,6 +19,12 @@ #include #include +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(); diff --git a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/aws_cryptosdk_private_derive_key_v2_harness.c b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/aws_cryptosdk_private_derive_key_v2_harness.c index bb3a99fdc..cf7408869 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/aws_cryptosdk_private_derive_key_v2_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_private_derive_key_v2/aws_cryptosdk_private_derive_key_v2_harness.c @@ -18,6 +18,13 @@ #include #include +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(); diff --git a/verification/cbmc/proofs/aws_cryptosdk_transfer_list/aws_cryptosdk_transfer_list_harness.c b/verification/cbmc/proofs/aws_cryptosdk_transfer_list/aws_cryptosdk_transfer_list_harness.c index 913376c68..f133bf88c 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_transfer_list/aws_cryptosdk_transfer_list_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_transfer_list/aws_cryptosdk_transfer_list_harness.c @@ -17,6 +17,7 @@ */ #include +#include #include #include #include diff --git a/verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c b/verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c index 4c188d62c..2fd3e3b17 100644 --- a/verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c +++ b/verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c @@ -20,6 +20,11 @@ #include #include +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); diff --git a/verification/cbmc/proofs/derive_data_key/derive_data_key_harness.c b/verification/cbmc/proofs/derive_data_key/derive_data_key_harness.c index 1a3fdd95b..b105d7e5d 100644 --- a/verification/cbmc/proofs/derive_data_key/derive_data_key_harness.c +++ b/verification/cbmc/proofs/derive_data_key/derive_data_key_harness.c @@ -23,6 +23,9 @@ #include #include +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 = diff --git a/verification/cbmc/proofs/list_copy_all/list_copy_all_harness.c b/verification/cbmc/proofs/list_copy_all/list_copy_all_harness.c index 7c47c45c8..49168c7c1 100644 --- a/verification/cbmc/proofs/list_copy_all/list_copy_all_harness.c +++ b/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; /** diff --git a/verification/cbmc/proofs/sign_header/sign_header_harness.c b/verification/cbmc/proofs/sign_header/sign_header_harness.c index 72e888f23..e638bc6e1 100644 --- a/verification/cbmc/proofs/sign_header/sign_header_harness.c +++ b/verification/cbmc/proofs/sign_header/sign_header_harness.c @@ -20,6 +20,8 @@ #include #include +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 diff --git a/verification/cbmc/sources/make_common_data_structures.c b/verification/cbmc/sources/make_common_data_structures.c index fcd59d39a..55d4476c0 100644 --- a/verification/cbmc/sources/make_common_data_structures.c +++ b/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; diff --git a/verification/cbmc/sources/openssl/asn1_override.c b/verification/cbmc/sources/openssl/asn1_override.c index 55622fb5d..42e7e3c84 100644 --- a/verification/cbmc/sources/openssl/asn1_override.c +++ b/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 diff --git a/verification/cbmc/sources/openssl/bio_override.c b/verification/cbmc/sources/openssl/bio_override.c index 479397f5f..41a59129f 100644 --- a/verification/cbmc/sources/openssl/bio_override.c +++ b/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; } /* diff --git a/verification/cbmc/sources/openssl/ec_override.c b/verification/cbmc/sources/openssl/ec_override.c index ce8e6bcec..0ce01997c 100644 --- a/verification/cbmc/sources/openssl/ec_override.c +++ b/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. diff --git a/verification/cbmc/sources/openssl/err_override.c b/verification/cbmc/sources/openssl/err_override.c index a598b90a7..8d22a5b90 100644 --- a/verification/cbmc/sources/openssl/err_override.c +++ b/verification/cbmc/sources/openssl/err_override.c @@ -13,6 +13,7 @@ * permissions and limitations under the License. */ +#include #include void ERR_print_errors_fp(FILE *fp) { diff --git a/verification/cbmc/sources/openssl/evp_override.c b/verification/cbmc/sources/openssl/evp_override.c index 3681b32e1..539a0d4ab 100644 --- a/verification/cbmc/sources/openssl/evp_override.c +++ b/verification/cbmc/sources/openssl/evp_override.c @@ -91,6 +91,8 @@ struct evp_pkey_ctx_st { EVP_PKEY *pkey; }; +bool evp_pkey_is_valid(EVP_PKEY *pkey); + /* * Description: The EVP_PKEY_CTX_new() function allocates public key algorithm context using the algorithm specified in * pkey and ENGINE e. Return values: EVP_PKEY_CTX_new() returns either the newly allocated EVP_PKEY_CTX structure of @@ -173,6 +175,8 @@ int EVP_PKEY_sign_init(EVP_PKEY_CTX *ctx) { return rv; } +bool evp_pkey_ctx_is_valid(EVP_PKEY_CTX *); + /* * Description: The EVP_PKEY_sign() function performs a public key signing operation using ctx. The data to be signed is * specified using the tbs and tbslen parameters. If sig is NULL then the maximum size of the output buffer is written @@ -723,6 +727,12 @@ int EVP_MD_size(const EVP_MD *md) { return 512; } +/* Helper function for CBMC proofs: checks if EVP_MD_CTX is valid. */ +bool evp_md_ctx_is_valid(EVP_MD_CTX *ctx) { + return ctx && ctx->is_initialized && ctx->digest_size <= EVP_MAX_MD_SIZE && + (ctx->pkey == NULL || evp_pkey_is_valid(ctx->pkey)); +} + /* * Description: Allocates and returns a digest context. */ @@ -757,6 +767,8 @@ void EVP_MD_CTX_free(EVP_MD_CTX *ctx) { } } +bool evp_md_is_valid(EVP_MD *md); + /* * Description: Sets up digest context ctx to use a digest type from ENGINE impl. type will typically be supplied by * a function such as EVP_sha1(). If impl is NULL then the default implementation of digest type is used. Return @@ -931,6 +943,8 @@ unsigned char *HMAC( return res; } +bool hmac_ctx_is_valid(HMAC_CTX *ctx); + /* * HMAC_Init_ex() initializes or reuses a HMAC_CTX structure to use the hash function evp_md and key key. * If both are NULL (or evp_md is the same as the previous digest used by ctx and key is NULL) the existing key is @@ -1031,12 +1045,6 @@ bool evp_md_is_valid(EVP_MD *md) { (md->from == EVP_SHA512 && md->size == 64)); } -/* Helper function for CBMC proofs: checks if EVP_MD_CTX is valid. */ -bool evp_md_ctx_is_valid(EVP_MD_CTX *ctx) { - return ctx && ctx->is_initialized && ctx->digest_size <= EVP_MAX_MD_SIZE && - (ctx->pkey == NULL || evp_pkey_is_valid(ctx->pkey)); -} - /* Helper function for CBMC proofs: allocates EVP_MD_CTX nondeterministically. */ EVP_MD_CTX *evp_md_ctx_nondet_alloc() { return can_fail_malloc(sizeof(EVP_MD_CTX)); diff --git a/verification/cbmc/sources/openssl/rand_override.c b/verification/cbmc/sources/openssl/rand_override.c index 7c6f01c04..5f26cd6b4 100644 --- a/verification/cbmc/sources/openssl/rand_override.c +++ b/verification/cbmc/sources/openssl/rand_override.c @@ -21,7 +21,9 @@ * An error occurs if the PRNG has not been seeded with enough randomness to ensure an unpredictable byte sequence. * RAND_bytes() returns 1 on success, 0 otherwise. */ -int RAND_bytes(unsigned char *buf, size_t num) { +int RAND_bytes(unsigned char *buf, int num) { + // https://github.com/openssl/openssl/blob/master/crypto/rand/rand_lib.c#L373 + if (num < 0) return 0; assert(AWS_MEM_IS_WRITABLE(buf, num)); int rv; __CPROVER_assume(rv == 0 || rv == 1); diff --git a/verification/cbmc/stubs/EVP_MD_CTX_free_no_pkey_stub.c b/verification/cbmc/stubs/EVP_MD_CTX_free_no_pkey_stub.c index c5888e3ae..e5c236373 100644 --- a/verification/cbmc/stubs/EVP_MD_CTX_free_no_pkey_stub.c +++ b/verification/cbmc/stubs/EVP_MD_CTX_free_no_pkey_stub.c @@ -13,6 +13,7 @@ * limitations under the License. */ +#include #include #include diff --git a/verification/cbmc/stubs/EVP_PKEY_free_no_ec_key_stub.c b/verification/cbmc/stubs/EVP_PKEY_free_no_ec_key_stub.c index d799b2f5b..7f4c99801 100644 --- a/verification/cbmc/stubs/EVP_PKEY_free_no_ec_key_stub.c +++ b/verification/cbmc/stubs/EVP_PKEY_free_no_ec_key_stub.c @@ -13,6 +13,7 @@ * limitations under the License. */ +#include #include #include diff --git a/verification/cbmc/stubs/evp_md_ctx_is_valid_no_pkey_stub.c b/verification/cbmc/stubs/evp_md_ctx_is_valid_no_pkey_stub.c index e8db65840..5c8d1dedb 100644 --- a/verification/cbmc/stubs/evp_md_ctx_is_valid_no_pkey_stub.c +++ b/verification/cbmc/stubs/evp_md_ctx_is_valid_no_pkey_stub.c @@ -15,6 +15,8 @@ #include +#include + /* * Checks whether EVP_MD_CTX is a valid object. * Use this stub when we are certain there is no pkey