Add CBMC proof for default_cmm_generate_enc_materials #656

adpaco-aws · 2020-12-04T10:11:06Z

This PR adds a CBMC proof for default_cmm_generate_enc_materials, a function from default_cmm.c,

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.

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

alex-chew

LGTM, pending the comment about the aws_cryptosdk_alg_props(alg_id) validity assertion.

feliperodri · 2020-12-07T03:48:17Z

source/default_cmm.c

+    AWS_PRECONDITION(cmm != NULL);
+    AWS_PRECONDITION(output != NULL);


Why don't we check for the validity functions of aws_cryptosdk_cmm and aws_cryptosdk_enc_materials, respectively?

In this function, output is just a placeholder for encryption materials so we are okay with them not being valid (@alex-chew please correct me if I am wrong). I have added the validator function for it but we can discuss it further.

For aws_cryptosdk_cmm we now have validator function for default_cmm.

Edit: The test suite seems to fail if we add more complex preconditions for output, so I am using the previous version (non-null check).

You are correct that output is an out parameter for the generated encryption materials, and at the start of the function it is typically not the case that **output is a valid encryption materials struct. A stronger precondition that would make sense might be to assert that output is writable for sizeof(*output) bytes.

feliperodri · 2020-12-07T03:49:20Z

verification/cbmc/proofs/default_cmm_generate_enc_materials/Makefile

+# Local vars
+MAX_NUM_ITEMS ?= 1
+# In OBJ_txt2nid, this value unwinds strcmp(s, "prime256v1")


Added a comment.

feliperodri · 2020-12-07T03:49:49Z

verification/cbmc/proofs/default_cmm_generate_enc_materials/Makefile

+PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
+PROOF_SOURCES += $(PROOF_STUB)/aws_base64_encode.c
+
+REMOVE_FUNCTION_BODY += aws_base64_encode


Why? Could you add a comment?

Looks like it was not required. Thanks for catching it!

feliperodri · 2020-12-07T03:51:21Z

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

+int on_encrypt(
+    struct aws_cryptosdk_keyring *keyring,
+    struct aws_allocator *request_alloc,
+    struct aws_byte_buf *unencrypted_data_key,
+    struct aws_array_list *keyring_trace,
+    struct aws_array_list *edks,
+    const struct aws_hash_table *enc_ctx,
+    enum aws_cryptosdk_alg_id alg) {
+    /* Check validity for all inputs to avoid memory-safety violations. */
+    assert(aws_cryptosdk_keyring_is_valid(keyring));
+    assert(aws_allocator_is_valid(request_alloc));
+    assert(aws_byte_buf_is_valid(unencrypted_data_key));
+    assert(aws_cryptosdk_keyring_trace_is_valid(keyring_trace));
+    assert(aws_cryptosdk_edk_list_is_valid(edks));
+    assert(aws_cryptosdk_edk_list_elements_are_valid(edks));
+    assert((enc_ctx == NULL) || aws_hash_table_is_valid(enc_ctx));
+
+    if (unencrypted_data_key->buffer == NULL) {
+        const struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg);
+        if (props != NULL) {
+            __CPROVER_assume(aws_byte_buf_is_bounded(unencrypted_data_key, props->data_key_len));
+            ensure_byte_buf_has_allocated_buffer_member(unencrypted_data_key);
+            /*
+             * This satisfies the post-condition that if this keyring
+             * generated data key, it must be the right length.
+             * The nondeterminism increases coverage.
+             */
+            if (nondet_bool()) unencrypted_data_key->len = props->data_key_len;
+            unencrypted_data_key->allocator = request_alloc;
+            __CPROVER_assume(aws_byte_buf_is_valid(unencrypted_data_key));
+        }
+    } else {
+        /*
+         * If the buffer is not NULL, the byte buffer must not have been modified;
+         * however, this allocation modifies the buffer and increases coverage.
+         */
+        if (nondet_bool()) ensure_byte_buf_has_allocated_buffer_member(unencrypted_data_key);
+    }
+    int ret;
+    return ret;
+}


Why is this function here? Is it a stub? If so, we need to move it to the stub folder and add proper header documentation, which must say "why" we may need this stub.

