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 <[email protected]> Co-authored-by: Alex Chew <[email protected]> Co-authored-by: Adrian Palacios <[email protected]> Co-authored-by: Adrian Palacios <[email protected]>
aws · Jan 11, 2021 · f2e9593 · f2e9593
1 parent 3db1aee
commit f2e9593
Show file tree

Hide file tree

Showing 8 changed files with 267 additions and 16 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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.
diff --git a/verification/cbmc/proofs/sign_header/sign_header_harness.c 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 <aws/cryptosdk/private/cipher.h>
+#include <aws/cryptosdk/private/session.h>
+#include <aws/cryptosdk/session.h>
+#include <cbmc_invariants.h>
+#include <make_common_data_structures.h>
+#include <proof_helpers/make_common_data_structures.h>
+
+/**
+ * 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
@@ -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
@@ -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 <aws/cryptosdk/private/header.h>
+
+#include <proof_helpers/make_common_data_structures.h>
+
+/**
+ * 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);
+    }
+}