diff --git a/source/default_cmm.c b/source/default_cmm.c index eb320a5ef..0217213a0 100644 --- a/source/default_cmm.c +++ b/source/default_cmm.c @@ -37,6 +37,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(cmm != NULL); + 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; 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..d2a5ae33b --- /dev/null +++ b/verification/cbmc/proofs/default_cmm_generate_enc_materials/Makefile @@ -0,0 +1,68 @@ +# 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. + +######### +# 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 +MAX_NUM_ITEMS ?= 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_NUM_ITEMS=$(MAX_NUM_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/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/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 + +REMOVE_FUNCTION_BODY += aws_base64_encode + +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..984935a6a --- /dev/null +++ b/verification/cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c @@ -0,0 +1,116 @@ +/* + * 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) { + /* 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; +} + +void default_cmm_generate_enc_materials_harness() { + /* Nondet input required to init cmm */ + struct aws_cryptosdk_keyring *keyring = malloc(sizeof(*keyring)); + const struct aws_cryptosdk_keyring_vt vtable = { .vt_size = sizeof(struct aws_cryptosdk_keyring_vt), + .name = ensure_c_str_is_allocated(SIZE_MAX), + .destroy = nondet_voidp(), + .on_encrypt = nondet_bool() ? NULL : on_encrypt, + .on_decrypt = nondet_voidp() }; + /* 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); + + /* Nondet input */ + struct aws_cryptosdk_cmm *cmm = aws_cryptosdk_default_cmm_new(can_fail_allocator(), keyring); + struct aws_cryptosdk_enc_materials **output = malloc(sizeof(*output)); + struct aws_cryptosdk_enc_request *request = malloc(sizeof(*request)); + + /* Assumptions */ + __CPROVER_assume(cmm != NULL); + + __CPROVER_assume(output != NULL); + + __CPROVER_assume(request != NULL); + request->alloc = can_fail_allocator(); + __CPROVER_assume(aws_allocator_is_valid(request->alloc)); + request->enc_ctx = malloc(sizeof(*request->enc_ctx)); + __CPROVER_assume(request->enc_ctx != NULL); + ensure_allocated_hash_table(request->enc_ctx, MAX_NUM_ITEMS); + __CPROVER_assume(aws_cryptosdk_enc_request_is_valid(request)); + + enum aws_cryptosdk_alg_id alg_id; + if (nondet_bool()) request->requested_alg = alg_id; + // We can either add this OR add "if (!props) goto err;" after line 61 in the source code + // I think adding the check to the source code is better in this case. + // struct aws_cryptosdk_alg_properties *alg_props = aws_cryptosdk_alg_props(alg_id); + // __CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(alg_props)); + + /* Nondet set self->default_alg to a valid alg_id */ + __CPROVER_assume(aws_cryptosdk_default_cmm_set_alg_id(cmm, alg_id) == AWS_OP_SUCCESS); + + /* 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)); + } else { + assert(*output == NULL); + } + + /* Postconditions */ + assert(aws_cryptosdk_cmm_base_is_valid(cmm)); + assert(aws_cryptosdk_enc_request_is_valid(request)); +}