diff --git a/include/aws/cryptosdk/default_cmm.h b/include/aws/cryptosdk/default_cmm.h index fda388afc..8d1982d00 100644 --- a/include/aws/cryptosdk/default_cmm.h +++ b/include/aws/cryptosdk/default_cmm.h @@ -68,6 +68,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 diff --git a/source/default_cmm.c b/source/default_cmm.c index 558506750..fc3cdead0 100644 --- a/source/default_cmm.c +++ b/source/default_cmm.c @@ -28,7 +28,7 @@ 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; }; @@ -36,6 +36,10 @@ 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; @@ -54,6 +58,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; @@ -176,3 +181,11 @@ int aws_cryptosdk_default_cmm_set_alg_id(struct aws_cryptosdk_cmm *cmm, enum aws 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); +} diff --git a/verification/cbmc/include/make_common_data_structures.h b/verification/cbmc/include/make_common_data_structures.h index 02ef4298d..bc327a3bf 100644 --- a/verification/cbmc/include/make_common_data_structures.h +++ b/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); diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/Makefile index 70c636589..1337fc535 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/Makefile +++ b/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)) diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/aws_cryptosdk_keyring_on_encrypt_harness.c b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/aws_cryptosdk_keyring_on_encrypt_harness.c index 393c2e7f7..000c70771 100644 --- a/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/aws_cryptosdk_keyring_on_encrypt_harness.c +++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_on_encrypt/aws_cryptosdk_keyring_on_encrypt_harness.c @@ -26,18 +26,6 @@ #include #include -/** - * 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, @@ -45,40 +33,7 @@ int on_encrypt( 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. */ diff --git a/verification/cbmc/proofs/default_cmm_generate_enc_materials/Makefile b/verification/cbmc/proofs/default_cmm_generate_enc_materials/Makefile new file mode 100644 index 000000000..80474f858 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/verification/cbmc/proofs/default_cmm_generate_enc_materials/cbmc-batch.yaml b/verification/cbmc/proofs/default_cmm_generate_enc_materials/cbmc-batch.yaml new file mode 100644 index 000000000..e936b4599 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c b/verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c new file mode 100644 index 000000000..4c188d62c --- /dev/null +++ b/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 +#include +#include + +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)); +} diff --git a/verification/cbmc/sources/make_common_data_structures.c b/verification/cbmc/sources/make_common_data_structures.c index 76622c2ac..fcd59d39a 100644 --- a/verification/cbmc/sources/make_common_data_structures.c +++ b/verification/cbmc/sources/make_common_data_structures.c @@ -14,6 +14,7 @@ */ #include +#include #include #include #include @@ -31,6 +32,14 @@ #include #include +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; -} \ No newline at end of file +} + +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; +} diff --git a/verification/cbmc/stubs/on_encrypt_stub.c b/verification/cbmc/stubs/on_encrypt_stub.c new file mode 100644 index 000000000..7438a8e6e --- /dev/null +++ b/verification/cbmc/stubs/on_encrypt_stub.c @@ -0,0 +1,73 @@ +/* + * 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 + +/** + * 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); + } + return nondet_int(); +}