Adds CBMC proof for aws_cryptosdk_priv_try_gen_key #661

tegansb · 2020-12-09T17:03:04Z

Adds Makefile, harness and yaml for proof of aws_cryptosdk_priv_try_gen_key.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

Check any applicable:

Were any files moved? Moving files changes their URL, which breaks all hyperlinks to the files.

verification/cbmc/sources/make_common_data_structures.c

...fication/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c

source/keyring_trace.c

adpaco-aws · 2020-12-19T11:27:24Z

source/session_encrypt.c

+    AWS_PRECONDITION(session != NULL);
+    AWS_PRECONDITION(aws_cryptosdk_cmm_base_is_valid(session->cmm));
+    AWS_PRECONDITION(aws_cryptosdk_alg_properties_is_valid(session->alg_props));
+    AWS_PRECONDITION(aws_cryptosdk_hdr_is_valid(&session->header));
+    AWS_PRECONDITION(aws_cryptosdk_keyring_trace_is_valid(&session->keyring_trace));
+    AWS_PRECONDITION(aws_allocator_is_valid(session->alloc));
+    AWS_PRECONDITION(aws_cryptosdk_commitment_policy_is_valid(session->commitment_policy));
+    AWS_PRECONDITION(session->state == ST_GEN_KEY);
+    AWS_PRECONDITION(session->mode == AWS_CRYPTOSDK_ENCRYPT);


Can you open an issue so that I do not forget replacing this by the session validator that I am writing?

Made one here - #670

verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile

verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/cbmc-batch.yaml

source/session_encrypt.c

verification/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/Makefile

...fication/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c

adpaco-aws

This PR is now ready to review! Here is a summary of the changes I have introduced since the last time you reviewed it:

The session validator now allows session->alg_props to be null or valid.
Due to the previous change, the proofs for sign_header and derive_data_key were broken (they assumed session->alg_props to be always valid). Therefore, I have added additional assumptions/preconditions to enforce session->alg_props to be valid.
All stubs that were defined in the harness have been moved to their own file on the stubs folder.
I have included the stub for aws_cryptosdk_hdr_write that I wrote for the sign_header proof in this PR. This reduced the time to complete this proof from ~2h to ~30mins.
Buffer validity is asserted for okm in the HKDF stub.

As noted in the harness, we do not use the session_setup function because would be creating objects that are not used or need to be replaced later (costly in proofs like this one).

Reviewer is now an author

feliperodri

LGTM, with a few more improvements in documentation.

feliperodri · 2021-01-19T12:20:53Z

include/aws/cryptosdk/private/session.h

