Add CBMC proof for default_cmm_generate_enc_materials (#656)

* Add proof files for default_cmm_generate_enc_materials

* Move on_encrypt function to its own file

* Add validator and allocator functions
Change variable name and add comment for it on Makefile
Merge changes from 'master'

* Add and edit allocators for materials and cmm

* Add missing file to Makefile (algorithm_is_known)

* Remove unnecessary assumptions

* Edit preconditions and postconditions

* Fix style checks

* Restore simpler precondition

* Check that output remains unchanged (top-level check only)
Do intial allocation as usual and pass output by reference
Remove request_alg assertion in case of failure

* Fix style issues

* Use C-style comments and add space

* Remove unneeded assumptions and use nondet values
Replace precondition by false case in enc_request validator

* Remove copyright year on Makefile

include/aws/cryptosdk/default_cmm.h

@@ -70,6 +70,9 @@ struct aws_cryptosdk_cmm *aws_cryptosdk_default_cmm_new(struct aws_allocator *al
 AWS_CRYPTOSDK_API
 int aws_cryptosdk_default_cmm_set_alg_id(struct aws_cryptosdk_cmm *cmm, enum aws_cryptosdk_alg_id alg_id);
 
+AWS_CRYPTOSDK_API
+bool aws_cryptosdk_default_cmm_is_valid(const struct aws_cryptosdk_cmm *cmm);
+
 #ifdef __cplusplus
 }
 #endif

source/default_cmm.c

@@ -29,14 +29,18 @@ struct default_cmm {
     struct aws_cryptosdk_cmm base;
     struct aws_allocator *alloc;
     struct aws_cryptosdk_keyring *kr;
-    // Invariant: this is either DEFAULT_ALG_UNSET or is a valid algorithm ID
+    /* Invariant: this is either DEFAULT_ALG_UNSET or is a valid algorithm ID */
     enum aws_cryptosdk_alg_id default_alg;
 };
 
 static int default_cmm_generate_enc_materials(
     struct aws_cryptosdk_cmm *cmm,
     struct aws_cryptosdk_enc_materials **output,
     struct aws_cryptosdk_enc_request *request) {
+    AWS_PRECONDITION(aws_cryptosdk_default_cmm_is_valid(cmm));
+    AWS_PRECONDITION(output != NULL);
+    AWS_PRECONDITION(aws_cryptosdk_enc_request_is_valid(request));
+
     struct aws_cryptosdk_enc_materials *enc_mat = NULL;
     struct default_cmm *self                    = (struct default_cmm *)cmm;
     struct aws_hash_element *pElement           = NULL;
@@ -59,6 +63,7 @@ static int default_cmm_generate_enc_materials(
         }
     }
     const struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(request->requested_alg);
+    if (!props) goto err;
 
     enc_mat = aws_cryptosdk_enc_materials_new(request->alloc, request->requested_alg);
     if (!enc_mat) goto err;
@@ -180,3 +185,11 @@ int aws_cryptosdk_default_cmm_set_alg_id(struct aws_cryptosdk_cmm *cmm, enum aws
     self->default_alg = alg_id;
     return AWS_OP_SUCCESS;
 }
+
+bool aws_cryptosdk_default_cmm_is_valid(const struct aws_cryptosdk_cmm *cmm) {
+    if (cmm == NULL) return false;
+
+    struct default_cmm *self = (struct default_cmm *)cmm;
+    return aws_cryptosdk_cmm_base_is_valid(&self->base) && aws_allocator_is_valid(self->alloc) &&
+           aws_cryptosdk_keyring_is_valid(self->kr);
+}

verification/cbmc/include/make_common_data_structures.h

@@ -106,3 +106,12 @@ bool aws_cryptosdk_dec_materials_members_are_bounded(
 
 struct aws_cryptosdk_dec_materials *dec_materials_setup(
     const size_t max_trace_items, const size_t max_item_size, const size_t max_len);
+
+/* Allocates the members of the enc_request and ensures that internal pointers are pointing to the correct objects. */
+struct aws_cryptosdk_enc_request *ensure_enc_request_attempt_allocation(const size_t max_table_size);
+
+/* Allocates the members of the enc_materials and ensures that internal pointers are pointing to the correct objects. */
+struct aws_cryptosdk_enc_materials *ensure_enc_materials_attempt_allocation();
+
+/* Allocates the members of the default_cmm and ensures that internal pointers are pointing to the correct objects. */
+struct aws_cryptosdk_cmm *ensure_default_cmm_attempt_allocation(const struct aws_cryptosdk_keyring_vt *vtable);

verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/Makefile

@@ -63,6 +63,7 @@ PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_array_list_defined_type.c
 PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
+PROOF_SOURCES += $(PROOF_STUB)/on_encrypt_stub.c
 
 UNWINDSET += aws_cryptosdk_edk_list_elements_are_bounded.0:$(call addone,$(NUM_ELEMS))
 UNWINDSET += aws_cryptosdk_edk_list_elements_are_valid.0:$(call addone,$(NUM_ELEMS))

verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/aws_cryptosdk_keyring_on_encrypt_harness.c

@@ -26,59 +26,14 @@
 #include <proof_helpers/proof_allocators.h>
 #include <proof_helpers/utils.h>
 
-/**
- * Stub for the virtual function on_encrypt of a aws_cryptosdk_keyring_vt structure.
- * Must implement if used for encryption.
- * It should be as nondeterministic as possible to increase coverage on the operation under
- * verfication; thus, it also triggers states with errors.
- *
- * When the buffer for the unencrypted data key is not NULL at the time of the call, it
- * must not be changed by callee. All buffers for EDKs pushed onto the list must be in a
- * valid state, which means either that they are set to all zeroes or that they have been
- * initialized using one of the byte buffer initialization functions. This assures proper
- * clean up and serialization.
- */
 int on_encrypt(
     struct aws_cryptosdk_keyring *keyring,
     struct aws_allocator *request_alloc,
     struct aws_byte_buf *unencrypted_data_key,
     struct aws_array_list *keyring_trace,
     struct aws_array_list *edks,
     const struct aws_hash_table *enc_ctx,
-    enum aws_cryptosdk_alg_id alg) {
-    /* Check validity for all inputs to avoid memory-safety violations. */
-    assert(aws_cryptosdk_keyring_is_valid(keyring));
-    assert(aws_allocator_is_valid(request_alloc));
-    assert(aws_byte_buf_is_valid(unencrypted_data_key));
-    assert(aws_cryptosdk_keyring_trace_is_valid(keyring_trace));
-    assert(aws_cryptosdk_edk_list_is_valid(edks));
-    assert(aws_cryptosdk_edk_list_elements_are_valid(edks));
-    assert((enc_ctx == NULL) || aws_hash_table_is_valid(enc_ctx));
-
-    if (unencrypted_data_key->buffer == NULL) {
-        const struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg);
-        if (props != NULL) {
-            __CPROVER_assume(aws_byte_buf_is_bounded(unencrypted_data_key, props->data_key_len));
-            ensure_byte_buf_has_allocated_buffer_member(unencrypted_data_key);
-            /*
-             * This satisfies the post-condition that if this keyring
-             * generated data key, it must be the right length.
-             * The nondeterminism increases coverage.
-             */
-            if (nondet_bool()) unencrypted_data_key->len = props->data_key_len;
-            unencrypted_data_key->allocator = request_alloc;
-            __CPROVER_assume(aws_byte_buf_is_valid(unencrypted_data_key));
-        }
-    } else {
-        /*
-         * If the buffer is not NULL, the byte buffer must not have been modified;
-         * however, this allocation modifies the buffer and increases coverage.
-         */
-        if (nondet_bool()) ensure_byte_buf_has_allocated_buffer_member(unencrypted_data_key);
-    }
-    int ret;
-    return ret;
-}
+    enum aws_cryptosdk_alg_id alg);
 
 void aws_cryptosdk_keyring_on_encrypt_harness() {
     /* Non-deterministic inputs. */

verification/cbmc/proofs/default_cmm_generate_enc_materials/Makefile

@@ -0,0 +1,67 @@
+# 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
+#########
+# Local vars
+# Values are chosen for performance. Increasing them does not improve coverage.
+MAX_TABLE_SIZE ?= 1
+# In OBJ_txt2nid, this value unwinds strcmp(s, "prime256v1")
+PRIME_STRING_LEN=10
+#########
+PROOF_UID = default_cmm_generate_enc_materials
+HARNESS_ENTRY = $(PROOF_UID)_harness
+HARNESS_FILE = $(HARNESS_ENTRY).c
+
+CBMCFLAGS +=
+
+DEFINES += -DMAX_TABLE_SIZE=$(MAX_TABLE_SIZE)
+
+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/encoding.c
+PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/error.c
+PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/hash_table.c
+PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/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/objects_override.c
+PROJECT_SOURCES += $(SRCDIR)/source/cipher.c
+PROJECT_SOURCES += $(SRCDIR)/source/cipher_openssl.c
+PROJECT_SOURCES += $(SRCDIR)/source/default_cmm.c
+PROJECT_SOURCES += $(SRCDIR)/source/edk.c
+PROJECT_SOURCES += $(SRCDIR)/source/header.c
+PROJECT_SOURCES += $(SRCDIR)/source/keyring_trace.c
+PROJECT_SOURCES += $(SRCDIR)/source/materials.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_hash_table_no_slots_override.c
+PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_string_destroy_override.c
+PROOF_SOURCES += $(COMMON_PROOF_STUB)/error.c
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
+PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_invariants.c
+PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
+PROOF_SOURCES += $(PROOF_STUB)/aws_base64_encode.c
+PROOF_SOURCES += $(PROOF_STUB)/on_encrypt_stub.c
+
+UNWINDSET +=  strcmp.0:$(call addone,$(PRIME_STRING_LEN))
+###########
+include ../Makefile.common

verification/cbmc/proofs/default_cmm_generate_enc_materials/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/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

@@ -0,0 +1,67 @@
+/*
+ * Copyright 2019 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/default_cmm.h>
+#include <aws/cryptosdk/materials.h>
+#include <make_common_data_structures.h>
+
+int on_encrypt(
+    struct aws_cryptosdk_keyring *keyring,
+    struct aws_allocator *request_alloc,
+    struct aws_byte_buf *unencrypted_data_key,
+    struct aws_array_list *keyring_trace,
+    struct aws_array_list *edks,
+    const struct aws_hash_table *enc_ctx,
+    enum aws_cryptosdk_alg_id alg);
+
+void default_cmm_generate_enc_materials_harness() {
+    const struct aws_cryptosdk_keyring_vt vtable = { .vt_size    = nondet_size_t(),
+                                                     .name       = ensure_c_str_is_allocated(SIZE_MAX),
+                                                     .destroy    = nondet_voidp(),
+                                                     .on_encrypt = nondet_bool() ? NULL : on_encrypt,
+                                                     .on_decrypt = nondet_voidp() };
+    /* Nondet input */
+    struct aws_cryptosdk_cmm *cmm              = ensure_default_cmm_attempt_allocation(&vtable);
+    struct aws_cryptosdk_enc_materials *output = ensure_enc_materials_attempt_allocation();
+    struct aws_cryptosdk_enc_request *request  = ensure_enc_request_attempt_allocation(MAX_TABLE_SIZE);
+
+    /* Assumptions */
+    __CPROVER_assume(aws_cryptosdk_default_cmm_is_valid(cmm));
+
+    __CPROVER_assume(output != NULL);
+
+    __CPROVER_assume(aws_cryptosdk_enc_request_is_valid(request));
+
+    /* Save current state of the data structures */
+    struct store_byte_from_buffer old_output;
+    save_byte_from_array((uint8_t *)output, sizeof(*output), &old_output);
+
+    /* Operation under verification */
+    if (__CPROVER_file_local_default_cmm_c_default_cmm_generate_enc_materials(cmm, &output, request) ==
+        AWS_OP_SUCCESS) {
+        assert(aws_cryptosdk_enc_materials_is_valid(output));
+        assert(aws_cryptosdk_algorithm_is_known(request->requested_alg));
+    } else {
+        /* Note that we perform a top-level comparison here */
+        assert_byte_from_buffer_matches((uint8_t *)output, &old_output);
+    }
+
+    /* Postconditions */
+    assert(aws_cryptosdk_default_cmm_is_valid(cmm));
+    assert(aws_cryptosdk_enc_request_is_valid(request));
+}

