Adds CBMC proof for aws_cryptosdk_priv_try_gen_key

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);

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) {

source/session_encrypt.c

@@ -48,6 +48,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;
@@ -89,7 +93,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;
     }
@@ -169,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);

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

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 <aws/cryptosdk/materials.h>
+#include <cbmc_invariants.h>
+#include <cipher_openssl.h>
+#include <make_common_data_structures.h>
+#include <proof_helpers/cryptosdk/make_common_data_structures.h>
+#include <proof_helpers/make_common_data_structures.h>
+#include <proof_helpers/proof_allocators.h>
+#include <proof_helpers/utils.h>
+
+#include <aws/cryptosdk/private/cipher.h>
+#include <aws/cryptosdk/private/session.h>
+#include <aws/cryptosdk/session.h>
+
+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);
+}

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.

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));
 

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)

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));

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 <proof_helpers/make_common_data_structures.h>
+
+/*
+ * 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;
+    }
+}