@@ -103,7 +103,7 @@ AWS_CRYPTOSDK_STATIC_INLINE bool aws_cryptosdk_session_is_valid(const struct aws
    bool cmm_valid            = aws_cryptosdk_cmm_base_is_valid(session->cmm);
    bool hdr_valid            = aws_cryptosdk_hdr_is_valid(&session->header);
    bool keyring_trace_valid  = aws_cryptosdk_keyring_trace_is_valid(&session->keyring_trace);
-    bool alg_props_valid      = aws_cryptosdk_alg_properties_is_valid(session->alg_props);
+    bool alg_props_valid      = session->alg_props == NULL || aws_cryptosdk_alg_properties_is_valid(session->alg_props);


I'd add parenthesis.

bool alg_props_valid = (session->alg_props == NULL || aws_cryptosdk_alg_properties_is_valid(session->alg_props));

And makes sure @alex-chew agree that a valid aws_cryptosdk_session can have a NULL alg_props.

Indeed session->alg_props can be NULL.

feliperodri · 2021-01-19T12:21:42Z

source/session_encrypt.c

+    if (aws_byte_buf_init(&session->header.message_id, session->alloc, message_id_len) != AWS_OP_SUCCESS) {
+        goto out;
+    }


Good catch.

feliperodri · 2021-01-19T12:25:48Z

...fication/cbmc/proofs/aws_cryptosdk_priv_try_gen_key/aws_cryptosdk_priv_try_gen_key_harness.c

+ * multiple functions (see Makefile). It also requires a quite specific
+ * configuration for the session struct (cmm's vtable must include a
+ * pointer to the function declared above, alg_props can be NULL or valid,
+ * etc.) so we do not use the session_setup method to initialize it


/* * ... to initialize it. */

feliperodri · 2021-01-19T12:30:09Z

verification/cbmc/stubs/aws_array_list_item_generator_u8_stub.c

+ * A generator function as described in the comment
+ * in aws_cryptosdk_hash_elems_array_init_stub.c


You should describe it again here.

feliperodri · 2021-01-19T12:35:37Z

verification/cbmc/stubs/keyring_trace_clean_up_stub.c

+/* Stub this until https://github.com/diffblue/cbmc/issues/5344 is fixed
+ Original function is here:
+ https://github.com/aws/aws-encryption-sdk-c/blob/master/source/edk.c#L44 */
+void aws_cryptosdk_edk_list_clean_up(struct aws_array_list *encrypted_data_keys) {
+    assert(aws_cryptosdk_edk_list_is_valid(encrypted_data_keys));
+    aws_array_list_clean_up(encrypted_data_keys);
+}


We need a github issue to track this in this project, please, create one.

Looks like that issue has been solved, but we should determine the correctness/performance impact next. That alone would make an outstanding PR, so I have created the corresponding issue here: #690

verification/cbmc/stubs/keyring_trace_clear_stub.c

verification/cbmc/stubs/transfer_list_stub.c

verification/cbmc/proofs/sign_header/sign_header_harness.c

* Adds check in case byte_buf_init fails * Adds harness, Makefile and yaml for priv_try_gen_key * Adds preconditions to source code * Update to harness * yaml update to boiler plate default * Remove unneccessary remove functions * Added preconditions of lne of byte bufs * Use CBMC_OBJECT_BITS = 9 flag * Use session setup and validator functions * Move stubs in harness to stubs folder * Weaken preconditions. Allow null in session members * Remove CBMC_OBJECT_BITS flag * Add comments and assert for `okm` in hkdf stub * Add props assumptions in sign_header and derive_data_key proofs * Remove unused stub `aws_default_allocator` * Add missing source file in `sign_header` proof * Add minor improvements Co-authored-by: Adrian Palacios <[email protected]>

tegansb added the cbmc CBMC proof related work label Dec 9, 2020

alex-chew reviewed Dec 15, 2020

View reviewed changes

tegansb requested review from feliperodri and adpaco-aws December 18, 2020 19:29

adpaco-aws previously requested changes Dec 19, 2020

View reviewed changes

feliperodri requested changes Dec 21, 2020

View reviewed changes

adpaco-aws self-requested a review December 21, 2020 19:12

tegansb added 8 commits January 11, 2021 19:16

Adds check in case byte_buf_init fails

4c43c2c

Adds harness, Makefile and yaml for priv_try_gen_key

cd2615f

Adds preconditions to source code

c6fd20a

Update to harness

6ad0f6e

yaml update to boiler plate default

161f58a

Remove unneccessary remove functions

c626714

Added preconditions of lne of byte bufs

abf4725

Use CBMC_OBJECT_BITS = 9 flag

2340de6

adpaco-aws force-pushed the cbmc_priv_try_gen_key branch from 76096d6 to 2340de6 Compare January 11, 2021 18:19

adpaco-aws added 5 commits January 12, 2021 19:29

Use session setup and validator functions

ca326d3

Move stubs in harness to stubs folder

284934d

Weaken preconditions. Allow null in session members

753f8a3

Remove CBMC_OBJECT_BITS flag

99e56f2

Add comments and assert for okm in hkdf stub

00e277b

adpaco-aws marked this pull request as ready for review January 15, 2021 19:44

adpaco-aws force-pushed the cbmc_priv_try_gen_key branch 2 times, most recently from 93cf80d to 00e277b Compare January 18, 2021 10:18

adpaco-aws added 2 commits January 19, 2021 09:34

Add props assumptions in sign_header and derive_data_key proofs

c782c0a

Remove unused stub aws_default_allocator

fd16bf3

adpaco-aws force-pushed the cbmc_priv_try_gen_key branch from faff1c2 to fd16bf3 Compare January 19, 2021 09:34

adpaco-aws reviewed Jan 19, 2021

View reviewed changes

adpaco-aws requested a review from feliperodri January 19, 2021 11:32

adpaco-aws requested a review from alex-chew January 19, 2021 11:33

feliperodri approved these changes Jan 19, 2021

View reviewed changes

Add missing source file in sign_header proof

df5baa3

adpaco-aws force-pushed the cbmc_priv_try_gen_key branch from a0d13b3 to dfadf04 Compare January 19, 2021 15:33

Add minor improvements

ec5b382

adpaco-aws force-pushed the cbmc_priv_try_gen_key branch from dfadf04 to ec5b382 Compare January 19, 2021 15:34

alex-chew reviewed Jan 19, 2021

View reviewed changes

verification/cbmc/proofs/sign_header/sign_header_harness.c Show resolved Hide resolved

alex-chew approved these changes Jan 19, 2021

View reviewed changes

adpaco-aws merged commit c8c123a into aws:master Jan 19, 2021

adpaco-aws mentioned this pull request Jan 28, 2021

Replace preconditions with session validator in sign_header and priv_try_gen_key proofs #670

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Adds CBMC proof for aws_cryptosdk_priv_try_gen_key #661

Adds CBMC proof for aws_cryptosdk_priv_try_gen_key #661

tegansb commented Dec 9, 2020 •

edited

Loading

adpaco-aws Dec 19, 2020

tegansb Dec 20, 2020

adpaco-aws left a comment

feliperodri left a comment

feliperodri Jan 19, 2021

alex-chew Jan 19, 2021

feliperodri Jan 19, 2021

feliperodri Jan 19, 2021

feliperodri Jan 19, 2021

adpaco-aws Jan 19, 2021

feliperodri Jan 19, 2021

adpaco-aws Jan 19, 2021

		* A generator function as described in the comment
		* in aws_cryptosdk_hash_elems_array_init_stub.c

Adds CBMC proof for aws_cryptosdk_priv_try_gen_key #661

Adds CBMC proof for aws_cryptosdk_priv_try_gen_key #661

Conversation

tegansb commented Dec 9, 2020 • edited Loading

Check any applicable:

Choose a reason for hiding this comment

Choose a reason for hiding this comment

adpaco-aws left a comment

Choose a reason for hiding this comment

feliperodri left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tegansb commented Dec 9, 2020 •

edited

Loading