From f2e95935e37ae82f540b2e19fbff42a53365de2d Mon Sep 17 00:00:00 2001 From: tegansb <68670922+tegansb@users.noreply.github.com> Date: Mon, 11 Jan 2021 08:29:41 -0800 Subject: [PATCH] Adds CBMC proof for sign_header (#659) * Split aws_cryptosdk_hdr_parse into smaller functions Resolves #639. * Adds harness, Makefile and yaml for sign_header * Added preconditions to source code and added checks for memcpy * Update Makefile * Remove unneeded empty slot assumption * Use new hdr_setup in harness and fix comment * Added comment about when the object-bits flag is required * Added preconditions of lne of byte bufs * Use CBMC_OBJECT_BITS flag * Make len != 0 check explicit * Use session_setup and aws_session_is_valid * Remove signctx precondition in harness. Weaken precondition in EVPDigestUpdate * Stub out hdr_write. Use default CBMC_OBJECT_BITS value * Remove unwind value for hdr_write * Add and improve documentation Co-authored-by: Alex Chew Co-authored-by: Alex Chew Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Co-authored-by: Adrian Palacios --- source/cipher.c | 2 +- source/keyring_trace.c | 17 ++- source/session_encrypt.c | 32 +++++- verification/cbmc/proofs/sign_header/Makefile | 102 ++++++++++++++++++ .../cbmc/proofs/sign_header/cbmc-batch.yaml | 4 + .../proofs/sign_header/sign_header_harness.c | 79 ++++++++++++++ .../cbmc/sources/openssl/evp_override.c | 2 +- verification/cbmc/stubs/hdr_write_stub.c | 45 ++++++++ 8 files changed, 267 insertions(+), 16 deletions(-) create mode 100644 verification/cbmc/proofs/sign_header/Makefile create mode 100644 verification/cbmc/proofs/sign_header/cbmc-batch.yaml create mode 100644 verification/cbmc/proofs/sign_header/sign_header_harness.c create mode 100644 verification/cbmc/stubs/hdr_write_stub.c diff --git a/source/cipher.c b/source/cipher.c index ea5a5a603..97fc9ff1e 100644 --- a/source/cipher.c +++ b/source/cipher.c @@ -275,7 +275,7 @@ bool aws_cryptosdk_alg_properties_is_valid(const struct aws_cryptosdk_alg_proper if (std_alg_props == NULL) { return false; } - return alg_props->md_name && alg_props->cipher_name && alg_props->alg_name && + return alg_props->md_name && alg_props->cipher_name && alg_props->alg_name && alg_props->impl && aws_cryptosdk_alg_properties_equal(*alg_props, *std_alg_props); } diff --git a/source/keyring_trace.c b/source/keyring_trace.c index 3571ae690..462a947e4 100644 --- a/source/keyring_trace.c +++ b/source/keyring_trace.c @@ -20,18 +20,17 @@ bool aws_cryptosdk_keyring_trace_is_valid(const struct aws_array_list *trace) { return false; } AWS_FATAL_PRECONDITION(trace->item_size == sizeof(struct aws_cryptosdk_keyring_trace_record)); + if (!aws_array_list_is_valid(trace)) { + return false; + } /* iterate over each record in the list */ - size_t num_records = aws_array_list_length(trace); - bool is_valid = aws_array_list_is_valid(trace); - for (size_t idx = 0; idx < num_records; ++idx) { - struct aws_cryptosdk_keyring_trace_record *record; - if (!aws_array_list_get_at_ptr(trace, (void **)&record, idx)) { - /* check if each record is valid */ - bool record_is_valid = aws_cryptosdk_keyring_trace_record_is_valid(record); - is_valid &= record_is_valid; + struct aws_cryptosdk_keyring_trace_record *data = (struct aws_cryptosdk_keyring_trace_record *)trace->data; + for (size_t i = 0; i < trace->length; ++i) { + if (!aws_cryptosdk_keyring_trace_record_is_valid(&(data[i]))) { + return false; } } - return is_valid; + return true; } bool aws_cryptosdk_keyring_trace_record_is_valid(struct aws_cryptosdk_keyring_trace_record *record) { diff --git a/source/session_encrypt.c b/source/session_encrypt.c index 289c6dfe1..5ec31016e 100644 --- a/source/session_encrypt.c +++ b/source/session_encrypt.c @@ -168,6 +168,12 @@ 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(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); + AWS_PRECONDITION(session->state == ST_GEN_KEY); + AWS_PRECONDITION(session->mode == AWS_CRYPTOSDK_ENCRYPT); session->header_size = aws_cryptosdk_hdr_size(&session->header); if (session->header_size == 0) { @@ -183,8 +189,14 @@ static int sign_header(struct aws_cryptosdk_session *session) { // see what happened. It also makes sure that the header is fully initialized, // again just in case some bug doesn't overwrite them properly. - memset(session->header.iv.buffer, 0x42, session->header.iv.len); - memset(session->header.auth_tag.buffer, 0xDE, session->header.auth_tag.len); + if (session->header.iv.len != 0) { + assert(session->header.iv.buffer); + memset(session->header.iv.buffer, 0x42, session->header.iv.len); + } + if (session->header.auth_tag.len != 0) { + assert(session->header.auth_tag.buffer); + memset(session->header.auth_tag.buffer, 0xDE, session->header.auth_tag.len); + } size_t actual_size; @@ -205,10 +217,20 @@ static int sign_header(struct aws_cryptosdk_session *session) { if (rv) return AWS_OP_ERR; if (session->alg_props->msg_format_version == AWS_CRYPTOSDK_HEADER_VERSION_1_0) { - memcpy(session->header.iv.buffer, authtag.buffer, session->header.iv.len); - memcpy(session->header.auth_tag.buffer, authtag.buffer + session->header.iv.len, session->header.auth_tag.len); + if (session->header.iv.len != 0) { + assert(session->header.iv.buffer); + memcpy(session->header.iv.buffer, authtag.buffer, session->header.iv.len); + } + if (session->header.auth_tag.len != 0) { + assert(session->header.auth_tag.buffer); + memcpy( + session->header.auth_tag.buffer, authtag.buffer + session->header.iv.len, session->header.auth_tag.len); + } } else { - memcpy(session->header.auth_tag.buffer, authtag.buffer, session->header.auth_tag.len); + if (session->header.auth_tag.len != 0) { + assert(session->header.auth_tag.buffer); + memcpy(session->header.auth_tag.buffer, authtag.buffer, session->header.auth_tag.len); + } } // Re-serialize the header now that we know the auth tag diff --git a/verification/cbmc/proofs/sign_header/Makefile b/verification/cbmc/proofs/sign_header/Makefile new file mode 100644 index 000000000..476513b32 --- /dev/null +++ b/verification/cbmc/proofs/sign_header/Makefile @@ -0,0 +1,102 @@ +# Copyright 2020 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.aws_byte_buf +include ../Makefile.string + +PROOF_UID = sign_header +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(HARNESS_ENTRY).c + +# Increasing the length of the edk_list or enc_ctx does not improve coverage. +# We use these values for performance. +MAX_TRACE_LIST_ITEMS ?= 1 +MAX_EDK_LIST_ITEMS ?= 1 +MAX_TABLE_SIZE ?= 2 + +DEFINES += -DAWS_NO_STATIC_IMPL +DEFINES += -DMAX_EDK_LIST_ITEMS=$(MAX_EDK_LIST_ITEMS) +DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE) +DEFINES += -DARRAY_LIST_TYPE="struct aws_cryptosdk_edk" +DEFINES += -DARRAY_LIST_TYPE_HEADER=\"aws/cryptosdk/edk.h\" +DEFINES += -DMAX_TRACE_LIST_ITEMS=$(MAX_TRACE_LIST_ITEMS) +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/hash_table.c +PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/string.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 += $(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/keyring_trace.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)/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 +# 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) + +# 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:$(call addone,$(MAX_TABLE_SIZE)) +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:$(call addone,$(MAX_TABLE_SIZE)) +UNWINDSET += aws_cryptosdk_hdr_size.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) +UNWINDSET += aws_cryptosdk_keyring_trace_is_valid.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/sign_header/cbmc-batch.yaml b/verification/cbmc/proofs/sign_header/cbmc-batch.yaml new file mode 100644 index 000000000..e936b4599 --- /dev/null +++ b/verification/cbmc/proofs/sign_header/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/sign_header/sign_header_harness.c b/verification/cbmc/proofs/sign_header/sign_header_harness.c new file mode 100644 index 000000000..1480d14cd --- /dev/null +++ b/verification/cbmc/proofs/sign_header/sign_header_harness.c @@ -0,0 +1,79 @@ +/* + * 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 + +/** + * A generator function as described in the comment in aws_cryptosdk_hash_elems_array_init_stub.c. + * Also see DEFINES += -DAWS_CRYPTOSDK_HASH_ELEMS_ARRAY_INIT_GENERATOR=array_list_item_generator + * (line 37) 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 checks in aws_cryptosdk_enc_ctx_size, no string can have a length > UINT16_MAX. */ + struct aws_string *key = ensure_string_is_allocated_nondet_length(); + __CPROVER_assume(aws_string_is_valid(key)); + /* 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. */ + __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; + } +} + +void sign_header_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); + + /* Assumptions */ + __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)); + __CPROVER_assume(session->state == ST_GEN_KEY); + __CPROVER_assume(session->mode == AWS_CRYPTOSDK_ENCRYPT); + + /* Save current state of the data structure */ + struct aws_byte_buf old_message_id = session->header.message_id; + struct store_byte_from_buffer old_byte_from_message_id; + save_byte_from_array(session->header.message_id.buffer, session->header.message_id.len, &old_byte_from_message_id); + + struct aws_byte_buf old_alg_suite_data = session->header.alg_suite_data; + struct store_byte_from_buffer old_byte_from_alg_suite_data; + save_byte_from_array( + session->header.alg_suite_data.buffer, session->header.alg_suite_data.len, &old_byte_from_alg_suite_data); + + struct store_byte_from_buffer old_enc_ctx; + save_byte_from_hash_table(&session->header.enc_ctx, &old_enc_ctx); + + /* Operation under verification */ + __CPROVER_file_local_session_encrypt_c_sign_header(session); + + /* Assertions */ + assert(aws_cryptosdk_session_is_valid(session)); + assert_byte_buf_equivalence(&session->header.message_id, &old_message_id, &old_byte_from_message_id); + assert_byte_buf_equivalence(&session->header.alg_suite_data, &old_alg_suite_data, &old_byte_from_alg_suite_data); + check_hash_table_unchanged(&session->header.enc_ctx, &old_enc_ctx); +} diff --git a/verification/cbmc/sources/openssl/evp_override.c b/verification/cbmc/sources/openssl/evp_override.c index 82a57d68e..3681b32e1 100644 --- a/verification/cbmc/sources/openssl/evp_override.c +++ b/verification/cbmc/sources/openssl/evp_override.c @@ -789,7 +789,7 @@ int EVP_DigestInit(EVP_MD_CTX *ctx, const EVP_MD *type) { * on the same ctx to hash additional data. Return values: Returns 1 for success and 0 for failure. */ int EVP_DigestUpdate(EVP_MD_CTX *ctx, const void *d, size_t cnt) { - assert(evp_md_ctx_is_valid(ctx)); + assert(ctx != NULL); assert(d); assert(AWS_MEM_IS_READABLE(d, cnt)); diff --git a/verification/cbmc/stubs/hdr_write_stub.c b/verification/cbmc/stubs/hdr_write_stub.c new file mode 100644 index 000000000..b8435076b --- /dev/null +++ b/verification/cbmc/stubs/hdr_write_stub.c @@ -0,0 +1,45 @@ +/* + * 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 + +/** + * The original aws_cryptosdk_hdr_write function declares an aws_byte_buf + * output variable where different components of the header get written, + * however, the actual output of the function is bytes_written. Therefore, + * we assign a nondeterministic value to bytes_written in case of success + * or zero both outbuf and outlen in case of failure. + */ +int aws_cryptosdk_hdr_write( + const struct aws_cryptosdk_hdr *hdr, size_t *bytes_written, uint8_t *outbuf, size_t outlen) { + assert(aws_cryptosdk_hdr_is_valid(hdr)); + assert(hdr->iv.len <= UINT8_MAX); // uint8_t max value + assert(outlen == 0 || AWS_MEM_IS_READABLE(outbuf, outlen)); + assert(bytes_written != NULL); + + if (nondet_bool()) { + size_t nondet_size; + __CPROVER_assume(nondet_size < MAX_BUFFER_SIZE); + *bytes_written = nondet_size; + return AWS_OP_SUCCESS; + } else { + int error = nondet_bool() ? AWS_CRYPTOSDK_ERR_BAD_STATE : AWS_ERROR_SHORT_BUFFER; + aws_secure_zero(outbuf, outlen); + *bytes_written = 0; + return aws_raise_error(error); + } +}