From 4c43c2cfe48a16e7217e77be277fd94e42918c0b Mon Sep 17 00:00:00 2001 From: Tegan Brennan Date: Wed, 9 Dec 2020 08:41:51 -0800 Subject: [PATCH 01/17] Adds check in case byte_buf_init fails --- source/session_encrypt.c | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/source/session_encrypt.c b/source/session_encrypt.c index 5ec31016e..a5a35c5f6 100644 --- a/source/session_encrypt.c +++ b/source/session_encrypt.c @@ -89,7 +89,9 @@ int aws_cryptosdk_priv_try_gen_key(struct aws_cryptosdk_session *session) { // Generate message ID and derive the content key from the data key. size_t message_id_len = aws_cryptosdk_private_algorithm_message_id_len(session->alg_props); - aws_byte_buf_init(&session->header.message_id, session->alloc, message_id_len); + if (aws_byte_buf_init(&session->header.message_id, session->alloc, message_id_len) != AWS_OP_SUCCESS) { + goto out; + } if (aws_cryptosdk_genrandom(session->header.message_id.buffer, message_id_len)) { goto out; } From cd2615ffb57a82cf1d26c1c153643af03787e2ff Mon Sep 17 00:00:00 2001 From: Tegan Brennan Date: Wed, 9 Dec 2020 09:00:53 -0800 Subject: [PATCH 02/17] Adds harness, Makefile and yaml for priv_try_gen_key --- .../aws_cryptosdk_priv_try_gen_key/Makefile | 126 +++++++++ .../aws_cryptosdk_priv_try_gen_key_harness.c | 246 ++++++++++++++++++ .../cbmc-batch.yaml | 4 + 3 files changed, 376 insertions(+) create mode 100644 verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile create mode 100644 verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c create mode 100644 verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile new file mode 100644 index 000000000..18f7cbf7c --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile @@ -0,0 +1,126 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Licensed under the Apache License, Version 2.0 (the "License"). You may not use +# this file except in compliance with the License. A copy of the License is +# located at +# +# http://aws.amazon.com/apache2.0/ +# +# or in the "license" file accompanying this file. This file is distributed on an +# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or +# implied. See the License for the specific language governing permissions and +# limitations under the License. + +######### +# if Makefile.local exists, use it. This provides a way to override the defaults +sinclude ../Makefile.local +#otherwise, use the default values +include ../Makefile.local_default +include ../Makefile.string +include ../Makefile.aws_byte_buf + +######### +PROOF_UID = aws_cryptosdk_priv_try_gen_key +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(HARNESS_ENTRY).c + +# Increasing the length of the edk_list or enc_ctx does not improve coverage. +# Therefore, we choose these values for performance. +MAX_EDK_LIST_ITEMS ?= 1 +MAX_TABLE_SIZE ?= 2 +MAX_TRACE_NUM_ITEMS ?= 2 + +DEFINES += -DARRAY_LIST_TYPE="struct aws_cryptosdk_edk" +DEFINES += -DARRAY_LIST_TYPE_HEADER=\"aws/cryptosdk/edk.h\" +DEFINES += -DAWS_CRYPTOSDK_HASH_ELEMS_ARRAY_INIT_GENERATOR=array_list_item_generator +DEFINES += -DAWS_NO_STATIC_IMPL +DEFINES += -DMAX_EDK_LIST_ITEMS=$(MAX_EDK_LIST_ITEMS) +DEFINES += -DMAX_IV_LEN=$(MAX_IV_LEN) +DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) +DEFINES += -DMAX_TRACE_NUM_ITEMS=$(MAX_TRACE_NUM_ITEMS) + +# The maximum number of objects is set to 2^8 = 256. This option changes that to 2^9. +# Without this flag, running this proof causes the CBMC error of +# "too many addressed objects: maximum number of objects is set to 2^n=256 (with n=8); +# use the `--object-bits n` option to increase the maximum number" +CBMCFLAGS += --object-bits 9 + +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/hash_table.c +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/math.c +PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/array_list.c +PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/atomics.c +PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/byte_order.c +PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/error.c +PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/math.c +PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/string.c +PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/bn_override.c +PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/ec_override.c +PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/evp_override.c +PROJECT_SOURCES += $(PROOF_SOURCE)/openssl/rand_override.c +PROJECT_SOURCES += $(SRCDIR)/source/cipher.c +PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c +PROJECT_SOURCES += $(SRCDIR)/source/edk.c +PROJECT_SOURCES += $(SRCDIR)/source/enc_ctx.c +PROJECT_SOURCES += $(SRCDIR)/source/header.c +PROJECT_SOURCES += $(SRCDIR)/source/hkdf.c +PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c +PROJECT_SOURCES += $(SRCDIR)/source/list_utils.c +PROJECT_SOURCES += $(SRCDIR)/source/materials.c +PROJECT_SOURCES += $(SRCDIR)/source/session.c +PROJECT_SOURCES += $(SRCDIR)/source/session_encrypt.c +PROJECT_SOURCES += $(SRCDIR)/source/utils.c + +PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/make_common_data_structures.c +PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/proof_allocators.c +PROOF_SOURCES += $(COMMON_PROOF_SOURCE)/utils.c +PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_array_list_defined_type.c +PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_byte_buf_write_stub.c +PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_iter_overrides.c +PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c +PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c +PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcmp_override.c +PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c +PROOF_SOURCES += $(COMMON_PROOF_STUB)/memset_override_havoc.c +PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c +PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_sort_noop_stub.c +PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_enc_ctx_size_stub.c +PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_hash_elems_array_init_stub.c +PROOF_SOURCES += $(PROOF_STUB)/aws_default_allocator_stub.c +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) + +REMOVE_FUNCTION_BODY += aws_array_list_get_at_ptr + +# Remove function bodies to deal with CBMC function pointer removal +# All functions removed are those removed in aws_cryptosdk_enc_ctx_serialize +REMOVE_FUNCTION_BODIES += --remove-function-body aws_array_list_sort +REMOVE_FUNCTION_BODIES += --remove-function-body aws_byte_buf_write +REMOVE_FUNCTION_BODIES += --remove-function-body aws_cryptosdk_enc_ctx_size +REMOVE_FUNCTION_BODIES += --remove-function-body aws_cryptosdk_hash_elems_array_init + +# We abstract these functions because manual inspection demonstrates that they are unreachable, +# which leads to improvements in coverage metrics +# All functions removed in aws_cryptosdk_sign_header +REMOVE_FUNCTION_BODY += EVP_DecryptUpdate +REMOVE_FUNCTION_BODY += EVP_sha256 +REMOVE_FUNCTION_BODY += EVP_sha384 +REMOVE_FUNCTION_BODY += EVP_sha512 + +UNWINDSET += array_list_item_generator.0:$(shell echo $$((1 + $(MAX_TABLE_SIZE)))) +UNWINDSET += aws_cryptosdk_edk_list_clear.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) +UNWINDSET += aws_cryptosdk_edk_list_elements_are_bounded.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) +UNWINDSET += aws_cryptosdk_edk_list_elements_are_valid.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) +UNWINDSET += aws_cryptosdk_enc_ctx_serialize.0:$(shell echo $$((1 + $(MAX_TABLE_SIZE)))) +UNWINDSET += aws_cryptosdk_hdr_size.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) +UNWINDSET += aws_cryptosdk_hdr_write.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) +UNWINDSET += aws_cryptosdk_keyring_trace_clear.0:$(call addone,$(MAX_TRACE_NUM_ITEMS)) +UNWINDSET += aws_cryptosdk_keyring_trace_is_valid.0:$(call addone,$(MAX_TRACE_NUM_ITEMS)) +UNWINDSET += aws_cryptosdk_transfer_list.4.0:$(call addone,$(MAX_TRACE_NUM_ITEMS)) +UNWINDSET += ensure_cryptosdk_edk_list_has_allocated_list_elements.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) +UNWINDSET += ensure_trace_has_allocated_records.0:$(call addone,$(MAX_TRACE_NUM_ITEMS)) +UNWINDSET += memcmp.0:$(call addone,$(MAX_BUFFER_SIZE)) + +########### +include ../Makefile.common diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c new file mode 100644 index 000000000..d2ee3e489 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c @@ -0,0 +1,246 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). You may not + * use + * this file except in compliance with the License. A copy of the License is + * located at + * + * http://aws.amazon.com/apache2.0/ + * + * or in the "license" file accompanying this file. This file is distributed on + * an + * "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express + * or + * implied. See the License for the specific language governing permissions and + * limitations under the License. + */ + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include +#include +#include +#include + +/* Stub this for performance but check the preconditions. + No modified data structure is used again. + Original function is here: + https://github.com/aws/aws-encryption-sdk-c/blob/master/source/hkdf.c#148 */ +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) { + assert(aws_byte_buf_is_valid(salt)); + assert(aws_byte_buf_is_valid(ikm)); + assert(aws_byte_buf_is_valid(info)); + if (nondet_bool()) { + return AWS_OP_ERR; + } + return AWS_OP_SUCCESS; +} + +/* Stub this because of the override of aws_array_list_get_at_ptr and for performance. + The contents of session_>keyring_trace are nondet in the construction of the harness. + Also neither keyring trace is later used. + Original function is here: + https://github.com/aws/aws-encryption-sdk-c/blob/master/source/list_utils.c#L17 */ +int aws_cryptosdk_transfer_list(struct aws_array_list *dest, struct aws_array_list *src) { + assert(src != dest); + assert(aws_array_list_is_valid(dest)); + assert(aws_array_list_is_valid(src)); + assert(dest->item_size == src->item_size); + + if (nondet_bool()) { + return AWS_OP_ERR; + } + return AWS_OP_SUCCESS; +} + +void array_list_item_generator(struct aws_array_list *elems) { + assert(elems->item_size == sizeof(struct aws_hash_element)); + for (size_t index = 0; index < elems->length; ++index) { + struct aws_hash_element *val = (struct aws_hash_element *)((uint8_t *)elems->data + (elems->item_size * index)); + /* Due to the cast to uint16, the entire size of the enc_ctx must be less than < UINT16_MAX + * This is a simple way to ensure this without a call to enc_ctx_size. */ + struct aws_string *key = ensure_string_is_allocated_nondet_length(); + __CPROVER_assume(aws_string_is_valid(key)); + __CPROVER_assume(key->len <= UINT8_MAX); + val->key = key; + struct aws_string *value = ensure_string_is_allocated_nondet_length(); + __CPROVER_assume(aws_string_is_valid(value)); + __CPROVER_assume(value->len <= UINT8_MAX); + val->value = value; + } +} + +/* Stub this because of the override of aws_array_list_get_at_ptr + Original function is here: + https://github.com/aws/aws-encryption-sdk-c/blob/master/source/keyring_trace.c#L235 */ +void aws_cryptosdk_keyring_trace_clear(struct aws_array_list *trace) { + AWS_FATAL_PRECONDITION(aws_cryptosdk_keyring_trace_is_valid(trace)); + AWS_FATAL_PRECONDITION(trace->item_size == sizeof(struct aws_cryptosdk_keyring_trace_record)); + aws_array_list_clear(trace); +} + +/* Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed + Original function is here: + https://github.com/aws/aws-encryption-sdk-c/blob/master/source/edk.c#L44 */ +void aws_cryptosdk_edk_list_clean_up(struct aws_array_list *encrypted_data_keys) { + assert(aws_cryptosdk_edk_list_is_valid(encrypted_data_keys)); + aws_array_list_clean_up(encrypted_data_keys); +} + +/** + * Receives encryption request from user and attempts to generate encryption materials, + * including an encrypted data key and a list of EDKs for doing encryption. + * + * On success returns AWS_OP_SUCCESS and allocates encryption materials object at address + * pointed to by output. + * + * On failure returns AWS_OP_ERR, sets address pointed to by output to NULL, and sets + * internal AWS error code. + */ +int generate_enc_materials( + struct aws_cryptosdk_cmm *cmm, + struct aws_cryptosdk_enc_materials **output, + struct aws_cryptosdk_enc_request *request) { + assert(aws_cryptosdk_cmm_base_is_valid(cmm)); + assert(AWS_OBJECT_PTR_IS_WRITABLE(output)); + assert(aws_cryptosdk_enc_request_is_valid(request)); + + struct aws_cryptosdk_enc_materials *materials = malloc(sizeof(*materials)); + if (materials == NULL) { + *output = NULL; + return AWS_OP_ERR; + } + + // Set up the allocator + // Request->alloc is session->alloc + materials->alloc = request->alloc; + __CPROVER_assume(aws_allocator_is_valid(materials->alloc)); + __CPROVER_assume(materials->alloc != NULL); + + // Set up the signctx + materials->signctx = ensure_nondet_sig_ctx_has_allocated_members(); + __CPROVER_assume(aws_cryptosdk_sig_ctx_is_valid_cbmc(materials->signctx)); + + // Set up the unencrypted_data_key + __CPROVER_assume(aws_byte_buf_is_bounded(&materials->unencrypted_data_key, MAX_BUFFER_SIZE)); + ensure_byte_buf_has_allocated_buffer_member(&materials->unencrypted_data_key); + __CPROVER_assume(aws_byte_buf_is_valid(&materials->unencrypted_data_key)); + + // Set up the edk_list + // edk_list Precondition: We have a valid list */ + __CPROVER_assume(aws_cryptosdk_edk_list_is_bounded(&materials->encrypted_data_keys, MAX_EDK_LIST_ITEMS)); + ensure_cryptosdk_edk_list_has_allocated_list(&materials->encrypted_data_keys); + __CPROVER_assume(aws_cryptosdk_edk_list_is_valid(&materials->encrypted_data_keys)); + + // The alloc is session->alloc + materials->encrypted_data_keys.alloc = request->alloc; + + // edk_list Precondition: The list has valid list elements + __CPROVER_assume(aws_cryptosdk_edk_list_elements_are_bounded(&materials->encrypted_data_keys, MAX_BUFFER_SIZE)); + ensure_cryptosdk_edk_list_has_allocated_list_elements(&materials->encrypted_data_keys); + __CPROVER_assume(aws_cryptosdk_edk_list_elements_are_valid(&materials->encrypted_data_keys)); + + // Set up the keyring trace + __CPROVER_assume(aws_array_list_is_bounded( + &materials->keyring_trace, MAX_TRACE_NUM_ITEMS, sizeof(struct aws_cryptosdk_keyring_trace_record))); + __CPROVER_assume(materials->keyring_trace.item_size == sizeof(struct aws_cryptosdk_keyring_trace_record)); + ensure_array_list_has_allocated_data_member(&materials->keyring_trace); + __CPROVER_assume(aws_array_list_is_valid(&materials->keyring_trace)); + ensure_trace_has_allocated_records(&materials->keyring_trace, MAX_STRING_LEN); + __CPROVER_assume(aws_cryptosdk_keyring_trace_is_valid(&materials->keyring_trace)); + + // Set the alg_id + enum aws_cryptosdk_alg_id alg_id; + materials->alg = alg_id; + + *output = materials; + return AWS_OP_SUCCESS; +} + +void aws_cryptosdk_priv_try_gen_key_harness() { + /* Nondet Input */ + struct aws_cryptosdk_session *session = malloc(sizeof(*session)); + + /* Assumptions */ + __CPROVER_assume(session != NULL); + + const struct aws_cryptosdk_cmm_vt vtable = { .vt_size = sizeof(struct aws_cryptosdk_cmm_vt), + .name = ensure_c_str_is_allocated(SIZE_MAX), + .destroy = nondet_voidp(), + .generate_enc_materials = + nondet_bool() ? generate_enc_materials : NULL, + .decrypt_materials = nondet_voidp() }; + __CPROVER_assume(aws_cryptosdk_cmm_vtable_is_valid(&vtable)); + + struct aws_cryptosdk_cmm *cmm = malloc(sizeof(*cmm)); + __CPROVER_assume(cmm); + cmm->vtable = &vtable; + __CPROVER_assume(aws_cryptosdk_cmm_base_is_valid(cmm)); + session->cmm = cmm; + + enum aws_cryptosdk_alg_id alg_id; + struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg_id); + __CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(props)); + session->alg_props = props; + + struct aws_cryptosdk_hdr *hdr = ensure_nondet_hdr_has_allocated_members(MAX_TABLE_SIZE); + + __CPROVER_assume(aws_cryptosdk_hdr_members_are_bounded(hdr, MAX_EDK_LIST_ITEMS, MAX_BUFFER_SIZE)); + + __CPROVER_assume(IMPLIES(hdr != NULL, aws_byte_buf_is_bounded(&hdr->iv, session->alg_props->iv_len))); + __CPROVER_assume(IMPLIES(hdr != NULL, aws_byte_buf_is_bounded(&hdr->auth_tag, session->alg_props->tag_len))); + + ensure_cryptosdk_edk_list_has_allocated_list_elements(&hdr->edk_list); + + __CPROVER_assume(aws_cryptosdk_hdr_is_valid(hdr)); + + // The header should have been cleared earlier + __CPROVER_assume(aws_array_list_length(&hdr->edk_list) == 0); + + __CPROVER_assume(hdr->enc_ctx.p_impl != NULL); + ensure_hash_table_has_valid_destroy_functions(&hdr->enc_ctx); + size_t empty_slot_idx; + __CPROVER_assume(aws_hash_table_has_an_empty_slot(&hdr->enc_ctx, &empty_slot_idx)); + session->header = *hdr; + + struct aws_array_list *keyring_trace = malloc(sizeof(*keyring_trace)); + __CPROVER_assume(keyring_trace != NULL); + __CPROVER_assume(aws_array_list_is_bounded( + keyring_trace, MAX_TRACE_NUM_ITEMS, sizeof(struct aws_cryptosdk_keyring_trace_record))); + __CPROVER_assume(keyring_trace->item_size == sizeof(struct aws_cryptosdk_keyring_trace_record)); + ensure_array_list_has_allocated_data_member(keyring_trace); + __CPROVER_assume(aws_array_list_is_valid(keyring_trace)); + ensure_trace_has_allocated_records(keyring_trace, MAX_STRING_LEN); + __CPROVER_assume(aws_cryptosdk_keyring_trace_is_valid(keyring_trace)); + session->keyring_trace = *keyring_trace; + + session->alloc = can_fail_allocator(); + __CPROVER_assume(aws_allocator_is_valid(session->alloc)); + __CPROVER_assume(session->alloc != NULL); + session->header.edk_list.alloc = session->alloc; // this assumption is needed for build_header + __CPROVER_assume(aws_cryptosdk_commitment_policy_is_valid(session->commitment_policy)); + + __CPROVER_assume(session->state == ST_GEN_KEY); + __CPROVER_assume(session->mode == AWS_CRYPTOSDK_ENCRYPT); + + struct content_key *content_key = malloc(sizeof(*content_key)); + __CPROVER_assume(content_key != NULL); + session->content_key = *content_key; + + /* Function under verification */ + aws_cryptosdk_priv_try_gen_key(session); +} diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml new file mode 100644 index 000000000..0dfb4c18a --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml @@ -0,0 +1,4 @@ +cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8" +expected: "SUCCESSFUL" +goto: aws_cryptosdk_cmm_generate_enc_materials_harness.goto +jobos: ubuntu16 From c6fd20a6e32e6a5a90c6eec04ccb2ac2e271b463 Mon Sep 17 00:00:00 2001 From: Tegan Brennan Date: Fri, 18 Dec 2020 11:15:06 -0800 Subject: [PATCH 03/17] Adds preconditions to source code --- source/session_encrypt.c | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/source/session_encrypt.c b/source/session_encrypt.c index a5a35c5f6..141380f88 100644 --- a/source/session_encrypt.c +++ b/source/session_encrypt.c @@ -48,6 +48,15 @@ void aws_cryptosdk_priv_encrypt_compute_body_estimate(struct aws_cryptosdk_sessi } int aws_cryptosdk_priv_try_gen_key(struct aws_cryptosdk_session *session) { + AWS_PRECONDITION(session != NULL); + AWS_PRECONDITION(aws_cryptosdk_cmm_base_is_valid(session->cmm)); + AWS_PRECONDITION(aws_cryptosdk_alg_properties_is_valid(session->alg_props)); + AWS_PRECONDITION(aws_cryptosdk_hdr_is_valid(&session->header)); + AWS_PRECONDITION(aws_cryptosdk_keyring_trace_is_valid(&session->keyring_trace)); + AWS_PRECONDITION(aws_allocator_is_valid(session->alloc)); + AWS_PRECONDITION(aws_cryptosdk_commitment_policy_is_valid(session->commitment_policy)); + AWS_PRECONDITION(session->state == ST_GEN_KEY); + AWS_PRECONDITION(session->mode == AWS_CRYPTOSDK_ENCRYPT); struct aws_cryptosdk_enc_request request; struct aws_cryptosdk_enc_materials *materials = NULL; struct data_key data_key; From 6ad0f6e3a23053a97bd25424ea79fd85651d3c47 Mon Sep 17 00:00:00 2001 From: Tegan Brennan Date: Fri, 18 Dec 2020 11:15:24 -0800 Subject: [PATCH 04/17] Update to harness --- .../aws_cryptosdk_priv_try_gen_key_harness.c | 48 +++++++++---------- 1 file changed, 23 insertions(+), 25 deletions(-) diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c index d2ee3e489..7ba1ad17f 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c @@ -51,7 +51,7 @@ int aws_cryptosdk_hkdf( } /* Stub this because of the override of aws_array_list_get_at_ptr and for performance. - The contents of session_>keyring_trace are nondet in the construction of the harness. + The contents of session->keyring_trace are nondet in the construction of the harness. Also neither keyring trace is later used. Original function is here: https://github.com/aws/aws-encryption-sdk-c/blob/master/source/list_utils.c#L17 */ @@ -141,7 +141,6 @@ int generate_enc_materials( __CPROVER_assume(aws_byte_buf_is_valid(&materials->unencrypted_data_key)); // Set up the edk_list - // edk_list Precondition: We have a valid list */ __CPROVER_assume(aws_cryptosdk_edk_list_is_bounded(&materials->encrypted_data_keys, MAX_EDK_LIST_ITEMS)); ensure_cryptosdk_edk_list_has_allocated_list(&materials->encrypted_data_keys); __CPROVER_assume(aws_cryptosdk_edk_list_is_valid(&materials->encrypted_data_keys)); @@ -149,7 +148,7 @@ int generate_enc_materials( // The alloc is session->alloc materials->encrypted_data_keys.alloc = request->alloc; - // edk_list Precondition: The list has valid list elements + // Precondition: The edk_list has valid list elements __CPROVER_assume(aws_cryptosdk_edk_list_elements_are_bounded(&materials->encrypted_data_keys, MAX_BUFFER_SIZE)); ensure_cryptosdk_edk_list_has_allocated_list_elements(&materials->encrypted_data_keys); __CPROVER_assume(aws_cryptosdk_edk_list_elements_are_valid(&materials->encrypted_data_keys)); @@ -178,6 +177,7 @@ void aws_cryptosdk_priv_try_gen_key_harness() { /* Assumptions */ __CPROVER_assume(session != NULL); + /* Set the session->cmm */ const struct aws_cryptosdk_cmm_vt vtable = { .vt_size = sizeof(struct aws_cryptosdk_cmm_vt), .name = ensure_c_str_is_allocated(SIZE_MAX), .destroy = nondet_voidp(), @@ -192,31 +192,25 @@ void aws_cryptosdk_priv_try_gen_key_harness() { __CPROVER_assume(aws_cryptosdk_cmm_base_is_valid(cmm)); session->cmm = cmm; + /* Set the session->alg_id */ enum aws_cryptosdk_alg_id alg_id; struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg_id); __CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(props)); session->alg_props = props; - struct aws_cryptosdk_hdr *hdr = ensure_nondet_hdr_has_allocated_members(MAX_TABLE_SIZE); + /* Set the session->header */ + struct aws_cryptosdk_hdr *hdr = hdr_setup(MAX_TABLE_SIZE, MAX_EDK_LIST_ITEMS, MAX_BUFFER_SIZE); - __CPROVER_assume(aws_cryptosdk_hdr_members_are_bounded(hdr, MAX_EDK_LIST_ITEMS, MAX_BUFFER_SIZE)); + __CPROVER_assume(aws_byte_buf_is_bounded(&hdr->iv, session->alg_props->iv_len)); + __CPROVER_assume(aws_byte_buf_is_bounded(&hdr->auth_tag, session->alg_props->tag_len)); - __CPROVER_assume(IMPLIES(hdr != NULL, aws_byte_buf_is_bounded(&hdr->iv, session->alg_props->iv_len))); - __CPROVER_assume(IMPLIES(hdr != NULL, aws_byte_buf_is_bounded(&hdr->auth_tag, session->alg_props->tag_len))); - - ensure_cryptosdk_edk_list_has_allocated_list_elements(&hdr->edk_list); - - __CPROVER_assume(aws_cryptosdk_hdr_is_valid(hdr)); - - // The header should have been cleared earlier + /* The header edk_list should have been cleared earlier. + See comment in build_header: "The header should have been cleared earlier, so the materials structure + should have zero EDKs (otherwise we'd need to destroy the old EDKs as well). */ __CPROVER_assume(aws_array_list_length(&hdr->edk_list) == 0); - - __CPROVER_assume(hdr->enc_ctx.p_impl != NULL); - ensure_hash_table_has_valid_destroy_functions(&hdr->enc_ctx); - size_t empty_slot_idx; - __CPROVER_assume(aws_hash_table_has_an_empty_slot(&hdr->enc_ctx, &empty_slot_idx)); session->header = *hdr; + /* Set the session->keyring_trace */ struct aws_array_list *keyring_trace = malloc(sizeof(*keyring_trace)); __CPROVER_assume(keyring_trace != NULL); __CPROVER_assume(aws_array_list_is_bounded( @@ -228,19 +222,23 @@ void aws_cryptosdk_priv_try_gen_key_harness() { __CPROVER_assume(aws_cryptosdk_keyring_trace_is_valid(keyring_trace)); session->keyring_trace = *keyring_trace; + /* Set the allocators */ session->alloc = can_fail_allocator(); __CPROVER_assume(aws_allocator_is_valid(session->alloc)); - __CPROVER_assume(session->alloc != NULL); - session->header.edk_list.alloc = session->alloc; // this assumption is needed for build_header - __CPROVER_assume(aws_cryptosdk_commitment_policy_is_valid(session->commitment_policy)); + session->header.edk_list.alloc = session->alloc; // This assumption is needed for build_header + __CPROVER_assume(aws_cryptosdk_commitment_policy_is_valid(session->commitment_policy)); __CPROVER_assume(session->state == ST_GEN_KEY); __CPROVER_assume(session->mode == AWS_CRYPTOSDK_ENCRYPT); - struct content_key *content_key = malloc(sizeof(*content_key)); - __CPROVER_assume(content_key != NULL); - session->content_key = *content_key; + /* Save current state of the data structure */ + struct store_byte_from_buffer old_enc_ctx; + save_byte_from_hash_table(&session->header.enc_ctx, &old_enc_ctx); /* Function under verification */ - aws_cryptosdk_priv_try_gen_key(session); + if (aws_cryptosdk_priv_try_gen_key(session) == AWS_OP_SUCCESS) { + /* Assertions */ + assert(aws_cryptosdk_hdr_is_valid(&session->header)); + } + check_hash_table_unchanged(&session->header.enc_ctx, &old_enc_ctx); } From 161f58a99a6f713d4b9fc0de0b07089ecaf2111c Mon Sep 17 00:00:00 2001 From: Tegan Brennan Date: Sat, 19 Dec 2020 14:36:44 -0800 Subject: [PATCH 05/17] yaml update to boiler plate default --- .../proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml index 0dfb4c18a..e936b4599 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml @@ -1,4 +1,4 @@ -cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8" -expected: "SUCCESSFUL" -goto: aws_cryptosdk_cmm_generate_enc_materials_harness.goto -jobos: ubuntu16 +: + This file marks this directory as containing a CBMC proof. This file + is automatically clobbered in CI and replaced with parameters for + running the proof. \ No newline at end of file From c6267140761e3d26f3a63deb966593b043d387a8 Mon Sep 17 00:00:00 2001 From: Tegan Brennan Date: Sat, 19 Dec 2020 14:37:48 -0800 Subject: [PATCH 06/17] Remove unneccessary remove functions --- .../cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile | 7 ------- 1 file changed, 7 deletions(-) diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile index 18f7cbf7c..86588ad9b 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile @@ -93,13 +93,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) REMOVE_FUNCTION_BODY += aws_array_list_get_at_ptr -# Remove function bodies to deal with CBMC function pointer removal -# All functions removed are those removed in aws_cryptosdk_enc_ctx_serialize -REMOVE_FUNCTION_BODIES += --remove-function-body aws_array_list_sort -REMOVE_FUNCTION_BODIES += --remove-function-body aws_byte_buf_write -REMOVE_FUNCTION_BODIES += --remove-function-body aws_cryptosdk_enc_ctx_size -REMOVE_FUNCTION_BODIES += --remove-function-body aws_cryptosdk_hash_elems_array_init - # We abstract these functions because manual inspection demonstrates that they are unreachable, # which leads to improvements in coverage metrics # All functions removed in aws_cryptosdk_sign_header From abf4725007cd7efe92524f9d51f81084a438ea70 Mon Sep 17 00:00:00 2001 From: Tegan Brennan Date: Sun, 20 Dec 2020 23:45:23 -0800 Subject: [PATCH 07/17] Added preconditions of lne of byte bufs --- source/session_encrypt.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/source/session_encrypt.c b/source/session_encrypt.c index 141380f88..84f822fb2 100644 --- a/source/session_encrypt.c +++ b/source/session_encrypt.c @@ -52,6 +52,8 @@ int aws_cryptosdk_priv_try_gen_key(struct aws_cryptosdk_session *session) { AWS_PRECONDITION(aws_cryptosdk_cmm_base_is_valid(session->cmm)); AWS_PRECONDITION(aws_cryptosdk_alg_properties_is_valid(session->alg_props)); AWS_PRECONDITION(aws_cryptosdk_hdr_is_valid(&session->header)); + AWS_PRECONDITION(session->header.iv.len <= session->alg_props->iv_len); + AWS_PRECONDITION(session->header.auth_tag.len <= session->alg_props->tag_len); AWS_PRECONDITION(aws_cryptosdk_keyring_trace_is_valid(&session->keyring_trace)); AWS_PRECONDITION(aws_allocator_is_valid(session->alloc)); AWS_PRECONDITION(aws_cryptosdk_commitment_policy_is_valid(session->commitment_policy)); From 2340de6724ef206cb247a59b1a94348621cb1e1e Mon Sep 17 00:00:00 2001 From: Tegan Brennan Date: Mon, 21 Dec 2020 13:01:14 -0800 Subject: [PATCH 08/17] Use CBMC_OBJECT_BITS = 9 flag --- .../cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile index 86588ad9b..8925e3111 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile @@ -43,7 +43,9 @@ DEFINES += -DMAX_TRACE_NUM_ITEMS=$(MAX_TRACE_NUM_ITEMS) # Without this flag, running this proof causes the CBMC error of # "too many addressed objects: maximum number of objects is set to 2^n=256 (with n=8); # use the `--object-bits n` option to increase the maximum number" -CBMCFLAGS += --object-bits 9 +# The proof hits the error when the line "rv = aws_cryptosdk_hdr_write(&session->header, +# &actual_size, session->header_copy, session->header_size);" is reached. +CBMC_OBJECT_BITS = 9 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c From ca326d39ac4ba13f38afd2b8ed5dd9847800d78a Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 12 Jan 2021 19:29:56 +0000 Subject: [PATCH 09/17] Use session setup and validator functions --- source/session_encrypt.c | 7 +------ .../proofs/aws_cryptosdk_priv_try_gen_key/Makefile | 12 ++++++------ .../aws_cryptosdk_priv_try_gen_key_harness.c | 7 ++++--- 3 files changed, 11 insertions(+), 15 deletions(-) diff --git a/source/session_encrypt.c b/source/session_encrypt.c index 84f822fb2..6b2692965 100644 --- a/source/session_encrypt.c +++ b/source/session_encrypt.c @@ -48,14 +48,9 @@ void aws_cryptosdk_priv_encrypt_compute_body_estimate(struct aws_cryptosdk_sessi } int aws_cryptosdk_priv_try_gen_key(struct aws_cryptosdk_session *session) { - AWS_PRECONDITION(session != NULL); - AWS_PRECONDITION(aws_cryptosdk_cmm_base_is_valid(session->cmm)); - AWS_PRECONDITION(aws_cryptosdk_alg_properties_is_valid(session->alg_props)); - AWS_PRECONDITION(aws_cryptosdk_hdr_is_valid(&session->header)); + AWS_PRECONDITION(aws_cryptosdk_session_is_valid(session)); AWS_PRECONDITION(session->header.iv.len <= session->alg_props->iv_len); AWS_PRECONDITION(session->header.auth_tag.len <= session->alg_props->tag_len); - AWS_PRECONDITION(aws_cryptosdk_keyring_trace_is_valid(&session->keyring_trace)); - AWS_PRECONDITION(aws_allocator_is_valid(session->alloc)); AWS_PRECONDITION(aws_cryptosdk_commitment_policy_is_valid(session->commitment_policy)); AWS_PRECONDITION(session->state == ST_GEN_KEY); AWS_PRECONDITION(session->mode == AWS_CRYPTOSDK_ENCRYPT); diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile index 8925e3111..5c7aa6698 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile @@ -28,7 +28,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c # Therefore, we choose these values for performance. MAX_EDK_LIST_ITEMS ?= 1 MAX_TABLE_SIZE ?= 2 -MAX_TRACE_NUM_ITEMS ?= 2 +MAX_TRACE_LIST_ITEMS ?= 2 DEFINES += -DARRAY_LIST_TYPE="struct aws_cryptosdk_edk" DEFINES += -DARRAY_LIST_TYPE_HEADER=\"aws/cryptosdk/edk.h\" @@ -37,7 +37,7 @@ DEFINES += -DAWS_NO_STATIC_IMPL DEFINES += -DMAX_EDK_LIST_ITEMS=$(MAX_EDK_LIST_ITEMS) DEFINES += -DMAX_IV_LEN=$(MAX_IV_LEN) DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) -DEFINES += -DMAX_TRACE_NUM_ITEMS=$(MAX_TRACE_NUM_ITEMS) +DEFINES += -DMAX_TRACE_LIST_ITEMS=$(MAX_TRACE_LIST_ITEMS) # The maximum number of objects is set to 2^8 = 256. This option changes that to 2^9. # Without this flag, running this proof causes the CBMC error of @@ -110,11 +110,11 @@ UNWINDSET += aws_cryptosdk_edk_list_elements_are_valid.0:$(call addone,$(MAX_EDK UNWINDSET += aws_cryptosdk_enc_ctx_serialize.0:$(shell echo $$((1 + $(MAX_TABLE_SIZE)))) UNWINDSET += aws_cryptosdk_hdr_size.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) UNWINDSET += aws_cryptosdk_hdr_write.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) -UNWINDSET += aws_cryptosdk_keyring_trace_clear.0:$(call addone,$(MAX_TRACE_NUM_ITEMS)) -UNWINDSET += aws_cryptosdk_keyring_trace_is_valid.0:$(call addone,$(MAX_TRACE_NUM_ITEMS)) -UNWINDSET += aws_cryptosdk_transfer_list.4.0:$(call addone,$(MAX_TRACE_NUM_ITEMS)) +UNWINDSET += aws_cryptosdk_keyring_trace_clear.0:$(call addone,$(MAX_TRACE_LIST_ITEMS)) +UNWINDSET += aws_cryptosdk_keyring_trace_is_valid.0:$(call addone,$(MAX_TRACE_LIST_ITEMS)) +UNWINDSET += aws_cryptosdk_transfer_list.4.0:$(call addone,$(MAX_TRACE_LIST_ITEMS)) UNWINDSET += ensure_cryptosdk_edk_list_has_allocated_list_elements.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) -UNWINDSET += ensure_trace_has_allocated_records.0:$(call addone,$(MAX_TRACE_NUM_ITEMS)) +UNWINDSET += ensure_trace_has_allocated_records.0:$(call addone,$(MAX_TRACE_LIST_ITEMS)) UNWINDSET += memcmp.0:$(call addone,$(MAX_BUFFER_SIZE)) ########### diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c index 7ba1ad17f..e7f9ead82 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c @@ -155,7 +155,7 @@ int generate_enc_materials( // Set up the keyring trace __CPROVER_assume(aws_array_list_is_bounded( - &materials->keyring_trace, MAX_TRACE_NUM_ITEMS, sizeof(struct aws_cryptosdk_keyring_trace_record))); + &materials->keyring_trace, MAX_TRACE_LIST_ITEMS, sizeof(struct aws_cryptosdk_keyring_trace_record))); __CPROVER_assume(materials->keyring_trace.item_size == sizeof(struct aws_cryptosdk_keyring_trace_record)); ensure_array_list_has_allocated_data_member(&materials->keyring_trace); __CPROVER_assume(aws_array_list_is_valid(&materials->keyring_trace)); @@ -172,7 +172,8 @@ int generate_enc_materials( void aws_cryptosdk_priv_try_gen_key_harness() { /* Nondet Input */ - struct aws_cryptosdk_session *session = malloc(sizeof(*session)); + struct aws_cryptosdk_session *session = + session_setup(MAX_TABLE_SIZE, MAX_TRACE_LIST_ITEMS, MAX_EDK_LIST_ITEMS, MAX_BUFFER_SIZE, MAX_STRING_LEN); /* Assumptions */ __CPROVER_assume(session != NULL); @@ -214,7 +215,7 @@ void aws_cryptosdk_priv_try_gen_key_harness() { struct aws_array_list *keyring_trace = malloc(sizeof(*keyring_trace)); __CPROVER_assume(keyring_trace != NULL); __CPROVER_assume(aws_array_list_is_bounded( - keyring_trace, MAX_TRACE_NUM_ITEMS, sizeof(struct aws_cryptosdk_keyring_trace_record))); + keyring_trace, MAX_TRACE_LIST_ITEMS, sizeof(struct aws_cryptosdk_keyring_trace_record))); __CPROVER_assume(keyring_trace->item_size == sizeof(struct aws_cryptosdk_keyring_trace_record)); ensure_array_list_has_allocated_data_member(keyring_trace); __CPROVER_assume(aws_array_list_is_valid(keyring_trace)); From 284934df6639fdf1f3e00deea0c70b605681af2f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 14 Jan 2021 17:32:42 +0000 Subject: [PATCH 10/17] Move stubs in harness to stubs folder --- .../aws_cryptosdk_priv_try_gen_key/Makefile | 11 +- .../aws_cryptosdk_priv_try_gen_key_harness.c | 141 +----------------- .../aws_array_list_item_generator_u8_stub.c | 38 +++++ .../cbmc/stubs/generate_enc_materials_stub.c | 89 +++++++++++ verification/cbmc/stubs/hkdf_stub.c | 37 +++++ .../cbmc/stubs/keyring_trace_clean_up_stub.c | 26 ++++ .../cbmc/stubs/keyring_trace_clear_stub.c | 27 ++++ verification/cbmc/stubs/transfer_list_stub.c | 35 +++++ 8 files changed, 262 insertions(+), 142 deletions(-) create mode 100644 verification/cbmc/stubs/aws_array_list_item_generator_u8_stub.c create mode 100644 verification/cbmc/stubs/generate_enc_materials_stub.c create mode 100644 verification/cbmc/stubs/hkdf_stub.c create mode 100644 verification/cbmc/stubs/keyring_trace_clean_up_stub.c create mode 100644 verification/cbmc/stubs/keyring_trace_clear_stub.c create mode 100644 verification/cbmc/stubs/transfer_list_stub.c diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile index 5c7aa6698..be68da02e 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile @@ -87,14 +87,19 @@ PROOF_SOURCES += $(COMMON_PROOF_STUB)/memcpy_override_havoc.c PROOF_SOURCES += $(COMMON_PROOF_STUB)/memset_override_havoc.c PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c +PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_item_generator_u8_stub.c PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_sort_noop_stub.c PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_enc_ctx_size_stub.c PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_hash_elems_array_init_stub.c PROOF_SOURCES += $(PROOF_STUB)/aws_default_allocator_stub.c +PROOF_SOURCES += $(PROOF_STUB)/generate_enc_materials_stub.c +PROOF_SOURCES += $(PROOF_STUB)/hdr_write_stub.c +PROOF_SOURCES += $(PROOF_STUB)/hkdf_stub.c +PROOF_SOURCES += $(PROOF_STUB)/keyring_trace_clean_up_stub.c +PROOF_SOURCES += $(PROOF_STUB)/keyring_trace_clear_stub.c +PROOF_SOURCES += $(PROOF_STUB)/transfer_list_stub.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) -REMOVE_FUNCTION_BODY += aws_array_list_get_at_ptr - # We abstract these functions because manual inspection demonstrates that they are unreachable, # which leads to improvements in coverage metrics # All functions removed in aws_cryptosdk_sign_header @@ -102,6 +107,7 @@ REMOVE_FUNCTION_BODY += EVP_DecryptUpdate REMOVE_FUNCTION_BODY += EVP_sha256 REMOVE_FUNCTION_BODY += EVP_sha384 REMOVE_FUNCTION_BODY += EVP_sha512 +REMOVE_FUNCTION_BODY += aws_array_list_get_at_ptr UNWINDSET += array_list_item_generator.0:$(shell echo $$((1 + $(MAX_TABLE_SIZE)))) UNWINDSET += aws_cryptosdk_edk_list_clear.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) @@ -109,7 +115,6 @@ UNWINDSET += aws_cryptosdk_edk_list_elements_are_bounded.0:$(call addone,$(MAX_E UNWINDSET += aws_cryptosdk_edk_list_elements_are_valid.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) UNWINDSET += aws_cryptosdk_enc_ctx_serialize.0:$(shell echo $$((1 + $(MAX_TABLE_SIZE)))) UNWINDSET += aws_cryptosdk_hdr_size.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) -UNWINDSET += aws_cryptosdk_hdr_write.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) UNWINDSET += aws_cryptosdk_keyring_trace_clear.0:$(call addone,$(MAX_TRACE_LIST_ITEMS)) UNWINDSET += aws_cryptosdk_keyring_trace_is_valid.0:$(call addone,$(MAX_TRACE_LIST_ITEMS)) UNWINDSET += aws_cryptosdk_transfer_list.4.0:$(call addone,$(MAX_TRACE_LIST_ITEMS)) diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c index e7f9ead82..c9e4a9c01 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c @@ -17,7 +17,6 @@ */ #include -#include #include #include #include @@ -27,153 +26,17 @@ #include #include -#include #include #include -/* Stub this for performance but check the preconditions. - No modified data structure is used again. - Original function is here: - https://github.com/aws/aws-encryption-sdk-c/blob/master/source/hkdf.c#148 */ -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) { - assert(aws_byte_buf_is_valid(salt)); - assert(aws_byte_buf_is_valid(ikm)); - assert(aws_byte_buf_is_valid(info)); - if (nondet_bool()) { - return AWS_OP_ERR; - } - return AWS_OP_SUCCESS; -} - -/* Stub this because of the override of aws_array_list_get_at_ptr and for performance. - The contents of session->keyring_trace are nondet in the construction of the harness. - Also neither keyring trace is later used. - Original function is here: - https://github.com/aws/aws-encryption-sdk-c/blob/master/source/list_utils.c#L17 */ -int aws_cryptosdk_transfer_list(struct aws_array_list *dest, struct aws_array_list *src) { - assert(src != dest); - assert(aws_array_list_is_valid(dest)); - assert(aws_array_list_is_valid(src)); - assert(dest->item_size == src->item_size); - - if (nondet_bool()) { - return AWS_OP_ERR; - } - return AWS_OP_SUCCESS; -} - -void array_list_item_generator(struct aws_array_list *elems) { - assert(elems->item_size == sizeof(struct aws_hash_element)); - for (size_t index = 0; index < elems->length; ++index) { - struct aws_hash_element *val = (struct aws_hash_element *)((uint8_t *)elems->data + (elems->item_size * index)); - /* Due to the cast to uint16, the entire size of the enc_ctx must be less than < UINT16_MAX - * This is a simple way to ensure this without a call to enc_ctx_size. */ - struct aws_string *key = ensure_string_is_allocated_nondet_length(); - __CPROVER_assume(aws_string_is_valid(key)); - __CPROVER_assume(key->len <= UINT8_MAX); - val->key = key; - struct aws_string *value = ensure_string_is_allocated_nondet_length(); - __CPROVER_assume(aws_string_is_valid(value)); - __CPROVER_assume(value->len <= UINT8_MAX); - val->value = value; - } -} - -/* Stub this because of the override of aws_array_list_get_at_ptr - Original function is here: - https://github.com/aws/aws-encryption-sdk-c/blob/master/source/keyring_trace.c#L235 */ -void aws_cryptosdk_keyring_trace_clear(struct aws_array_list *trace) { - AWS_FATAL_PRECONDITION(aws_cryptosdk_keyring_trace_is_valid(trace)); - AWS_FATAL_PRECONDITION(trace->item_size == sizeof(struct aws_cryptosdk_keyring_trace_record)); - aws_array_list_clear(trace); -} - -/* Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed - Original function is here: - https://github.com/aws/aws-encryption-sdk-c/blob/master/source/edk.c#L44 */ -void aws_cryptosdk_edk_list_clean_up(struct aws_array_list *encrypted_data_keys) { - assert(aws_cryptosdk_edk_list_is_valid(encrypted_data_keys)); - aws_array_list_clean_up(encrypted_data_keys); -} - -/** - * Receives encryption request from user and attempts to generate encryption materials, - * including an encrypted data key and a list of EDKs for doing encryption. - * - * On success returns AWS_OP_SUCCESS and allocates encryption materials object at address - * pointed to by output. - * - * On failure returns AWS_OP_ERR, sets address pointed to by output to NULL, and sets - * internal AWS error code. - */ int generate_enc_materials( struct aws_cryptosdk_cmm *cmm, struct aws_cryptosdk_enc_materials **output, - struct aws_cryptosdk_enc_request *request) { - assert(aws_cryptosdk_cmm_base_is_valid(cmm)); - assert(AWS_OBJECT_PTR_IS_WRITABLE(output)); - assert(aws_cryptosdk_enc_request_is_valid(request)); - - struct aws_cryptosdk_enc_materials *materials = malloc(sizeof(*materials)); - if (materials == NULL) { - *output = NULL; - return AWS_OP_ERR; - } - - // Set up the allocator - // Request->alloc is session->alloc - materials->alloc = request->alloc; - __CPROVER_assume(aws_allocator_is_valid(materials->alloc)); - __CPROVER_assume(materials->alloc != NULL); - - // Set up the signctx - materials->signctx = ensure_nondet_sig_ctx_has_allocated_members(); - __CPROVER_assume(aws_cryptosdk_sig_ctx_is_valid_cbmc(materials->signctx)); - - // Set up the unencrypted_data_key - __CPROVER_assume(aws_byte_buf_is_bounded(&materials->unencrypted_data_key, MAX_BUFFER_SIZE)); - ensure_byte_buf_has_allocated_buffer_member(&materials->unencrypted_data_key); - __CPROVER_assume(aws_byte_buf_is_valid(&materials->unencrypted_data_key)); - - // Set up the edk_list - __CPROVER_assume(aws_cryptosdk_edk_list_is_bounded(&materials->encrypted_data_keys, MAX_EDK_LIST_ITEMS)); - ensure_cryptosdk_edk_list_has_allocated_list(&materials->encrypted_data_keys); - __CPROVER_assume(aws_cryptosdk_edk_list_is_valid(&materials->encrypted_data_keys)); - - // The alloc is session->alloc - materials->encrypted_data_keys.alloc = request->alloc; - - // Precondition: The edk_list has valid list elements - __CPROVER_assume(aws_cryptosdk_edk_list_elements_are_bounded(&materials->encrypted_data_keys, MAX_BUFFER_SIZE)); - ensure_cryptosdk_edk_list_has_allocated_list_elements(&materials->encrypted_data_keys); - __CPROVER_assume(aws_cryptosdk_edk_list_elements_are_valid(&materials->encrypted_data_keys)); - - // Set up the keyring trace - __CPROVER_assume(aws_array_list_is_bounded( - &materials->keyring_trace, MAX_TRACE_LIST_ITEMS, sizeof(struct aws_cryptosdk_keyring_trace_record))); - __CPROVER_assume(materials->keyring_trace.item_size == sizeof(struct aws_cryptosdk_keyring_trace_record)); - ensure_array_list_has_allocated_data_member(&materials->keyring_trace); - __CPROVER_assume(aws_array_list_is_valid(&materials->keyring_trace)); - ensure_trace_has_allocated_records(&materials->keyring_trace, MAX_STRING_LEN); - __CPROVER_assume(aws_cryptosdk_keyring_trace_is_valid(&materials->keyring_trace)); - - // Set the alg_id - enum aws_cryptosdk_alg_id alg_id; - materials->alg = alg_id; - - *output = materials; - return AWS_OP_SUCCESS; -} + struct aws_cryptosdk_enc_request *request); void aws_cryptosdk_priv_try_gen_key_harness() { /* Nondet Input */ - struct aws_cryptosdk_session *session = - session_setup(MAX_TABLE_SIZE, MAX_TRACE_LIST_ITEMS, MAX_EDK_LIST_ITEMS, MAX_BUFFER_SIZE, MAX_STRING_LEN); + struct aws_cryptosdk_session *session = malloc(sizeof(*session)); /* Assumptions */ __CPROVER_assume(session != NULL); diff --git a/verification/cbmc/stubs/aws_array_list_item_generator_u8_stub.c b/verification/cbmc/stubs/aws_array_list_item_generator_u8_stub.c new file mode 100644 index 000000000..667fca104 --- /dev/null +++ b/verification/cbmc/stubs/aws_array_list_item_generator_u8_stub.c @@ -0,0 +1,38 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). + * You may not use this file except in compliance with the License. + * A copy of the License is located at + * + * http://aws.amazon.com/apache2.0 + * + * or in the "license" file accompanying this file. This file is distributed + * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + * express or implied. See the License for the specific language governing + * permissions and limitations under the License. + */ + +#include + +/* + * A generator function as described in the comment + * in aws_cryptosdk_hash_elems_array_init_stub.c + * This generator is set in the Makefile + */ +void array_list_item_generator(struct aws_array_list *elems) { + assert(elems->item_size == sizeof(struct aws_hash_element)); + for (size_t index = 0; index < elems->length; ++index) { + struct aws_hash_element *val = (struct aws_hash_element *)((uint8_t *)elems->data + (elems->item_size * index)); + /* Due to the cast to uint16, the entire size of the enc_ctx must be less than < UINT16_MAX + * This is a simple way to ensure this without a call to enc_ctx_size. */ + struct aws_string *key = ensure_string_is_allocated_nondet_length(); + __CPROVER_assume(aws_string_is_valid(key)); + __CPROVER_assume(key->len <= UINT8_MAX); + val->key = key; + struct aws_string *value = ensure_string_is_allocated_nondet_length(); + __CPROVER_assume(aws_string_is_valid(value)); + __CPROVER_assume(value->len <= UINT8_MAX); + val->value = value; + } +} diff --git a/verification/cbmc/stubs/generate_enc_materials_stub.c b/verification/cbmc/stubs/generate_enc_materials_stub.c new file mode 100644 index 000000000..1e9478209 --- /dev/null +++ b/verification/cbmc/stubs/generate_enc_materials_stub.c @@ -0,0 +1,89 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). + * You may not use this file except in compliance with the License. + * A copy of the License is located at + * + * http://aws.amazon.com/apache2.0 + * + * or in the "license" file accompanying this file. This file is distributed + * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + * express or implied. See the License for the specific language governing + * permissions and limitations under the License. + */ + +#include + +#include +#include +#include + +/** + * Receives encryption request from user and attempts to generate encryption materials, + * including an encrypted data key and a list of EDKs for doing encryption. + * + * On success returns AWS_OP_SUCCESS and allocates encryption materials object at address + * pointed to by output. + * + * On failure returns AWS_OP_ERR, sets address pointed to by output to NULL, and sets + * internal AWS error code. + */ +int generate_enc_materials( + struct aws_cryptosdk_cmm *cmm, + struct aws_cryptosdk_enc_materials **output, + struct aws_cryptosdk_enc_request *request) { + assert(aws_cryptosdk_cmm_base_is_valid(cmm)); + assert(AWS_OBJECT_PTR_IS_WRITABLE(output)); + assert(aws_cryptosdk_enc_request_is_valid(request)); + + struct aws_cryptosdk_enc_materials *materials = malloc(sizeof(*materials)); + if (materials == NULL) { + *output = NULL; + return AWS_OP_ERR; + } + + // Set up the allocator + // Request->alloc is session->alloc + materials->alloc = request->alloc; + __CPROVER_assume(aws_allocator_is_valid(materials->alloc)); + __CPROVER_assume(materials->alloc != NULL); + + // Set up the signctx + materials->signctx = ensure_nondet_sig_ctx_has_allocated_members(); + __CPROVER_assume(aws_cryptosdk_sig_ctx_is_valid_cbmc(materials->signctx)); + + // Set up the unencrypted_data_key + __CPROVER_assume(aws_byte_buf_is_bounded(&materials->unencrypted_data_key, MAX_BUFFER_SIZE)); + ensure_byte_buf_has_allocated_buffer_member(&materials->unencrypted_data_key); + __CPROVER_assume(aws_byte_buf_is_valid(&materials->unencrypted_data_key)); + + // Set up the edk_list + __CPROVER_assume(aws_cryptosdk_edk_list_is_bounded(&materials->encrypted_data_keys, MAX_EDK_LIST_ITEMS)); + ensure_cryptosdk_edk_list_has_allocated_list(&materials->encrypted_data_keys); + __CPROVER_assume(aws_cryptosdk_edk_list_is_valid(&materials->encrypted_data_keys)); + + // The alloc is session->alloc + materials->encrypted_data_keys.alloc = request->alloc; + + // Precondition: The edk_list has valid list elements + __CPROVER_assume(aws_cryptosdk_edk_list_elements_are_bounded(&materials->encrypted_data_keys, MAX_BUFFER_SIZE)); + ensure_cryptosdk_edk_list_has_allocated_list_elements(&materials->encrypted_data_keys); + __CPROVER_assume(aws_cryptosdk_edk_list_elements_are_valid(&materials->encrypted_data_keys)); + + // Set up the keyring trace + __CPROVER_assume(aws_array_list_is_bounded( + &materials->keyring_trace, MAX_TRACE_LIST_ITEMS, sizeof(struct aws_cryptosdk_keyring_trace_record))); + __CPROVER_assume(materials->keyring_trace.item_size == sizeof(struct aws_cryptosdk_keyring_trace_record)); + ensure_array_list_has_allocated_data_member(&materials->keyring_trace); + __CPROVER_assume(aws_array_list_is_valid(&materials->keyring_trace)); + ensure_trace_has_allocated_records(&materials->keyring_trace, MAX_STRING_LEN); + __CPROVER_assume(aws_cryptosdk_keyring_trace_is_valid(&materials->keyring_trace)); + + // Set the alg_id + enum aws_cryptosdk_alg_id alg_id; + materials->alg = alg_id; + + *output = materials; + return AWS_OP_SUCCESS; +} diff --git a/verification/cbmc/stubs/hkdf_stub.c b/verification/cbmc/stubs/hkdf_stub.c new file mode 100644 index 000000000..4ca4a78cc --- /dev/null +++ b/verification/cbmc/stubs/hkdf_stub.c @@ -0,0 +1,37 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). + * You may not use this file except in compliance with the License. + * A copy of the License is located at + * + * http://aws.amazon.com/apache2.0 + * + * or in the "license" file accompanying this file. This file is distributed + * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + * express or implied. See the License for the specific language governing + * permissions and limitations under the License. + */ + +#include + +#include + +/* Stub this for performance but check the preconditions. + No modified data structure is used again. + Original function is here: + https://github.com/aws/aws-encryption-sdk-c/blob/master/source/hkdf.c#148 */ +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) { + assert(aws_byte_buf_is_valid(salt)); + assert(aws_byte_buf_is_valid(ikm)); + assert(aws_byte_buf_is_valid(info)); + if (nondet_bool()) { + return AWS_OP_ERR; + } + return AWS_OP_SUCCESS; +} diff --git a/verification/cbmc/stubs/keyring_trace_clean_up_stub.c b/verification/cbmc/stubs/keyring_trace_clean_up_stub.c new file mode 100644 index 000000000..4d2d73f6c --- /dev/null +++ b/verification/cbmc/stubs/keyring_trace_clean_up_stub.c @@ -0,0 +1,26 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). + * You may not use this file except in compliance with the License. + * A copy of the License is located at + * + * http://aws.amazon.com/apache2.0 + * + * or in the "license" file accompanying this file. This file is distributed + * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + * express or implied. See the License for the specific language governing + * permissions and limitations under the License. + */ + +#include + +#include + +/* Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed + Original function is here: + https://github.com/aws/aws-encryption-sdk-c/blob/master/source/edk.c#L44 */ +void aws_cryptosdk_edk_list_clean_up(struct aws_array_list *encrypted_data_keys) { + assert(aws_cryptosdk_edk_list_is_valid(encrypted_data_keys)); + aws_array_list_clean_up(encrypted_data_keys); +} diff --git a/verification/cbmc/stubs/keyring_trace_clear_stub.c b/verification/cbmc/stubs/keyring_trace_clear_stub.c new file mode 100644 index 000000000..c78c11f56 --- /dev/null +++ b/verification/cbmc/stubs/keyring_trace_clear_stub.c @@ -0,0 +1,27 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). + * You may not use this file except in compliance with the License. + * A copy of the License is located at + * + * http://aws.amazon.com/apache2.0 + * + * or in the "license" file accompanying this file. This file is distributed + * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + * express or implied. See the License for the specific language governing + * permissions and limitations under the License. + */ + +#include + +#include + +/* Stub this because of the override of aws_array_list_get_at_ptr + Original function is here: + https://github.com/aws/aws-encryption-sdk-c/blob/master/source/keyring_trace.c#L235 */ +void aws_cryptosdk_keyring_trace_clear(struct aws_array_list *trace) { + AWS_FATAL_PRECONDITION(aws_cryptosdk_keyring_trace_is_valid(trace)); + AWS_FATAL_PRECONDITION(trace->item_size == sizeof(struct aws_cryptosdk_keyring_trace_record)); + aws_array_list_clear(trace); +} diff --git a/verification/cbmc/stubs/transfer_list_stub.c b/verification/cbmc/stubs/transfer_list_stub.c new file mode 100644 index 000000000..b04f4bec5 --- /dev/null +++ b/verification/cbmc/stubs/transfer_list_stub.c @@ -0,0 +1,35 @@ +/* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"). + * You may not use this file except in compliance with the License. + * A copy of the License is located at + * + * http://aws.amazon.com/apache2.0 + * + * or in the "license" file accompanying this file. This file is distributed + * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either + * express or implied. See the License for the specific language governing + * permissions and limitations under the License. + */ + +#include + +#include + +/* Stub this because of the override of aws_array_list_get_at_ptr and for performance. + The contents of session->keyring_trace are nondet in the construction of the harness. + Also neither keyring trace is later used. + Original function is here: + https://github.com/aws/aws-encryption-sdk-c/blob/master/source/list_utils.c#L17 */ +int aws_cryptosdk_transfer_list(struct aws_array_list *dest, struct aws_array_list *src) { + assert(src != dest); + assert(aws_array_list_is_valid(dest)); + assert(aws_array_list_is_valid(src)); + assert(dest->item_size == src->item_size); + + if (nondet_bool()) { + return AWS_OP_ERR; + } + return AWS_OP_SUCCESS; +} From 753f8a32eabc3c978ba483f8a7dc77cdaf56ad99 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 14 Jan 2021 22:02:22 +0000 Subject: [PATCH 11/17] Weaken preconditions. Allow null in session members --- include/aws/cryptosdk/private/session.h | 2 +- source/session_encrypt.c | 2 -- .../aws_cryptosdk_priv_try_gen_key_harness.c | 22 +++++++++++-------- 3 files changed, 14 insertions(+), 12 deletions(-) diff --git a/include/aws/cryptosdk/private/session.h b/include/aws/cryptosdk/private/session.h index 62478b2fd..1626e0640 100644 --- a/include/aws/cryptosdk/private/session.h +++ b/include/aws/cryptosdk/private/session.h @@ -103,7 +103,7 @@ AWS_CRYPTOSDK_STATIC_INLINE bool aws_cryptosdk_session_is_valid(const struct aws bool cmm_valid = aws_cryptosdk_cmm_base_is_valid(session->cmm); bool hdr_valid = aws_cryptosdk_hdr_is_valid(&session->header); bool keyring_trace_valid = aws_cryptosdk_keyring_trace_is_valid(&session->keyring_trace); - bool alg_props_valid = aws_cryptosdk_alg_properties_is_valid(session->alg_props); + bool alg_props_valid = session->alg_props == NULL || aws_cryptosdk_alg_properties_is_valid(session->alg_props); bool content_key_valid = aws_cryptosdk_content_key_is_valid(&session->content_key); bool key_commitment_valid = aws_byte_buf_is_valid(&session->key_commitment); bool signctx_valid = (session->signctx == NULL) || aws_cryptosdk_sig_ctx_is_valid(session->signctx); diff --git a/source/session_encrypt.c b/source/session_encrypt.c index 6b2692965..bc8ca1d85 100644 --- a/source/session_encrypt.c +++ b/source/session_encrypt.c @@ -49,8 +49,6 @@ void aws_cryptosdk_priv_encrypt_compute_body_estimate(struct aws_cryptosdk_sessi int aws_cryptosdk_priv_try_gen_key(struct aws_cryptosdk_session *session) { AWS_PRECONDITION(aws_cryptosdk_session_is_valid(session)); - AWS_PRECONDITION(session->header.iv.len <= session->alg_props->iv_len); - AWS_PRECONDITION(session->header.auth_tag.len <= session->alg_props->tag_len); AWS_PRECONDITION(aws_cryptosdk_commitment_policy_is_valid(session->commitment_policy)); AWS_PRECONDITION(session->state == ST_GEN_KEY); AWS_PRECONDITION(session->mode == AWS_CRYPTOSDK_ENCRYPT); diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c index c9e4a9c01..dba672e7e 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c @@ -56,18 +56,13 @@ void aws_cryptosdk_priv_try_gen_key_harness() { __CPROVER_assume(aws_cryptosdk_cmm_base_is_valid(cmm)); session->cmm = cmm; - /* Set the session->alg_id */ - enum aws_cryptosdk_alg_id alg_id; - struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg_id); - __CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(props)); - session->alg_props = props; + /* session->alg_props can be NULL or valid */ + session->alg_props = ensure_alg_properties_attempt_allocation(MAX_STRING_LEN); + __CPROVER_assume(IMPLIES(session->alg_props != NULL, aws_cryptosdk_alg_properties_is_valid(session->alg_props))); /* Set the session->header */ struct aws_cryptosdk_hdr *hdr = hdr_setup(MAX_TABLE_SIZE, MAX_EDK_LIST_ITEMS, MAX_BUFFER_SIZE); - __CPROVER_assume(aws_byte_buf_is_bounded(&hdr->iv, session->alg_props->iv_len)); - __CPROVER_assume(aws_byte_buf_is_bounded(&hdr->auth_tag, session->alg_props->tag_len)); - /* The header edk_list should have been cleared earlier. See comment in build_header: "The header should have been cleared earlier, so the materials structure should have zero EDKs (otherwise we'd need to destroy the old EDKs as well). */ @@ -95,6 +90,15 @@ void aws_cryptosdk_priv_try_gen_key_harness() { __CPROVER_assume(session->state == ST_GEN_KEY); __CPROVER_assume(session->mode == AWS_CRYPTOSDK_ENCRYPT); + /* session->signctx can be NULL or valid */ + session->signctx = ensure_nondet_sig_ctx_has_allocated_members(); + __CPROVER_assume(IMPLIES(session->signctx != NULL, aws_cryptosdk_sig_ctx_is_valid(session->signctx))); + + /* session->key_commitment must be valid */ + ensure_byte_buf_has_allocated_buffer_member(&session->key_commitment); + __CPROVER_assume(aws_byte_buf_is_bounded(&session->key_commitment, MAX_BUFFER_SIZE)); + __CPROVER_assume(aws_byte_buf_is_valid(&session->key_commitment)); + /* Save current state of the data structure */ struct store_byte_from_buffer old_enc_ctx; save_byte_from_hash_table(&session->header.enc_ctx, &old_enc_ctx); @@ -102,7 +106,7 @@ void aws_cryptosdk_priv_try_gen_key_harness() { /* Function under verification */ if (aws_cryptosdk_priv_try_gen_key(session) == AWS_OP_SUCCESS) { /* Assertions */ - assert(aws_cryptosdk_hdr_is_valid(&session->header)); + assert(aws_cryptosdk_session_is_valid(session)); } check_hash_table_unchanged(&session->header.enc_ctx, &old_enc_ctx); } From 99e56f20ca6972bc3109141baf44df78a54a5195 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 15 Jan 2021 15:21:15 +0000 Subject: [PATCH 12/17] Remove CBMC_OBJECT_BITS flag --- .../proofs/aws_cryptosdk_priv_try_gen_key/Makefile | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile index be68da02e..af3537880 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile @@ -39,14 +39,6 @@ DEFINES += -DMAX_IV_LEN=$(MAX_IV_LEN) DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) DEFINES += -DMAX_TRACE_LIST_ITEMS=$(MAX_TRACE_LIST_ITEMS) -# The maximum number of objects is set to 2^8 = 256. This option changes that to 2^9. -# Without this flag, running this proof causes the CBMC error of -# "too many addressed objects: maximum number of objects is set to 2^n=256 (with n=8); -# use the `--object-bits n` option to increase the maximum number" -# The proof hits the error when the line "rv = aws_cryptosdk_hdr_write(&session->header, -# &actual_size, session->header_copy, session->header_size);" is reached. -CBMC_OBJECT_BITS = 9 - PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/hash_table.c @@ -93,6 +85,8 @@ PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_enc_ctx_size_stub.c PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_hash_elems_array_init_stub.c PROOF_SOURCES += $(PROOF_STUB)/aws_default_allocator_stub.c PROOF_SOURCES += $(PROOF_STUB)/generate_enc_materials_stub.c +# Stubbing out aws_cryptosdk_hdr_write leads to a huge gain in performance +# Not including this stub would also require you to set CBMC_OBJECT_BITS = 9 PROOF_SOURCES += $(PROOF_STUB)/hdr_write_stub.c PROOF_SOURCES += $(PROOF_STUB)/hkdf_stub.c PROOF_SOURCES += $(PROOF_STUB)/keyring_trace_clean_up_stub.c From 00e277b0de7e5c41baccbcf802b4030404333437 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 15 Jan 2021 18:28:53 +0000 Subject: [PATCH 13/17] Add comments and assert for `okm` in hkdf stub --- .../aws_cryptosdk_priv_try_gen_key_harness.c | 20 ++++++++++++++----- verification/cbmc/stubs/hkdf_stub.c | 1 + 2 files changed, 16 insertions(+), 5 deletions(-) diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c index dba672e7e..e9e30277a 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c @@ -34,6 +34,13 @@ int generate_enc_materials( struct aws_cryptosdk_enc_materials **output, struct aws_cryptosdk_enc_request *request); +/* + * This harness is extremely expensive to run so we have stubbed out + * multiple functions (see Makefile). It also requires a quite specific + * configuration for the session struct (cmm's vtable must include a + * pointer to the function declared above, alg_props can be NULL or valid, + * etc.) so we do not use the session_setup method to initialize it + */ void aws_cryptosdk_priv_try_gen_key_harness() { /* Nondet Input */ struct aws_cryptosdk_session *session = malloc(sizeof(*session)); @@ -41,7 +48,7 @@ void aws_cryptosdk_priv_try_gen_key_harness() { /* Assumptions */ __CPROVER_assume(session != NULL); - /* Set the session->cmm */ + /* Set session->cmm */ const struct aws_cryptosdk_cmm_vt vtable = { .vt_size = sizeof(struct aws_cryptosdk_cmm_vt), .name = ensure_c_str_is_allocated(SIZE_MAX), .destroy = nondet_voidp(), @@ -64,12 +71,14 @@ void aws_cryptosdk_priv_try_gen_key_harness() { struct aws_cryptosdk_hdr *hdr = hdr_setup(MAX_TABLE_SIZE, MAX_EDK_LIST_ITEMS, MAX_BUFFER_SIZE); /* The header edk_list should have been cleared earlier. - See comment in build_header: "The header should have been cleared earlier, so the materials structure - should have zero EDKs (otherwise we'd need to destroy the old EDKs as well). */ + * See comment in build_header: + * "The header should have been cleared earlier, so the materials structure + * should have zero EDKs" (otherwise we'd need to destroy the old EDKs as well) + */ __CPROVER_assume(aws_array_list_length(&hdr->edk_list) == 0); session->header = *hdr; - /* Set the session->keyring_trace */ + /* Set session->keyring_trace */ struct aws_array_list *keyring_trace = malloc(sizeof(*keyring_trace)); __CPROVER_assume(keyring_trace != NULL); __CPROVER_assume(aws_array_list_is_bounded( @@ -84,7 +93,8 @@ void aws_cryptosdk_priv_try_gen_key_harness() { /* Set the allocators */ session->alloc = can_fail_allocator(); __CPROVER_assume(aws_allocator_is_valid(session->alloc)); - session->header.edk_list.alloc = session->alloc; // This assumption is needed for build_header + /* This assumption is needed for build_header */ + session->header.edk_list.alloc = session->alloc; __CPROVER_assume(aws_cryptosdk_commitment_policy_is_valid(session->commitment_policy)); __CPROVER_assume(session->state == ST_GEN_KEY); diff --git a/verification/cbmc/stubs/hkdf_stub.c b/verification/cbmc/stubs/hkdf_stub.c index 4ca4a78cc..243c168d7 100644 --- a/verification/cbmc/stubs/hkdf_stub.c +++ b/verification/cbmc/stubs/hkdf_stub.c @@ -27,6 +27,7 @@ int aws_cryptosdk_hkdf( const struct aws_byte_buf *salt, const struct aws_byte_buf *ikm, const struct aws_byte_buf *info) { + assert(aws_byte_buf_is_valid(okm)); assert(aws_byte_buf_is_valid(salt)); assert(aws_byte_buf_is_valid(ikm)); assert(aws_byte_buf_is_valid(info)); From c782c0a95c72e98dc4aeb099df6c435ac7476aa4 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 18 Jan 2021 13:19:48 +0000 Subject: [PATCH 14/17] Add props assumptions in sign_header and derive_data_key proofs --- source/session_decrypt.c | 1 + source/session_encrypt.c | 1 + .../cbmc/proofs/derive_data_key/derive_data_key_harness.c | 5 +++++ verification/cbmc/proofs/sign_header/sign_header_harness.c | 5 +++++ 4 files changed, 12 insertions(+) diff --git a/source/session_decrypt.c b/source/session_decrypt.c index cbda6b308..792d394e2 100644 --- a/source/session_decrypt.c +++ b/source/session_decrypt.c @@ -68,6 +68,7 @@ static int fill_request(struct aws_cryptosdk_dec_request *request, struct aws_cr static int derive_data_key(struct aws_cryptosdk_session *session, struct aws_cryptosdk_dec_materials *materials) { AWS_PRECONDITION(aws_cryptosdk_session_is_valid(session)); + AWS_PRECONDITION(aws_cryptosdk_alg_properties_is_valid(session->alg_props)); AWS_PRECONDITION(aws_cryptosdk_dec_materials_is_valid(materials)); if (materials->unencrypted_data_key.len != session->alg_props->data_key_len) { diff --git a/source/session_encrypt.c b/source/session_encrypt.c index bc8ca1d85..b1be29f75 100644 --- a/source/session_encrypt.c +++ b/source/session_encrypt.c @@ -175,6 +175,7 @@ static int build_header(struct aws_cryptosdk_session *session, struct aws_crypto static int sign_header(struct aws_cryptosdk_session *session) { AWS_PRECONDITION(aws_cryptosdk_session_is_valid(session)); + AWS_PRECONDITION(aws_cryptosdk_alg_properties_is_valid(session->alg_props)); AWS_PRECONDITION(session->alg_props->impl->cipher_ctor != NULL); AWS_PRECONDITION(session->header.iv.len <= session->alg_props->iv_len); AWS_PRECONDITION(session->header.auth_tag.len <= session->alg_props->tag_len); 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 23a61fba0..1a3fdd95b 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 @@ -31,6 +31,11 @@ void derive_data_key_harness() { dec_materials_setup(MAX_TRACE_LIST_ITEMS, MAX_BUFFER_SIZE, MAX_STRING_LEN); /* Assumptions */ + if (session->alg_props == NULL) { + struct aws_cryptosdk_alg_properties *props = ensure_alg_properties_attempt_allocation(MAX_STRING_LEN); + __CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(props)); + session->alg_props = props; + } __CPROVER_assume(aws_cryptosdk_commitment_policy_is_valid(session->commitment_policy)); __CPROVER_assume(session->alg_props->commitment_len <= sizeof(session->key_commitment_arr)); diff --git a/verification/cbmc/proofs/sign_header/sign_header_harness.c b/verification/cbmc/proofs/sign_header/sign_header_harness.c index 1480d14cd..72e888f23 100644 --- a/verification/cbmc/proofs/sign_header/sign_header_harness.c +++ b/verification/cbmc/proofs/sign_header/sign_header_harness.c @@ -49,6 +49,11 @@ void sign_header_harness() { session_setup(MAX_TABLE_SIZE, MAX_TRACE_LIST_ITEMS, MAX_EDK_LIST_ITEMS, MAX_BUFFER_SIZE, MAX_STRING_LEN); /* Assumptions */ + if (session->alg_props == NULL) { + struct aws_cryptosdk_alg_properties *props = ensure_alg_properties_attempt_allocation(MAX_STRING_LEN); + __CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(props)); + session->alg_props = props; + } __CPROVER_assume(session->alg_props->impl->cipher_ctor != NULL); __CPROVER_assume(aws_byte_buf_is_bounded(&session->header.iv, session->alg_props->iv_len)); __CPROVER_assume(aws_byte_buf_is_bounded(&session->header.auth_tag, session->alg_props->tag_len)); From fd16bf3a040ab82b2b385ea0edc2bb54e00c3593 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 19 Jan 2021 09:28:29 +0000 Subject: [PATCH 15/17] Remove unused stub `aws_default_allocator` --- verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile | 1 - verification/cbmc/proofs/sign_header/Makefile | 1 - 2 files changed, 2 deletions(-) diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile index af3537880..e0ecbedf5 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile @@ -83,7 +83,6 @@ PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_item_generator_u8_stub.c PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_sort_noop_stub.c PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_enc_ctx_size_stub.c PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_hash_elems_array_init_stub.c -PROOF_SOURCES += $(PROOF_STUB)/aws_default_allocator_stub.c PROOF_SOURCES += $(PROOF_STUB)/generate_enc_materials_stub.c # Stubbing out aws_cryptosdk_hdr_write leads to a huge gain in performance # Not including this stub would also require you to set CBMC_OBJECT_BITS = 9 diff --git a/verification/cbmc/proofs/sign_header/Makefile b/verification/cbmc/proofs/sign_header/Makefile index 476513b32..0c9c245cb 100644 --- a/verification/cbmc/proofs/sign_header/Makefile +++ b/verification/cbmc/proofs/sign_header/Makefile @@ -75,7 +75,6 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c PROOF_SOURCES += $(PROOF_STUB)/aws_array_list_sort_noop_stub.c PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_enc_ctx_size_stub.c PROOF_SOURCES += $(PROOF_STUB)/aws_cryptosdk_hash_elems_array_init_stub.c -PROOF_SOURCES += $(PROOF_STUB)/aws_default_allocator_stub.c # Stubbing out aws_cryptosdk_hdr_write leads to a huge gain in performance PROOF_SOURCES += $(PROOF_STUB)/hdr_write_stub.c PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) From df5baa368523bfc7090cbe2062ccb417cfbe8a3b Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 19 Jan 2021 12:47:55 +0000 Subject: [PATCH 16/17] Add missing source file in `sign_header` proof --- verification/cbmc/proofs/sign_header/Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/verification/cbmc/proofs/sign_header/Makefile b/verification/cbmc/proofs/sign_header/Makefile index 0c9c245cb..454cac3cf 100644 --- a/verification/cbmc/proofs/sign_header/Makefile +++ b/verification/cbmc/proofs/sign_header/Makefile @@ -38,6 +38,7 @@ DEFINES += -DMAX_IV_LEN=$(MAX_IV_LEN) DEFINES += -DAWS_CRYPTOSDK_HASH_ELEMS_ARRAY_INIT_GENERATOR=array_list_item_generator PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/hash_table.c PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/string.c PROJECT_SOURCES += $(COMMON_PROOF_UNINLINE)/array_list.c From ec5b3820e7ca305dab7219220cb2fb292af6e76c Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 19 Jan 2021 15:10:17 +0000 Subject: [PATCH 17/17] Add minor improvements --- include/aws/cryptosdk/private/session.h | 12 ++++++------ .../aws_cryptosdk_priv_try_gen_key_harness.c | 2 +- .../stubs/aws_array_list_item_generator_u8_stub.c | 14 ++++++++++++-- 3 files changed, 19 insertions(+), 9 deletions(-) diff --git a/include/aws/cryptosdk/private/session.h b/include/aws/cryptosdk/private/session.h index 1626e0640..3875896d7 100644 --- a/include/aws/cryptosdk/private/session.h +++ b/include/aws/cryptosdk/private/session.h @@ -99,12 +99,12 @@ AWS_CRYPTOSDK_STATIC_INLINE bool aws_cryptosdk_session_is_valid(const struct aws if (!AWS_OBJECT_PTR_IS_WRITABLE(session)) { return false; } - bool allocator_valid = aws_allocator_is_valid(session->alloc); - bool cmm_valid = aws_cryptosdk_cmm_base_is_valid(session->cmm); - bool hdr_valid = aws_cryptosdk_hdr_is_valid(&session->header); - bool keyring_trace_valid = aws_cryptosdk_keyring_trace_is_valid(&session->keyring_trace); - bool alg_props_valid = session->alg_props == NULL || aws_cryptosdk_alg_properties_is_valid(session->alg_props); - bool content_key_valid = aws_cryptosdk_content_key_is_valid(&session->content_key); + bool allocator_valid = aws_allocator_is_valid(session->alloc); + bool cmm_valid = aws_cryptosdk_cmm_base_is_valid(session->cmm); + bool hdr_valid = aws_cryptosdk_hdr_is_valid(&session->header); + bool keyring_trace_valid = aws_cryptosdk_keyring_trace_is_valid(&session->keyring_trace); + bool alg_props_valid = (session->alg_props == NULL || aws_cryptosdk_alg_properties_is_valid(session->alg_props)); + bool content_key_valid = aws_cryptosdk_content_key_is_valid(&session->content_key); bool key_commitment_valid = aws_byte_buf_is_valid(&session->key_commitment); bool signctx_valid = (session->signctx == NULL) || aws_cryptosdk_sig_ctx_is_valid(session->signctx); return allocator_valid && cmm_valid && hdr_valid && keyring_trace_valid && alg_props_valid && content_key_valid && diff --git a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c index e9e30277a..491079eee 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c @@ -39,7 +39,7 @@ int generate_enc_materials( * multiple functions (see Makefile). It also requires a quite specific * configuration for the session struct (cmm's vtable must include a * pointer to the function declared above, alg_props can be NULL or valid, - * etc.) so we do not use the session_setup method to initialize it + * etc.) so we do not use the session_setup method to initialize it. */ void aws_cryptosdk_priv_try_gen_key_harness() { /* Nondet Input */ diff --git a/verification/cbmc/stubs/aws_array_list_item_generator_u8_stub.c b/verification/cbmc/stubs/aws_array_list_item_generator_u8_stub.c index 667fca104..5de9979f2 100644 --- a/verification/cbmc/stubs/aws_array_list_item_generator_u8_stub.c +++ b/verification/cbmc/stubs/aws_array_list_item_generator_u8_stub.c @@ -17,8 +17,18 @@ /* * A generator function as described in the comment - * in aws_cryptosdk_hash_elems_array_init_stub.c - * This generator is set in the Makefile + * in aws_cryptosdk_hash_elems_array_init_stub.c: + * + * If the consumer of the list does not use the elements in the list, + * we can just leave it undefined. This is sound, as it gives you a totally + * nondet. value every time you use a list element, and is the default + * behaviour of CBMC. But if it is used, we need a way for the harness + * to specify valid values for the element, for example if they are copying + * values out of the table. They can do this by defining + * -DAWS_CRYPTOSDK_HASH_ELEMS_ARRAY_INIT_GENERATOR=the_generator_fn + * where the_generator_fn has signature + * the_generator_fn(struct aws_array_list *elems). + * [elems] is a pointer to the array_list whose values need to be set */ void array_list_item_generator(struct aws_array_list *elems) { assert(elems->item_size == sizeof(struct aws_hash_element));