Update Makefile.common with malloc-may-fail and malloc-fail-null (#618)

* Removes extra flags from coverage check (#617)

Signed-off-by: Felipe R. Monteiro <[email protected]>

* Improves coverage for the aws_cryptosdk_md_* proofs  (#616)

* Added READMEs documenting expected coverage for aws_cryptosdk_md_update and aws_cryptosdk_md_abort

* Added stubs for EVP_MD_CTX_free and evp_md_ctx_is_valid to be used when ctx->pkey is sure to be NULL

* Updated Makefile to use new stubs for EVP_MD_XTX_free and evp_md_ctx_is_valid to improve coverage

* Updated README.md files with new expected coverage

* Use AWS_FATAL_PRECONDITION instead of abort

* Updated Makefiles with stubs for aws_raise_error_private, EVP_MD_CTX_free and evp_md_ctx_is_valid

* Added README files specifying expected coverage behavior

* Empty commit to run tests

* Empty commit to run tests

* More descriptive names for stubs and added documentation to Makefile

* Added additional documentation to Makefile and updated stub names

* Added more information about unreached lines of code

* Moved struct definitions for evp_md_ctx_st and evp_pkey_st to evp.h

* Use AWS_FATAL_PRECONDITION instead of abort

* Updated Makefiles with stubs for aws_raise_error_private, EVP_MD_CTX_free and evp_md_ctx_is_valid

* Added README files specifying expected coverage behavior

* Added additional documentation to Makefile and updated stub names

* Added more information about unreached lines of code

* Re-ordered structs in evp.h and fixed comments

* remove extra line

* Removed unneeded includes and cleaned comments

* made pkey == NULL into an assert

* Remove unnecessary READMEs for proofs with full coverage

* Added comments about abstractions and removed REMOVE_FUNCTION_BODIES

* Use AWS_FATAL_PRECONDITION instead of abort

* Updated Makefiles with stubs for aws_raise_error_private, EVP_MD_CTX_free and evp_md_ctx_is_valid

* Added README files specifying expected coverage behavior

* Added additional documentation to Makefile and updated stub names

* Added more information about unreached lines of code

* Removed extra line in Makefiles

* Remove README for function with full coverage

* Removed redition of struct from stubs

* empty commit to rerun tests

* Simplified includes for stubs

* Trigger CI

* Trigger stuck CI

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>
Co-authored-by: Felipe R. Monteiro <[email protected]>

* Make c-common a submodule for verification, and update the CBMC makefile to point at it

* Updated proofs harnesses for aws_cryptosdk_rsa_encrypt and decrypt (#603)

* Make c-common a submodule for verification, and update the CBMC makefile to point at it

* Update c-common to latest, and update the makefile to match

* fixed keyring_trace_add_record_buf and keyring_on_encrypt

* push c-common again, and fix makefile for aws_gcm_decypt

* Updated harneses with explicit non-NULL assumptions to handle may-fail-malloc flag

Added preconditions to source code

* Use new string allocators and add matching preconditions to harness

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

* Updates to aws_atomic_var_is_valid and aws_cryptosdk_keyring_base_init harness (#607)

* Make c-common a submodule for verification, and update the CBMC makefile to point at it

* Update c-common to latest, and update the makefile to match

* fixed keyring_trace_add_record_buf and keyring_on_encrypt

* push c-common again, and fix makefile for aws_gcm_decypt

* Added non-NULL assumptions to keyring_base_init harness for vtable name

modified aws_atomic_var_is_valid check

Fixed IMPLIES structure of assume

Fix comment structure in cmm_base_init harness

aws_atomic_var_is_valid divided into two functions, one for int and one for ptr, preconditions added to source code

Updated Makefile to include MAX_STRING_LEN

update to keyring_on_encrypt and keyring_on_decrypt proof harnesses

* Added the ensure_vtable_has_allocated_members function

* Use ensures function in the harness as well as bounded malloc

* removed unneeded assumption on refcount.value

* Removed stubs from Makefile

* use malloc and ensure_vtable_has_allocated_members

* Use new ensure_nondet_allocate_vtable_members function

* Made two vtable allocator functions, for keyring_trace and cmm

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

* Update harness for aws_cryptosdk_enc_ctx_clone (#611)

* Make c-common a submodule for verification, and update the CBMC makefile to point at it

* Update c-common to latest, and update the makefile to match

* fixed keyring_trace_add_record_buf and keyring_on_encrypt

* push c-common again, and fix makefile for aws_gcm_decypt

* Update enc_ctx_clone harness and Makefile, additional assumptions, needs new stubs from aws-c-common

* Updated harness to use malloc

* update time in Makefile and remove unneeded assumptions

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

* Update to aws_cryptosdk_enc_ctx_size proof (#608)

* Make c-common a submodule for verification, and update the CBMC makefile to point at it

* Update c-common to latest, and update the makefile to match

* fixed keyring_trace_add_record_buf and keyring_on_encrypt

* push c-common again, and fix makefile for aws_gcm_decypt

* Updated harness for enc_ctx_size and added non-NULL assumptions

* Malloc data structures and then assume non-NULL

* Use aws_string_is_valid and added preconditions to source code

* Updated conditions in the function to asserts

* include missing assert header

* size becomes *size

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

* Update CBMC harnesses for aws_cryptosdk_enc_ctx_serialize, aws_cryptosdk_sig_sign_start and aws_cryptosdk_sig_get_privkey (#606)

* Make c-common a submodule for verification, and update the CBMC makefile to point at it

* Update c-common to latest, and update the makefile to match

* fixed keyring_trace_add_record_buf and keyring_on_encrypt

* push c-common again, and fix makefile for aws_gcm_decypt

* Simple cleanup of sig_get_privkey harness

Added explicit non-NULL instructions to sig_sign_start harness

Added explicit non-NULL assumptions to the key and value fiends of each array_list_element in enc_ctx_serialize harness

Added corresponding preconditions to source code functions

* Added ensure_sig_ctx_has_allocated_members function and harness updates

* Updated preconditions in the source code

* Updated other harnesses to use the new ensure_sig_ctx_has_allocated_members function

* Use malloc

* rename of ensure_sig_ctx_has_allocated_members function

* change function name

* Update to aws_cryptosdk_dec_materials_destroy and enc_material_destroy harnesses

* fixes

* Added precondition to source code

* remove memory leak check from Makefile

remove memory clean up

moved assumptions about non-NULL elems

remove memory leak check from .yaml

Added comment about non-NULL assumption in hash_elems

* Removed too strong assumption about privkey

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

* Updates aws_cryptosdk_keyring_trace_copy_all proof  (#609)

* Make c-common a submodule for verification, and update the CBMC makefile to point at it

* Update c-common to latest, and update the makefile to match

* fixed keyring_trace_add_record_buf and keyring_on_encrypt

* push c-common again, and fix makefile for aws_gcm_decypt

* Updated harness for keyring_trace_copy_all to handle new malloc-may-fail flag

Added new ensure_trace_has_readable_records function

Updated Makefile with loop unwinding

Added preconditions to source code

update to new c-common

revert to old aws-c-common

* Use malloc instead of can-fail

* update to recent c common to see if proof will go through CI

* use the aws_cryptosdk_keyring_trace_is_valid function and update yaml

* remove extra function from make_common_datastructures

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

* Update aws_cryptodsk_sig_verify_start and aws_cryptodsk_sig_verify_finish harnesses (#602)

* Make c-common a submodule for verification, and update the CBMC makefile to point at it

* Updated assumptions in proof harnesses to handle malloc-may-fail

Updated preconditions in source code to match those in harness

* updates and use the ensure_sig_ctx_has_allocated_members function

* Added is_valid assumptions to source code

* update signature

* Simple cleanup of sig_get_privkey harness

Added explicit non-NULL instructions to sig_sign_start harness

Added explicit non-NULL assumptions to the key and value fiends of each array_list_element in enc_ctx_serialize harness

Added corresponding preconditions to source code functions

* Added ensure_sig_ctx_has_allocated_members function and harness updates

* Updated preconditions in the source code

* Remove un-needed assumptions

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

* Update Makefile.common with -malloc-may-fail and ---malloc-fail-null flags

* Update harnesses for keyring_trace_add_record, keyring_trace_add_record_c_str and aws_cryptosdk_keyring_trace_record_init_clone (#604)

* Make c-common a submodule for verification, and update the CBMC makefile to point at it

* Update c-common to latest, and update the makefile to match

* fixed keyring_trace_add_record_buf and keyring_on_encrypt

* push c-common again, and fix makefile for aws_gcm_decypt

* Update harnesses with non-NULL assumptions on strings

Added non-NULL assumptions on strings to harness

* Updated harnesses to use is_valid assumptions, new c-common allocation functions and matched preconditions in the source code

* Use ensure_string_is_allocated_nondet_length for record_init_clone and assumption on length

* Fixed changes to ensure_record_has_allocated_members

* Fixed broken proofs due to changes in c-common not addressed in other PRs

* update harness for string_dup and compare_hash_elems_by_key_string

* Update to c-common

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

* Update harness for edk_list_copy_all (#610)

* Make c-common a submodule for verification, and update the CBMC makefile to point at it

* Update c-common to latest, and update the makefile to match

* fixed keyring_trace_add_record_buf and keyring_on_encrypt

* push c-common again, and fix makefile for aws_gcm_decypt

* Added the ensure_cryptosdk_edk_list_elements_are_readable function

Updated edk_list_copy_all harness with assumptions for the malloc-may-fail flag

Added to unwindset

Added preconditions to source code

* use malloc

* Update to use aws_cryptosdk_edk_list_elements_are_valid

Updated signature for clean up and init stubs

Updated signature for clean up and init stubs

add yaml

Update signature for clean_up and init_clone

* Update Makefile

* Update to new c-common and remove un-needed function

* set NUM_ELEMS to 1 just to test

* Stub out aws_array_list_push_back and aws_array_list_pop_back

* Updated time comment in Makefile

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

* Pushing new yamls and updating Makefile

* Update Makefiles for enc_materials_new and dec_materials_new and harness for enc_ctx_deserialize

* update c-common

Co-authored-by: Felipe R. Monteiro <[email protected]>
Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>
Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

.cbmc-batch/include/openssl/evp.h

@@ -17,14 +17,27 @@
 #ifndef HEADER_EVP_H
 #define HEADER_EVP_H
 
-#include <stddef.h>
-
 #include <openssl/ec.h>
 #include <openssl/ossl_typ.h>
+#include <stdbool.h>
+#include <stddef.h>
 
 #define EVP_MAX_MD_SIZE 64  /* longest known is SHA512 */
 #define EVP_PKEY_HKDF 1036  // reference from obj_mac.h
 
+/* Abstraction of the EVP_PKEY struct. */
+struct evp_pkey_st {
+    int references;
+    EC_KEY *ec_key;
+};
+
+/* Abstraction of the EVP_MD_CTX struct. */
+struct evp_md_ctx_st {
+    bool is_initialized;
+    EVP_PKEY *pkey;
+    size_t digest_size;
+};
+
 EVP_PKEY *EVP_PKEY_new(void);
 EC_KEY *EVP_PKEY_get0_EC_KEY(EVP_PKEY *pkey);
 int EVP_PKEY_set1_EC_KEY(EVP_PKEY *pkey, EC_KEY *key);

.cbmc-batch/jobs/Makefile.common

@@ -48,26 +48,28 @@ CBMC_VERBOSITY ?= ""
 CBMCFLAGS += --flush
 
 #error checking
-CBMCFLAGS += --bounds-check
-CBMCFLAGS += --conversion-check
-CBMCFLAGS += --div-by-zero-check
-#CBMCFLAGS += --enum-range-check
-CBMCFLAGS += --float-overflow-check
-CBMCFLAGS += --nan-check
-CBMCFLAGS += --pointer-check
-CBMCFLAGS += --pointer-overflow-check
-CBMCFLAGS += --pointer-primitive-check
-CBMCFLAGS += --signed-overflow-check
-CBMCFLAGS += --undefined-shift-check
-CBMCFLAGS += --unsigned-overflow-check
-CBMCFLAGS += --unwind 1
-CBMCFLAGS += --unwinding-assertions
-
+CHECKFLAGS += --bounds-check
+CHECKFLAGS += --conversion-check
+CHECKFLAGS += --div-by-zero-check
+#CHECKFLAGS += --enum-range-check
+CHECKFLAGS += --float-overflow-check
+CHECKFLAGS += --nan-check
+CHECKFLAGS += --pointer-check
+CHECKFLAGS += --pointer-overflow-check
+CHECKFLAGS += --pointer-primitive-check
+CHECKFLAGS += --signed-overflow-check
+CHECKFLAGS += --undefined-shift-check
+CHECKFLAGS += --unsigned-overflow-check
+CHECKFLAGS += --unwinding-assertions
+CHECKFLAGS += --malloc-may-fail
+CHECKFLAGS += --malloc-fail-null
+
+CBMCFLAGS += $(CHECKFLAGS)
 
 ################################################################
 # Preprocess the unwindset
 ifneq ($(UNWINDSET),)
-CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET)))
+CBMC_UNWINDSET := --unwind 1 --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET)))
 endif
 CBMCFLAGS += $(CBMC_UNWINDSET)
 
@@ -276,7 +278,7 @@ property.xml: $(ENTRY).goto
 	cbmc $(CBMCFLAGS) --show-properties --xml-ui $< 2>&1 > $@
 
 coverage.xml: $(ENTRY).goto
-	cbmc $(filter-out --unwinding-assertions,$(CBMCFLAGS)) --cover location --xml-ui $< 2>&1 > $@
+	cbmc $(filter-out $(CHECKFLAGS),$(CBMCFLAGS)) --malloc-may-fail --malloc-fail-null --cover location --xml-ui $< 2>&1 > $@
 
 cbmc: cbmc.log
 

.cbmc-batch/jobs/aws_cryptosdk_aes_gcm_decrypt/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-jobos: ubuntu16
-cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;flush_openssl_errors.0:1;--object-bits;8"
-goto: aws_cryptosdk_aes_gcm_decrypt_harness.goto
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;flush_openssl_errors.0:1;--object-bits;8"
 expected: "SUCCESSFUL"
+goto: aws_cryptosdk_aes_gcm_decrypt_harness.goto
+jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_aes_gcm_encrypt/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-jobos: ubuntu16
-cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;flush_openssl_errors.0:1;--object-bits;8"
-goto: aws_cryptosdk_aes_gcm_encrypt_harness.goto
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;flush_openssl_errors.0:1;--object-bits;8"
 expected: "SUCCESSFUL"
+goto: aws_cryptosdk_aes_gcm_encrypt_harness.goto
+jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_alg_props/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-cbmcflags: "--flush;--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
 expected: "SUCCESSFUL"
 goto: aws_cryptosdk_alg_props_harness.goto
 jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_cmm_base_init/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-jobos: ubuntu16
-cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
-goto: aws_cryptosdk_cmm_base_init_harness.goto
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
 expected: "SUCCESSFUL"
+goto: aws_cryptosdk_cmm_base_init_harness.goto
+jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_cmm_decrypt_materials/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8"
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8"
 expected: "SUCCESSFUL"
 goto: aws_cryptosdk_cmm_decrypt_materials_harness.goto
 jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_cmm_generate_enc_materials/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8"
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_edk_list_clear.0:2,aws_cryptosdk_edk_list_elements_are_bounded.0:2,aws_cryptosdk_edk_list_elements_are_valid.0:2,aws_cryptosdk_edk_list_is_bounded.0:2,aws_cryptosdk_edk_list_is_valid.0:2,aws_cryptosdk_keyring_trace_clear.0:2,aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:2,ensure_cryptosdk_edk_list_has_allocated_members.0:2,ensure_trace_has_allocated_records.0:2;--object-bits;8"
 expected: "SUCCESSFUL"
 goto: aws_cryptosdk_cmm_generate_enc_materials_harness.goto
 jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_cmm_release/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
 expected: "SUCCESSFUL"
 goto: aws_cryptosdk_cmm_release_harness.goto
 jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_cmm_retain/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-jobos: ubuntu16
-cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
-goto: aws_cryptosdk_cmm_retain_harness.goto
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
 expected: "SUCCESSFUL"
+goto: aws_cryptosdk_cmm_retain_harness.goto
+jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_compare_hash_elems_by_key_string/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;memcmp.0:17;--object-bits;8"
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwindset;memcmp.0:17;--object-bits;8"
 expected: "SUCCESSFUL"
 goto: aws_cryptosdk_compare_hash_elems_by_key_string_harness.goto
 jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_dec_materials_destroy/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_trace_has_allocated_records.0:2,aws_cryptosdk_keyring_trace_clear.0:2;--object-bits;8"
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:2,ensure_trace_has_allocated_records.0:2,aws_cryptosdk_keyring_trace_clear.0:2;--object-bits;8"
 expected: "SUCCESSFUL"
 goto: aws_cryptosdk_dec_materials_destroy_harness.goto
 jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_dec_materials_new/Makefile

@@ -22,6 +22,7 @@ include ../Makefile.string
 #########
 # Local vars
 # Expected runtime 2min
+KEYRING_TRACE_SIZE = 10 # Value is hardcoded in aws_cryptosdk_keyring_trace_init
 
 #########
 ABSTRACTIONS += $(SRCDIR)/c-common-helper-stubs/error.c
@@ -50,5 +51,6 @@ DEPENDENCIES += $(SRCDIR)/c-common-helper-uninline/atomics.c
 
 ENTRY = aws_cryptosdk_dec_materials_new_harness
 
+UNWINDSET += aws_cryptosdk_keyring_trace_is_valid.0:$(shell echo $$(($(KEYRING_TRACE_SIZE) + 1)))
 ###########
 include ../Makefile.common

.cbmc-batch/jobs/aws_cryptosdk_dec_materials_new/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_keyring_trace_is_valid.0:11;--object-bits;8"
 expected: "SUCCESSFUL"
 goto: aws_cryptosdk_dec_materials_new_harness.goto
 jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_decrypt_body/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;aws_cryptosdk_decrypt_body.0:5,strlen.0:37;--object-bits;8"
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_decrypt_body.0:5,strlen.0:37;--object-bits;8"
 expected: "SUCCESSFUL"
 goto: aws_cryptosdk_decrypt_body_harness.goto
 jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_derive_key/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-cbmcflags: "--flush;--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
 expected: "SUCCESSFUL"
 goto: aws_cryptosdk_derive_key_harness.goto
 jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_deserialize_frame/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-jobos: ubuntu16
-cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
-goto: aws_cryptosdk_deserialize_frame_harness.goto
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
 expected: "SUCCESSFUL"
+goto: aws_cryptosdk_deserialize_frame_harness.goto
+jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_edk_clean_up/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-jobos: ubuntu16
-cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
-goto: aws_cryptosdk_edk_clean_up_harness.goto
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
 expected: "SUCCESSFUL"
+goto: aws_cryptosdk_edk_clean_up_harness.goto
+jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_edk_eq/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-jobos: ubuntu16
-cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
-goto: aws_cryptosdk_edk_eq_harness.goto
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
 expected: "SUCCESSFUL"
+goto: aws_cryptosdk_edk_eq_harness.goto
+jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_edk_init_clone/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-jobos: ubuntu16
-cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
-goto: aws_cryptosdk_edk_init_clone_harness.goto
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--object-bits;8"
 expected: "SUCCESSFUL"
+goto: aws_cryptosdk_edk_init_clone_harness.goto
+jobos: ubuntu16

.cbmc-batch/jobs/aws_cryptosdk_edk_list_clean_up/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-cbmcflags: "--flush;--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;aws_cryptosdk_edk_list_clear.0:3,aws_cryptosdk_edk_list_elements_are_bounded.0:3,aws_cryptosdk_edk_list_elements_are_valid.0:3,aws_cryptosdk_edk_list_is_bounded.0:3,aws_cryptosdk_edk_list_is_valid.0:3,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:3,ensure_cryptosdk_edk_list_has_allocated_members.0:3;--object-bits;8"
+cbmcflags: "--flush;--bounds-check;--conversion-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwinding-assertions;--malloc-may-fail;--malloc-fail-null;--unwind;1;--unwindset;aws_cryptosdk_edk_list_clear.0:3,aws_cryptosdk_edk_list_elements_are_bounded.0:3,aws_cryptosdk_edk_list_elements_are_valid.0:3,aws_cryptosdk_edk_list_is_bounded.0:3,aws_cryptosdk_edk_list_is_valid.0:3,ensure_cryptosdk_edk_list_has_allocated_list_elements.0:3,ensure_cryptosdk_edk_list_has_allocated_members.0:3;--object-bits;8"
 expected: "SUCCESSFUL"
 goto: aws_cryptosdk_edk_list_clean_up_harness.goto
 jobos: ubuntu16