Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Applies malloc flags across all CBMC proofs (#619)
* 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 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]> * 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]> Co-authored-by: Daniel Schwartz-Narbonne <[email protected]> Co-authored-by: Felipe R. Monteiro <[email protected]> Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>
- Loading branch information
