Adds CBMC proof for sign_header #659

tegansb · 2020-12-08T16:33:27Z

Adds harness, Makefile and yaml for sign_header.

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.

Resolves aws#639.

alex-chew

Mostly LGTM, just a few nitpicks about naming/comments.

verification/cbmc/proofs/sign_header/sign_header_harness.c

feliperodri · 2020-12-16T02:08:21Z

source/session_encrypt.c

+    AWS_PRECONDITION(session != NULL);
+    AWS_PRECONDITION(aws_allocator_is_valid(session->alloc));
+    AWS_PRECONDITION(aws_cryptosdk_hdr_is_valid(&session->header));
+    AWS_PRECONDITION(aws_cryptosdk_sig_ctx_is_valid(session->signctx));
+    AWS_PRECONDITION(session->state == ST_GEN_KEY);
+    AWS_PRECONDITION(session->mode == AWS_CRYPTOSDK_ENCRYPT);


Replace it by

AWS_PRECONDITION(aws_cryptosdk_session_is_valid(session));

source/session_encrypt.c

feliperodri · 2020-12-21T17:04:20Z

source/session_encrypt.c

+    AWS_PRECONDITION(session != NULL);
+    AWS_PRECONDITION(aws_allocator_is_valid(session->alloc));
+    AWS_PRECONDITION(aws_cryptosdk_hdr_is_valid(&session->header));
+    AWS_PRECONDITION(session->header.iv.len <= session->alg_props->iv_len);
+    AWS_PRECONDITION(session->header.auth_tag.len <= session->alg_props->tag_len);
+    AWS_PRECONDITION(aws_cryptosdk_sig_ctx_is_valid(session->signctx));
+    AWS_PRECONDITION(session->state == ST_GEN_KEY);
+    AWS_PRECONDITION(session->mode == AWS_CRYPTOSDK_ENCRYPT);


We don't need an unique allocator for session to cope with proof complexity, but we should have a validity function for it. Could you group the general checks here into a validity function for aws_cryptosdk_session structures?

Yes! This has been updated!

feliperodri · 2020-12-21T17:04:49Z

source/session_encrypt.c

+    if (session->header.iv.len) {
+        assert(session->header.iv.buffer);
+        memset(session->header.iv.buffer, 0x42, session->header.iv.len);
+    }
+    if (session->header.auth_tag.len) {
+        assert(session->header.auth_tag.buffer);
+        memset(session->header.auth_tag.buffer, 0xDE, session->header.auth_tag.len);
+    }


Should we assert or return error? @alex-chew

Short answer: assert. The condition should always be true, and if not then it's a programming error rather than a user/data error.

Long answer: I think we can actually leave out the assert, since the aws_cryptosdk_hdr_is_valid(&session->header) precondition implies that the session->header.iv and session->header.auth_tag are aws_byte_buf_is_valid, which in turn implies that iv.len implies iv.buffer and likewise for auth_tag. But the assert is valuable as documentation of this intent.

Digging deeper, it looks like the only callsite of sign_header appears after a successfull call to build_header, which initializes these buffers to have positive length (since all supported algorithm suites use 12- and 16-byte IVs and authentication tag lengths, respectively). So we can change the guards/asserts to preconditions (i.e. byte_buf_is_valid and buf.len > 0 for each of the IV and auth tag).

source/session_encrypt.c

verification/cbmc/proofs/sign_header/Makefile

alex-chew · 2021-01-06T02:04:50Z

source/session_encrypt.c

    AWS_PRECONDITION(session->header.iv.len <= session->alg_props->iv_len);
    AWS_PRECONDITION(session->header.auth_tag.len <= session->alg_props->tag_len);
-    AWS_PRECONDITION(aws_cryptosdk_sig_ctx_is_valid(session->signctx));


Not a blocker, but I'm curious why this is no longer needed?

Thanks for bringing this up. I will check if the associated assumption in the harness can be removed.

@alex-chew we have investigated this issue and we have decided to remove the assumption from the harness. Note that the session validator allows session->signctx to be either NULL or valid. To do so, we modified a precondition in EVP_DigestUpdate which we think is too restrictive.

