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
aws · Dec 21, 2020 · face741 · face741
1 parent ae10685
commit face741
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 8 deletions.
diff --git a/...mc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c b/...mc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c
@@ -20,8 +20,6 @@
 #include <aws/cryptosdk/materials.h>
 #include <make_common_data_structures.h>
 
-#define DEFAULT_ALG_UNSET 0xFFFF
-
 int on_encrypt(
     struct aws_cryptosdk_keyring *keyring,
     struct aws_allocator *request_alloc,
@@ -39,7 +37,7 @@ void default_cmm_generate_enc_materials_harness() {
                                                      .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_materials *output = ensure_enc_materials_attempt_allocation();
     struct aws_cryptosdk_enc_request *request   = ensure_enc_request_attempt_allocation(MAX_TABLE_SIZE);
 
     /* Assumptions */
@@ -53,14 +51,17 @@ void default_cmm_generate_enc_materials_harness() {
     __CPROVER_assume(request->enc_ctx != 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));
+    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 {
-        // assert(request->requested_alg == DEFAULT_ALG_UNSET ||
-        // aws_cryptosdk_algorithm_is_known(request->requested_alg));
-        ;
+        /* Note that we perform a top-level comparison here */
+        assert_byte_from_buffer_matches((uint8_t *)output, &old_output);
     }
 
     /* Postconditions */

diff --git a/verification/cbmc/sources/make_common_data_structures.c b/verification/cbmc/sources/make_common_data_structures.c
@@ -279,7 +279,10 @@ 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();
+        ensure_byte_buf_has_allocated_buffer_member(&materials->encrypted_data_keys);
         materials->signctx = ensure_nondet_sig_ctx_has_allocated_members();
+        ensure_array_list_has_allocated_data_member(&materials->keyring_trace);
+        ensure_array_list_has_allocated_data_member(&materials->encrypted_data_keys);
     }
     return materials;
 }