From 95d70999864eb014c49548b3fc76ea19ad25f6af Mon Sep 17 00:00:00 2001 From: tegansb <68670922+tegansb@users.noreply.github.com> Date: Tue, 19 Jan 2021 11:14:11 -0800 Subject: [PATCH] Adds CBMC proof for aws_cryptosdk_priv_try_gen_key (#661) * Adds check in case byte_buf_init fails * Adds harness, Makefile and yaml for priv_try_gen_key * Adds preconditions to source code * Update to harness * yaml update to boiler plate default * Remove unneccessary remove functions * Added preconditions of lne of byte bufs * Use CBMC_OBJECT_BITS = 9 flag * Use session setup and validator functions * Move stubs in harness to stubs folder * Weaken preconditions. Allow null in session members * Remove CBMC_OBJECT_BITS flag * Add comments and assert for `okm` in hkdf stub * Add props assumptions in sign_header and derive_data_key proofs * Remove unused stub `aws_default_allocator` * Add missing source file in `sign_header` proof * Add minor improvements Co-authored-by: Adrian Palacios --- include/aws/cryptosdk/private/session.h | 12 +- source/session_decrypt.c | 1 + source/session_encrypt.c | 9 +- .../aws_cryptosdk_priv_try_gen_key/Makefile | 119 +++++++++++++++++ .../aws_cryptosdk_priv_try_gen_key_harness.c | 122 ++++++++++++++++++ .../cbmc-batch.yaml | 4 + .../derive_data_key/derive_data_key_harness.c | 5 + verification/cbmc/proofs/sign_header/Makefile | 2 +- .../proofs/sign_header/sign_header_harness.c | 5 + .../aws_array_list_item_generator_u8_stub.c | 48 +++++++ .../cbmc/stubs/generate_enc_materials_stub.c | 89 +++++++++++++ verification/cbmc/stubs/hkdf_stub.c | 38 ++++++ .../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 +++++ 15 files changed, 534 insertions(+), 8 deletions(-) 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 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/include/aws/cryptosdk/private/session.h b/include/aws/cryptosdk/private/session.h index 4ad32e942..66fc8f3d5 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 = 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/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 57b80b223..e6de3cbdd 100644 --- a/source/session_encrypt.c +++ b/source/session_encrypt.c @@ -54,6 +54,10 @@ 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(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; @@ -95,7 +99,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; } @@ -176,6 +182,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/aws_cryptosdk_priv_try_gen_key/Makefile b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile new file mode 100644 index 000000000..e0ecbedf5 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile @@ -0,0 +1,119 @@ +# 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_LIST_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_LIST_ITEMS=$(MAX_TRACE_LIST_ITEMS) + +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_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)/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 +PROOF_SOURCES += $(PROOF_STUB)/keyring_trace_clear_stub.c +PROOF_SOURCES += $(PROOF_STUB)/transfer_list_stub.c +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) + +# 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 +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)) +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_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_LIST_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..491079eee --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c @@ -0,0 +1,122 @@ +/* + * 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 + +int generate_enc_materials( + struct aws_cryptosdk_cmm *cmm, + 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)); + + /* Assumptions */ + __CPROVER_assume(session != NULL); + + /* 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(), + .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; + + /* 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); + + /* 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); + session->header = *hdr; + + /* 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( + 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)); + 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; + + /* Set the allocators */ + session->alloc = can_fail_allocator(); + __CPROVER_assume(aws_allocator_is_valid(session->alloc)); + /* 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); + __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); + + /* Function under verification */ + if (aws_cryptosdk_priv_try_gen_key(session) == AWS_OP_SUCCESS) { + /* Assertions */ + assert(aws_cryptosdk_session_is_valid(session)); + } + check_hash_table_unchanged(&session->header.enc_ctx, &old_enc_ctx); +} 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..e936b4599 --- /dev/null +++ b/verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml @@ -0,0 +1,4 @@ +: + 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 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/Makefile b/verification/cbmc/proofs/sign_header/Makefile index 476513b32..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 @@ -75,7 +76,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) 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)); 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..5de9979f2 --- /dev/null +++ b/verification/cbmc/stubs/aws_array_list_item_generator_u8_stub.c @@ -0,0 +1,48 @@ +/* + * 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: + * + * 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)); + 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..243c168d7 --- /dev/null +++ b/verification/cbmc/stubs/hkdf_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 + +#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(okm)); + 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; +}