Moreover, we have opened an issue (#685) to remove this type of validators from the code base, since they cannot be mirrored as preconditions.

feliperodri

LGTM.

…estUpdate

adpaco-aws · 2021-01-11T11:32:15Z

The last changes include a stub for aws_cryptosdk_hdr_write which causes the proof to run much faster than earlier.

@feliperodri can you take a look at this stub and let us know what you think? The original function can be found here:

aws-encryption-sdk-c/source/header.c

Lines 472 to 568 in 6a2ee0e

    
           int aws_cryptosdk_hdr_write( 
        
               const struct aws_cryptosdk_hdr *hdr, size_t *bytes_written, uint8_t *outbuf, size_t outlen) { 
        
               AWS_PRECONDITION(aws_cryptosdk_hdr_is_valid(hdr)); 
        
               AWS_PRECONDITION(hdr->iv.len <= UINT8_MAX);  // uint8_t max value 
        
               AWS_PRECONDITION(outlen == 0 || AWS_MEM_IS_READABLE(outbuf, outlen)); 
        
               AWS_PRECONDITION(bytes_written != NULL); 
        
               struct aws_byte_buf output = aws_byte_buf_from_array(outbuf, outlen); 
        
               output.len                 = 0; 
        
               const struct aws_cryptosdk_alg_properties *alg_props = aws_cryptosdk_alg_props(hdr->alg_id); 
        
               if (!alg_props) goto INVALID_HEADER; 
        
               enum aws_cryptosdk_hdr_version header_version = alg_props->msg_format_version; 
        
               if (!aws_byte_buf_write_u8(&output, header_version)) goto WRITE_ERR; 
        
               if (header_version == AWS_CRYPTOSDK_HEADER_VERSION_1_0) { 
        
                   if (!aws_byte_buf_write_u8(&output, AWS_CRYPTOSDK_HEADER_TYPE_CUSTOMER_AED)) goto WRITE_ERR; 
        
               } 
        
               if (!aws_byte_buf_write_be16(&output, hdr->alg_id)) goto WRITE_ERR; 
        
               if (!aws_byte_buf_write_from_whole_cursor( 
        
                       &output, aws_byte_cursor_from_array(hdr->message_id.buffer, hdr->message_id.len))) 
        
                   goto WRITE_ERR; 
        
               // TODO - unify everything on byte_bufs when the aws-c-common refactor lands 
        
               // See: https://github.com/awslabs/aws-c-common/pull/130 
        
               struct aws_byte_buf aad_length_field; 
        
               init_aws_byte_buf_raw(&aad_length_field); 
        
               if (!aws_byte_buf_advance(&output, &aad_length_field, 2)) goto WRITE_ERR; 
        
               size_t old_len = output.len; 
        
               if (aws_cryptosdk_enc_ctx_serialize(aws_default_allocator(), &output, &hdr->enc_ctx)) goto WRITE_ERR; 
        
               if (!aws_byte_buf_write_be16(&aad_length_field, (uint16_t)(output.len - old_len))) goto WRITE_ERR; 
        
               size_t edk_count = aws_array_list_length(&hdr->edk_list); 
        
               if (!aws_byte_buf_write_be16(&output, (uint16_t)edk_count)) goto WRITE_ERR; 
        
               for (size_t idx = 0; idx < edk_count; ++idx) { 
        
                   void *vp_edk = NULL; 
        
                   aws_array_list_get_at_ptr(&hdr->edk_list, &vp_edk, idx); 
        
                   assert(vp_edk); 
        
                   const struct aws_cryptosdk_edk *edk = vp_edk; 
        
                   if (!aws_byte_buf_write_be16(&output, (uint16_t)edk->provider_id.len)) goto WRITE_ERR; 
        
                   if (!aws_byte_buf_write_from_whole_cursor( 
        
                           &output, aws_byte_cursor_from_array(edk->provider_id.buffer, edk->provider_id.len))) 
        
                       goto WRITE_ERR; 
        
                   if (!aws_byte_buf_write_be16(&output, (uint16_t)edk->provider_info.len)) goto WRITE_ERR; 
        
                   if (!aws_byte_buf_write_from_whole_cursor( 
        
                           &output, aws_byte_cursor_from_array(edk->provider_info.buffer, edk->provider_info.len))) 
        
                       goto WRITE_ERR; 
        
                   if (!aws_byte_buf_write_be16(&output, (uint16_t)edk->ciphertext.len)) goto WRITE_ERR; 
        
                   if (!aws_byte_buf_write_from_whole_cursor( 
        
                           &output, aws_byte_cursor_from_array(edk->ciphertext.buffer, edk->ciphertext.len))) 
        
                       goto WRITE_ERR; 
        
               } 
        
               if (!aws_byte_buf_write_u8( 
        
                       &output, hdr->frame_len ? AWS_CRYPTOSDK_HEADER_CTYPE_FRAMED : AWS_CRYPTOSDK_HEADER_CTYPE_NONFRAMED)) 
        
                   goto WRITE_ERR; 
        
               if (header_version == AWS_CRYPTOSDK_HEADER_VERSION_1_0) { 
        
                   if (!aws_byte_buf_write(&output, zero.bytes, 4)) goto WRITE_ERR;  // v01 reserved field 
        
                   if (!aws_byte_buf_write_u8(&output, (uint8_t)hdr->iv.len)) goto WRITE_ERR; 
        
               } 
        
               if (!aws_byte_buf_write_be32(&output, hdr->frame_len)) goto WRITE_ERR; 
        
               if (!aws_byte_buf_write_from_whole_cursor( 
        
                       &output, aws_byte_cursor_from_array(hdr->alg_suite_data.buffer, hdr->alg_suite_data.len))) 
        
                   goto WRITE_ERR; 
        
               if (header_version == AWS_CRYPTOSDK_HEADER_VERSION_1_0) { 
        
                   if (!aws_byte_buf_write_from_whole_cursor(&output, aws_byte_cursor_from_array(hdr->iv.buffer, hdr->iv.len))) 
        
                       goto WRITE_ERR; 
        
               } 
        
               if (!aws_byte_buf_write_from_whole_cursor( 
        
                       &output, aws_byte_cursor_from_array(hdr->auth_tag.buffer, hdr->auth_tag.len))) 
        
                   goto WRITE_ERR; 
        
               *bytes_written = output.len; 
        
               return AWS_OP_SUCCESS; 
        
           INVALID_HEADER: 
        
               aws_secure_zero(outbuf, outlen); 
        
               *bytes_written = 0; 
        
               return aws_raise_error(AWS_CRYPTOSDK_ERR_BAD_STATE); 
        
           WRITE_ERR: 
        
               aws_secure_zero(outbuf, outlen); 
        
               *bytes_written = 0; 
        
               return aws_raise_error(AWS_ERROR_SHORT_BUFFER); 
        
           }

feliperodri

LGTM, modulo a few suggestions.

feliperodri · 2021-01-11T14:43:15Z

verification/cbmc/proofs/sign_header/Makefile

+PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_byte_buf_write_stub.c
+PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_iter_overrides.c


Could you create a GitHub issue to standardize the name of stubs? Some of them use as sufix stub some others use overrides some other use something else... (no a blocker for this PR).

verification/cbmc/proofs/sign_header/Makefile

feliperodri · 2021-01-11T15:03:55Z

verification/cbmc/stubs/hdr_write_stub.c

+/*
+ * Stub for aws_cryptosdk_hdr_write
+ * The original function declares an aws_byte_buf output variable where
+ * different components of the header get written, but the actual output
+ * of the function is bytes_written. Therefore, we assign a nondet. value
+ * to this variable in case of success or zero both outbuf and outlen in
+ * case of failure
+ */


nit: Suggestion:

/** * The original aws_cryptosdk_hdr_write function declares an aws_byte_buf * output variable where different components of the header get written, * however, the actual output of the function is bytes_written. Therefore, * we assign a nondeterministic value to bytes_written in case of success * or zero both outbuf and outlen in case of failure. */

The stub looks great. How much gain in performance?

Thanks! It was ~40min on my dedicated machine before, but only ~10min now 😄

* Split aws_cryptosdk_hdr_parse into smaller functions Resolves #639. * Adds harness, Makefile and yaml for sign_header * Added preconditions to source code and added checks for memcpy * Update Makefile * Remove unneeded empty slot assumption * Use new hdr_setup in harness and fix comment * Added comment about when the object-bits flag is required * Added preconditions of lne of byte bufs * Use CBMC_OBJECT_BITS flag * Make len != 0 check explicit * Use session_setup and aws_session_is_valid * Remove signctx precondition in harness. Weaken precondition in EVPDigestUpdate * Stub out hdr_write. Use default CBMC_OBJECT_BITS value * Remove unwind value for hdr_write * Add and improve documentation Co-authored-by: Alex Chew <[email protected]> Co-authored-by: Alex Chew <[email protected]> Co-authored-by: Adrian Palacios <[email protected]> Co-authored-by: Adrian Palacios <[email protected]>

* Split aws_cryptosdk_hdr_parse into smaller functions Resolves aws#639. * Adds harness, Makefile and yaml for sign_header * Added preconditions to source code and added checks for memcpy * Update Makefile * Remove unneeded empty slot assumption * Use new hdr_setup in harness and fix comment * Added comment about when the object-bits flag is required * Added preconditions of lne of byte bufs * Use CBMC_OBJECT_BITS flag * Make len != 0 check explicit * Use session_setup and aws_session_is_valid * Remove signctx precondition in harness. Weaken precondition in EVPDigestUpdate * Stub out hdr_write. Use default CBMC_OBJECT_BITS value * Remove unwind value for hdr_write * Add and improve documentation Co-authored-by: Alex Chew <[email protected]> Co-authored-by: Alex Chew <[email protected]> Co-authored-by: Adrian Palacios <[email protected]> Co-authored-by: Adrian Palacios <[email protected]>

* Split aws_cryptosdk_hdr_parse into smaller functions Resolves #639. * Adds harness, Makefile and yaml for sign_header * Added preconditions to source code and added checks for memcpy * Update Makefile * Remove unneeded empty slot assumption * Use new hdr_setup in harness and fix comment * Added comment about when the object-bits flag is required * Added preconditions of lne of byte bufs * Use CBMC_OBJECT_BITS flag * Make len != 0 check explicit * Use session_setup and aws_session_is_valid * Remove signctx precondition in harness. Weaken precondition in EVPDigestUpdate * Stub out hdr_write. Use default CBMC_OBJECT_BITS value * Remove unwind value for hdr_write * Add and improve documentation Co-authored-by: Alex Chew <[email protected]> Co-authored-by: Alex Chew <[email protected]> Co-authored-by: Adrian Palacios <[email protected]> Co-authored-by: Adrian Palacios <[email protected]>

alex-chew and others added 6 commits November 26, 2020 14:06

Split aws_cryptosdk_hdr_parse into smaller functions

533c105

Resolves aws#639.

Merge branch 'master' into split-hdr-parse

183bd77

Merge branch 'master' into split-hdr-parse

855217a

merge

57a97cd

Adds harness, Makefile and yaml for sign_header

9cbe91e

Added preconditions to source code and added checks for memcpy

f128327

tegansb requested a review from alex-chew December 8, 2020 16:33

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

tegansb requested a review from feliperodri December 8, 2020 16:33

alex-chew approved these changes Dec 8, 2020

View reviewed changes

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

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

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

tegansb and others added 7 commits December 9, 2020 22:41

Update Makefile

318601b

Remove unneeded empty slot assumption

3fee097

Merge branch 'master' into sign_header

d128aef

Merge branch 'master' into sign_header

41c671f

Use new hdr_setup in harness and fix comment

54135ed

Added comment about when the object-bits flag is required

8d8a1b5

Added preconditions of lne of byte bufs

1c0ea26

feliperodri requested changes Dec 21, 2020

View reviewed changes

tegansb and others added 5 commits December 21, 2020 12:13

Use CBMC_OBJECT_BITS flag

038c3da

Make len != 0 check explicit

beb8a1e

Merge branch 'master' into sign_header

9a628e1

Merge branch 'master' into sign_header

99b7aa9

Use session_setup and aws_session_is_valid

26db5d3

alex-chew reviewed Jan 6, 2021

View reviewed changes

alex-chew approved these changes Jan 6, 2021

View reviewed changes

Merge branch 'master' into sign_header

76e8d41

feliperodri approved these changes Jan 7, 2021

View reviewed changes

Merge branch 'master' into sign_header

c06ea6a

adpaco-aws force-pushed the sign_header branch from de4cede to 5a4f1cb Compare January 11, 2021 10:34

Remove signctx precondition in harness. Weaken precondition in EVPDig…

4d0477a

…estUpdate

Stub out hdr_write. Use default CBMC_OBJECT_BITS value

0dd0ee0

adpaco-aws force-pushed the sign_header branch from 5a4f1cb to 0dd0ee0 Compare January 11, 2021 10:41

adpaco-aws mentioned this pull request Jan 11, 2021

Remove CBMC validator functions #685

Open

Remove unwind value for hdr_write

56621c2

adpaco-aws marked this pull request as ready for review January 11, 2021 12:16

feliperodri approved these changes Jan 11, 2021

View reviewed changes

Add and improve documentation

e537227

adpaco-aws merged commit f2e9593 into aws:master Jan 11, 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 sign_header #659

Adds CBMC proof for sign_header #659

tegansb commented Dec 8, 2020

alex-chew left a comment

feliperodri Dec 16, 2020

tegansb Dec 29, 2020

feliperodri Dec 21, 2020

tegansb Dec 29, 2020

feliperodri Dec 21, 2020

alex-chew Dec 21, 2020

alex-chew Dec 21, 2020

alex-chew Jan 6, 2021

adpaco-aws Jan 6, 2021 •

edited

Loading

adpaco-aws Jan 11, 2021

feliperodri left a comment

adpaco-aws commented Jan 11, 2021

feliperodri left a comment

feliperodri Jan 11, 2021

adpaco-aws Jan 11, 2021

feliperodri Jan 11, 2021

feliperodri Jan 11, 2021

adpaco-aws Jan 11, 2021

		PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_byte_buf_write_stub.c
		PROOF_SOURCES += $(COMMON_PROOF_STUB)/aws_hash_iter_overrides.c

Adds CBMC proof for sign_header #659

Adds CBMC proof for sign_header #659

Conversation

tegansb commented Dec 8, 2020

Check any applicable:

alex-chew 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

adpaco-aws Jan 6, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

feliperodri left a comment

Choose a reason for hiding this comment

adpaco-aws commented Jan 11, 2021

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

adpaco-aws Jan 6, 2021 •

edited

Loading