verification/cbmc/sources/make_common_data_structures.c

@@ -14,6 +14,7 @@
  */
 
 #include <aws/cryptosdk/cipher.h>
+#include <aws/cryptosdk/default_cmm.h>
 #include <aws/cryptosdk/keyring_trace.h>
 #include <aws/cryptosdk/materials.h>
 #include <aws/cryptosdk/private/header.h>
@@ -31,6 +32,14 @@
 #include <proof_helpers/make_common_data_structures.h>
 #include <proof_helpers/proof_allocators.h>
 
+struct default_cmm {
+    struct aws_cryptosdk_cmm base;
+    struct aws_allocator *alloc;
+    struct aws_cryptosdk_keyring *kr;
+    /* Invariant: this is either DEFAULT_ALG_UNSET or is a valid algorithm ID */
+    enum aws_cryptosdk_alg_id default_alg;
+};
+
 const EVP_MD *nondet_EVP_MD_ptr(void);
 const EVP_CIPHER *nondet_EVP_CIPHER_ptr(void);
 
@@ -346,6 +355,7 @@ bool aws_cryptosdk_dec_materials_members_are_bounded(
     }
     return true;
 }
+
 struct aws_cryptosdk_dec_materials *ensure_dec_materials_attempt_allocation() {
     struct aws_cryptosdk_dec_materials *materials = malloc(sizeof(struct aws_cryptosdk_dec_materials));
     if (materials) {
@@ -369,4 +379,51 @@ struct aws_cryptosdk_dec_materials *dec_materials_setup(
     }
     __CPROVER_assume(aws_cryptosdk_dec_materials_is_valid(materials));
     return materials;
-}
+}
+
+struct aws_cryptosdk_enc_request *ensure_enc_request_attempt_allocation(const size_t max_table_size) {
+    struct aws_cryptosdk_enc_request *request = malloc(sizeof(struct aws_cryptosdk_enc_request));
+    if (request) {
+        request->alloc   = nondet_bool() ? NULL : can_fail_allocator();
+        request->enc_ctx = malloc(sizeof(struct aws_hash_table));
+        if (request->enc_ctx) {
+            ensure_allocated_hash_table(request->enc_ctx, max_table_size);
+        }
+    }
+    return request;
+}
+
+struct aws_cryptosdk_enc_materials *ensure_enc_materials_attempt_allocation() {
+    struct aws_cryptosdk_enc_materials *materials = malloc(sizeof(struct aws_cryptosdk_enc_materials));
+    if (materials) {
+        materials->alloc   = nondet_bool() ? NULL : can_fail_allocator();
+        materials->signctx = ensure_nondet_sig_ctx_has_allocated_members();
+        ensure_byte_buf_has_allocated_buffer_member(&materials->encrypted_data_keys);
+        ensure_array_list_has_allocated_data_member(&materials->keyring_trace);
+        ensure_array_list_has_allocated_data_member(&materials->encrypted_data_keys);
+    }
+    return materials;
+}
+
+struct aws_cryptosdk_cmm *ensure_default_cmm_attempt_allocation(const struct aws_cryptosdk_keyring_vt *vtable) {
+    /* Nondet input required to init cmm */
+    struct aws_cryptosdk_keyring *keyring = malloc(sizeof(*keyring));
+
+    /* Assumptions required to init cmm */
+    ensure_cryptosdk_keyring_has_allocated_members(keyring, vtable);
+    __CPROVER_assume(aws_cryptosdk_keyring_is_valid(keyring));
+    __CPROVER_assume(keyring->vtable != NULL);
+
+    struct aws_cryptosdk_cmm *cmm = malloc(sizeof(struct default_cmm));
+    if (cmm) {
+        cmm->vtable = vtable;
+    }
+
+    struct default_cmm *self = NULL;
+    if (cmm) {
+        self        = (struct default_cmm *)cmm;
+        self->alloc = nondet_bool() ? NULL : can_fail_allocator();
+        self->kr    = keyring;
+    }
+    return (struct aws_cryptosdk_cmm *)self;
+}