I remember other proofs might do the same, do you think we could just use one on_encrypt implementation across them all?

You are right, I have put this function into the stubs folder.

feliperodri · 2020-12-07T03:53:36Z

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

+
+void default_cmm_generate_enc_materials_harness() {
+    /* Nondet input required to init cmm */
+    struct aws_cryptosdk_keyring *keyring        = malloc(sizeof(*keyring));


The allocator should contain this initial allocation.

feliperodri · 2020-12-07T03:54:27Z

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

+void default_cmm_generate_enc_materials_harness() {
+    /* Nondet input required to init cmm */
+    struct aws_cryptosdk_keyring *keyring        = malloc(sizeof(*keyring));
+    const struct aws_cryptosdk_keyring_vt vtable = { .vt_size    = sizeof(struct aws_cryptosdk_keyring_vt),


Why can't we have a non-deterministic number here? Does this assumption maps into an assertion into the code?

Yes, we have it now.

feliperodri · 2020-12-07T03:56:28Z

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

+    __CPROVER_assume(keyring->vtable != NULL);
+
+    /* Nondet input */
+    struct aws_cryptosdk_cmm *cmm               = aws_cryptosdk_default_cmm_new(can_fail_allocator(), keyring);


Why are you calling aws_cryptosdk_default_cmm_new to initialize cmm? This should only be done by allocators and validity functions. Any extra requirements should be add as an assumption and mapped as an assertion into the codebase.

I have created a new allocator function for default_cmm (which is an extension of cmm). We are not using this function anymore.

feliperodri · 2020-12-07T03:57:15Z

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

+    struct aws_cryptosdk_enc_materials **output = malloc(sizeof(*output));
+    struct aws_cryptosdk_enc_request *request   = malloc(sizeof(*request));
+
+    /* Assumptions */
+    __CPROVER_assume(cmm != NULL);
+
+    __CPROVER_assume(output != NULL);
+
+    __CPROVER_assume(request != NULL);
+    request->alloc = can_fail_allocator();
+    __CPROVER_assume(aws_allocator_is_valid(request->alloc));
+    request->enc_ctx = malloc(sizeof(*request->enc_ctx));
+    __CPROVER_assume(request->enc_ctx != NULL);
+    ensure_allocated_hash_table(request->enc_ctx, MAX_NUM_ITEMS);
+    __CPROVER_assume(aws_cryptosdk_enc_request_is_valid(request));


Where are the allocators functions for aws_cryptosdk_enc_materials and aws_cryptosdk_enc_request?

Added them.

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

feliperodri · 2020-12-10T05:15:49Z

/cbmc run checks

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

adpaco-aws

Sorry, I had this PR almost updated but I wanted to inspect some stuff in detail. We have a new solution which includes as much feedback from you when possible.

adpaco-aws · 2020-12-14T16:22:53Z

source/default_cmm.c

+    AWS_PRECONDITION(cmm != NULL);
+    AWS_PRECONDITION(output != NULL);


In this function, output is just a placeholder for encryption materials so we are okay with them not being valid (@alex-chew please correct me if I am wrong). I have added the validator function for it but we can discuss it further.

For aws_cryptosdk_cmm we now have validator function for default_cmm.

Edit: The test suite seems to fail if we add more complex preconditions for output, so I am using the previous version (non-null check).

adpaco-aws · 2020-12-14T16:23:09Z

verification/cbmc/proofs/default_cmm_generate_enc_materials/Makefile

+# Local vars
+MAX_NUM_ITEMS ?= 1
+# In OBJ_txt2nid, this value unwinds strcmp(s, "prime256v1")


Added a comment.

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

adpaco-aws · 2020-12-15T11:15:17Z

verification/cbmc/proofs/default_cmm_generate_enc_materials/Makefile

+PROOF_SOURCES += $(PROOF_SOURCE)/make_common_data_structures.c
+PROOF_SOURCES += $(PROOF_STUB)/aws_base64_encode.c
+
+REMOVE_FUNCTION_BODY += aws_base64_encode


Looks like it was not required. Thanks for catching it!

adpaco-aws · 2020-12-15T16:52:45Z

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

+int on_encrypt(
+    struct aws_cryptosdk_keyring *keyring,
+    struct aws_allocator *request_alloc,
+    struct aws_byte_buf *unencrypted_data_key,
+    struct aws_array_list *keyring_trace,
+    struct aws_array_list *edks,
+    const struct aws_hash_table *enc_ctx,
+    enum aws_cryptosdk_alg_id alg) {
+    /* Check validity for all inputs to avoid memory-safety violations. */
+    assert(aws_cryptosdk_keyring_is_valid(keyring));
+    assert(aws_allocator_is_valid(request_alloc));
+    assert(aws_byte_buf_is_valid(unencrypted_data_key));
+    assert(aws_cryptosdk_keyring_trace_is_valid(keyring_trace));
+    assert(aws_cryptosdk_edk_list_is_valid(edks));
+    assert(aws_cryptosdk_edk_list_elements_are_valid(edks));
+    assert((enc_ctx == NULL) || aws_hash_table_is_valid(enc_ctx));
+
+    if (unencrypted_data_key->buffer == NULL) {
+        const struct aws_cryptosdk_alg_properties *props = aws_cryptosdk_alg_props(alg);
+        if (props != NULL) {
+            __CPROVER_assume(aws_byte_buf_is_bounded(unencrypted_data_key, props->data_key_len));
+            ensure_byte_buf_has_allocated_buffer_member(unencrypted_data_key);
+            /*
+             * This satisfies the post-condition that if this keyring
+             * generated data key, it must be the right length.
+             * The nondeterminism increases coverage.
+             */
+            if (nondet_bool()) unencrypted_data_key->len = props->data_key_len;
+            unencrypted_data_key->allocator = request_alloc;
+            __CPROVER_assume(aws_byte_buf_is_valid(unencrypted_data_key));
+        }
+    } else {
+        /*
+         * If the buffer is not NULL, the byte buffer must not have been modified;
+         * however, this allocation modifies the buffer and increases coverage.
+         */
+        if (nondet_bool()) ensure_byte_buf_has_allocated_buffer_member(unencrypted_data_key);
+    }
+    int ret;
+    return ret;
+}


You are right, I have put this function into the stubs folder.

adpaco-aws · 2020-12-16T11:40:03Z

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

+void default_cmm_generate_enc_materials_harness() {
+    /* Nondet input required to init cmm */
+    struct aws_cryptosdk_keyring *keyring        = malloc(sizeof(*keyring));
+    const struct aws_cryptosdk_keyring_vt vtable = { .vt_size    = sizeof(struct aws_cryptosdk_keyring_vt),


Yes, we have it now.

adpaco-aws · 2020-12-16T11:44:15Z

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

+    __CPROVER_assume(keyring->vtable != NULL);
+
+    /* Nondet input */
+    struct aws_cryptosdk_cmm *cmm               = aws_cryptosdk_default_cmm_new(can_fail_allocator(), keyring);


I have created a new allocator function for default_cmm (which is an extension of cmm). We are not using this function anymore.

adpaco-aws · 2020-12-16T11:44:30Z

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

+    struct aws_cryptosdk_enc_materials **output = malloc(sizeof(*output));
+    struct aws_cryptosdk_enc_request *request   = malloc(sizeof(*request));
+
+    /* Assumptions */
+    __CPROVER_assume(cmm != NULL);
+
+    __CPROVER_assume(output != NULL);
+
+    __CPROVER_assume(request != NULL);
+    request->alloc = can_fail_allocator();
+    __CPROVER_assume(aws_allocator_is_valid(request->alloc));
+    request->enc_ctx = malloc(sizeof(*request->enc_ctx));
+    __CPROVER_assume(request->enc_ctx != NULL);
+    ensure_allocated_hash_table(request->enc_ctx, MAX_NUM_ITEMS);
+    __CPROVER_assume(aws_cryptosdk_enc_request_is_valid(request));


Added them.

adpaco-aws · 2020-12-16T12:09:09Z

@alex-chew I have tried the first one in here

If the call fails, you can verify:

request->requested_alg is a valid algorithm ID or zero
output is unchanged

assert(!request->requested_alg || aws_cryptosdk_algorithm_is_known(request->requested_alg);

and

assert(request->requested_alg == DEFAULT_ALG_UNSET ||
           aws_cryptosdk_algorithm_is_known(request->requested_alg));

(in case you meant DEFAULT_ALG_UNSET as zero). But none of them work for me. Can you please elaborate?

Also, I am not sure how to check that output remains unchanged. Do we have templates for this? @feliperodri @tegansb

alex-chew · 2020-12-16T21:02:58Z

@alex-chew I have tried the first one in here

If the call fails, you can verify:
request->requested_alg is a valid algorithm ID or zero
output is unchanged
assert(!request->requested_alg || aws_cryptosdk_algorithm_is_known(request->requested_alg);
and
assert(request->requested_alg == DEFAULT_ALG_UNSET ||
           aws_cryptosdk_algorithm_is_known(request->requested_alg));
(in case you meant DEFAULT_ALG_UNSET as zero). But none of them work for me. Can you please elaborate?

Oops, that's my bad. If the call fails, it should be the case that request->requested_alg is valid or unchanged (not zero). Sorry for the confusion. In retrospect, however, I'm not sure this is worth verifying.

Also, I am not sure how to check that output remains unchanged. Do we have templates for this? @feliperodri @tegansb

You can save its value prior to calling the function under verification and check that its value is unchanged by the call. e.g. https://github.com/aws/aws-encryption-sdk-c/blob/master/verification/cbmc/proofs/aws_cryptosdk_priv_hdr_parse_alg_id/aws_cryptosdk_priv_hdr_parse_alg_id_harness.c

adpaco-aws · 2020-12-21T18:24:01Z

@alex-chew Ok, I have removed the assert in case of failure.

I have also added code to check that output remains unchanged at the top level (i.e., it performs a cast of the struct and compares the values as an array, but does not check for changes on structures being pointed to by its members). The main reason to leave it as it is performance, since doing these checks would be time-consuming and the structures are not really used in the function under verification (remember that output is just a placeholder in this function).

feliperodri · 2020-12-21T18:46:31Z

source/default_cmm.c

@@ -180,3 +185,10 @@ int aws_cryptosdk_default_cmm_set_alg_id(struct aws_cryptosdk_cmm *cmm, enum aws
    self->default_alg = alg_id;
    return AWS_OP_SUCCESS;
 }
+
+bool aws_cryptosdk_default_cmm_is_valid(const struct aws_cryptosdk_cmm *cmm) {
+    AWS_PRECONDITION(cmm != NULL);


It should return false in case cmm is NULL, not fail on an assertion.

Right, I am happy you saw this because I had my doubts about it.

feliperodri · 2020-12-21T18:47:56Z

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

+    __CPROVER_assume(cmm != NULL);
+    __CPROVER_assume(aws_cryptosdk_default_cmm_is_valid(cmm));


You wouldn't need it if aws_cryptosdk_default_cmm_is_valid returned false in case cmm is NULL.

Removed non-null assumption, thanks!

feliperodri · 2020-12-21T18:48:46Z

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c

+    __CPROVER_assume(request != NULL);
+    __CPROVER_assume(aws_allocator_is_valid(request->alloc));
+    __CPROVER_assume(request->enc_ctx != NULL);
+    __CPROVER_assume(aws_cryptosdk_enc_request_is_valid(request));


This looks odd to me too. Why the first three assumptions are not part of the validity check for aws_cryptosdk_enc_request?

This is probably from my early days of proof-writing. The assumptions were not needed so I removed them.

feliperodri · 2020-12-21T18:49:38Z

verification/cbmc/sources/make_common_data_structures.c

+    struct aws_cryptosdk_cmm base;
+    struct aws_allocator *alloc;
+    struct aws_cryptosdk_keyring *kr;
+    // Invariant: this is either DEFAULT_ALG_UNSET or is a valid algorithm ID


Avoid cpp comments.

/* Invariant: this is either DEFAULT_ALG_UNSET or is a valid algorithm ID. */

I copied this from the source code, so I fixed it in both places.

feliperodri · 2020-12-21T18:50:40Z

verification/cbmc/sources/make_common_data_structures.c

+    /* Assumptions required to init cmm */
+    ensure_cryptosdk_keyring_has_allocated_members(keyring, vtable);
+    __CPROVER_assume(aws_cryptosdk_keyring_is_valid(keyring));
+    __CPROVER_assume(keyring->vtable != NULL);


Create a GitHub issue to investigate a way to move these assumptions to the validity function and not to the allocator.

Opened one here: #675

feliperodri · 2020-12-21T18:51:11Z

verification/cbmc/sources/make_common_data_structures.c

+    struct default_cmm *self = NULL;
+    if (cmm) {
+        self        = (struct default_cmm *)cmm;
+        self->alloc = can_fail_allocator();


Could it be NULL? We should be as nondet as possible here.

Yes, I missed that one. It can be NULL now.

feliperodri · 2020-12-21T18:53:04Z

verification/cbmc/stubs/on_encrypt_stub.c

+    int ret;
+    return ret;


return nondet_int();

Done as well.

Change variable name and add comment for it on Makefile Merge changes from 'master'

Do intial allocation as usual and pass output by reference Remove request_alg assertion in case of failure

Replace precondition by false case in enc_request validator

alex-chew

LGTM, pending CI fixes.

feliperodri

I have a few more questions, but no blockers.

feliperodri · 2021-01-06T14:42:54Z

source/default_cmm.c

+bool aws_cryptosdk_default_cmm_is_valid(const struct aws_cryptosdk_cmm *cmm) {
+    if (cmm == NULL) return false;
+
+    struct default_cmm *self = (struct default_cmm *)cmm;
+    return aws_cryptosdk_cmm_base_is_valid(&self->base) && aws_allocator_is_valid(self->alloc) &&
+           aws_cryptosdk_keyring_is_valid(self->kr);
+}


Why this function wasn't written like...

bool default_cmm_is_valid(const struct default_cmm *cmm) { return (cmm != NULL) && aws_cryptosdk_cmm_base_is_valid(&cmm->base) && aws_allocator_is_valid(cmm->alloc) && aws_cryptosdk_keyring_is_valid(cmm->kr); }

Shouldn't we validate both structures separately (i.e., on validity function for each data structure)?

In general, extensions of aws_cryptosdk_cmm are always handled like this in the source code: The type is used as a parameter/return type and the struct is cast before doing any operations on it. This way, we are following API guidelines.

I am not sure what you mean by "validate both structures separately". We have aws_cryptosdk_cmm_base_is_valid for validating aws_cryptosdk_cmm structs and this one to validate default_cmm structs.

feliperodri · 2021-01-06T14:49:42Z

verification/cbmc/sources/make_common_data_structures.c

+    if (cmm) {
+        self        = (struct default_cmm *)cmm;
+        self->alloc = nondet_bool() ? NULL : can_fail_allocator();
+        self->kr    = keyring;
+    }
+    return (struct aws_cryptosdk_cmm *)self;


feliperodri · 2021-01-06T14:50:01Z

verification/cbmc/stubs/on_encrypt_stub.c

+ * limitations under the License.
+ */
+
+#include <stdlib.h>


Why do you need that include?

You are right, this was not required.

* Add proof files for default_cmm_generate_enc_materials * Move on_encrypt function to its own file * Add validator and allocator functions Change variable name and add comment for it on Makefile Merge changes from 'master' * Add and edit allocators for materials and cmm * Add missing file to Makefile (algorithm_is_known) * Remove unnecessary assumptions * Edit preconditions and postconditions * Fix style checks * Restore simpler precondition * 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 * Fix style issues * Use C-style comments and add space * Remove unneeded assumptions and use nondet values Replace precondition by false case in enc_request validator * Remove copyright year on Makefile

adpaco-aws force-pushed the default-materials-proof branch 5 times, most recently from 22aa393 to 33b1cd1 Compare December 4, 2020 10:46

adpaco-aws marked this pull request as ready for review December 4, 2020 11:31

alex-chew reviewed Dec 5, 2020

View reviewed changes

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c Outdated Show resolved Hide resolved

alex-chew requested changes Dec 5, 2020

View reviewed changes

feliperodri added the cbmc CBMC proof related work label Dec 7, 2020

feliperodri requested changes Dec 7, 2020

View reviewed changes

adpaco-aws force-pushed the default-materials-proof branch from 33b1cd1 to 2c7bbea Compare December 11, 2020 12:46

alex-chew requested changes Dec 15, 2020

View reviewed changes

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c Outdated Show resolved Hide resolved

.../cbmc/proofs/default_cmm_generate_enc_materials/default_cmm_generate_enc_materials_harness.c Outdated Show resolved Hide resolved

adpaco-aws commented Dec 16, 2020

View reviewed changes

adpaco-aws force-pushed the default-materials-proof branch from 2c7bbea to 493ee2a Compare December 16, 2020 11:57

adpaco-aws force-pushed the default-materials-proof branch 3 times, most recently from f34515e to 656eadd Compare December 16, 2020 12:33

adpaco-aws requested review from feliperodri and alex-chew December 16, 2020 12:36

adpaco-aws force-pushed the default-materials-proof branch from 0f2499b to face741 Compare December 21, 2020 16:42

adpaco-aws requested a review from tegansb December 21, 2020 18:24

feliperodri requested changes Dec 21, 2020

View reviewed changes

adpaco-aws force-pushed the default-materials-proof branch 2 times, most recently from 97bb1bd to a8d9dd0 Compare December 22, 2020 16:03

adpaco-aws mentioned this pull request Dec 22, 2020

Investigate how to move assumptions out of ensure_... functions #675

Open

adpaco-aws requested a review from feliperodri December 22, 2020 17:38

adpaco-aws force-pushed the default-materials-proof branch from 34604fe to f9b0169 Compare December 28, 2020 09:25

adpaco-aws added 13 commits December 28, 2020 10:26

Add proof files for default_cmm_generate_enc_materials

073a17c

Move on_encrypt function to its own file

d6cdba9

Add validator and allocator functions

d9c49a2

Change variable name and add comment for it on Makefile Merge changes from 'master'

Add and edit allocators for materials and cmm

ffde1fb

Add missing file to Makefile (algorithm_is_known)

a2179de

Remove unnecessary assumptions

fd997a6

Edit preconditions and postconditions

c014f30

Fix style checks

3104993

Restore simpler precondition

8042c35

Check that output remains unchanged (top-level check only)

2c8da7d

Do intial allocation as usual and pass output by reference Remove request_alg assertion in case of failure

Fix style issues

3a9d3c7

Use C-style comments and add space

90f4d45

Remove unneeded assumptions and use nondet values

ecec9b5

Replace precondition by false case in enc_request validator

adpaco-aws force-pushed the default-materials-proof branch from f9b0169 to ecec9b5 Compare December 28, 2020 09:27

alex-chew approved these changes Jan 6, 2021

View reviewed changes

Remove copyright year on Makefile

73ccb76

feliperodri approved these changes Jan 6, 2021

View reviewed changes

adpaco-aws merged commit 7aaad97 into aws:master Jan 6, 2021

adpaco-aws mentioned this pull request Jan 7, 2021

Remove unnecessary include from on_encrypt stub #684

Merged

1 task

		AWS_PRECONDITION(cmm != NULL);
		AWS_PRECONDITION(output != NULL);

		__CPROVER_assume(cmm != NULL);
		__CPROVER_assume(aws_cryptosdk_default_cmm_is_valid(cmm));

Add CBMC proof for default_cmm_generate_enc_materials #656

Add CBMC proof for default_cmm_generate_enc_materials #656

Conversation

adpaco-aws commented Dec 4, 2020

Check any applicable:

alex-chew left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

adpaco-aws Dec 14, 2020 • edited Loading

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

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

feliperodri commented Dec 10, 2020

adpaco-aws left a comment

Choose a reason for hiding this comment

adpaco-aws Dec 14, 2020 • edited Loading

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 commented Dec 16, 2020

alex-chew commented Dec 16, 2020

adpaco-aws commented Dec 21, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

adpaco-aws Dec 22, 2020 • edited Loading

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

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

adpaco-aws Dec 14, 2020 •

edited

Loading

adpaco-aws Dec 14, 2020 •

edited

Loading

adpaco-aws commented Dec 21, 2020 •

edited

Loading

adpaco-aws Dec 22, 2020 •

edited

Loading