Adds CBMC proof for sign_header

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(session != NULL);
+    AWS_PRECONDITION(aws_allocator_is_valid(session->alloc));
+    AWS_PRECONDITION(aws_cryptosdk_hdr_is_valid(&session->header));
+    AWS_PRECONDITION(aws_cryptosdk_sig_ctx_is_valid(session->signctx));
+    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) {
+        assert(session->header.iv.buffer);
+        memset(session->header.iv.buffer, 0x42, session->header.iv.len);
+    }
+    if (session->header.auth_tag.len) {
+        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) {
+            assert(session->header.iv.buffer);
+            memcpy(session->header.iv.buffer, authtag.buffer, session->header.iv.len);
+        }
+        if (session->header.auth_tag.len) {
+            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) {
+            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

verification/cbmc/proofs/sign_header/Makefile

@@ -0,0 +1,109 @@
+# 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
+
+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_EDK_LIST_ITEMS ?= 1
+MAX_TABLE_SIZE ?= 2
+MAX_IV_LEN ?= 12
+
+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_IV_LEN=$(MAX_IV_LEN)
+DEFINES += -DAWS_CRYPTOSDK_HASH_ELEMS_ARRAY_INIT_GENERATOR=array_list_item_generator
+
+# 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/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)/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/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
+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:$(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_hdr_write.0:$(call addone,$(MAX_EDK_LIST_ITEMS)) 
+UNWINDSET += ensure_cryptosdk_edk_list_has_allocated_list_elements.0:$(call addone,$(MAX_EDK_LIST_ITEMS))
+UNWINDSET += memcmp.0:$(call addone,$(MAX_BUFFER_SIZE))
+
+include ../Makefile.common

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.

verification/cbmc/proofs/sign_header/sign_header_harness.c

@@ -0,0 +1,99 @@
+/*
+ * 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 line 33 of 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 = malloc(sizeof(*session));
+
+    /* Assumptions */
+    __CPROVER_assume(session != NULL);
+
+    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));
+
+    __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_cryptosdk_sig_ctx *ctx = ensure_nondet_sig_ctx_has_allocated_members();
+    __CPROVER_assume(aws_cryptosdk_sig_ctx_is_valid_cbmc(ctx));
+    session->signctx = ctx;
+
+    __CPROVER_assume(aws_allocator_is_valid(session->alloc));
+    __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_hdr_is_valid(&session->header));
+    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);
+}