void aws_cryptosdk_private_derive_key_harness()

in verification/cbmc/proofs/aws_cryptosdk_private_derive_key/aws_cryptosdk_private_derive_key_harness.c [22:83]

• 49 lines of code
• 10 McCabe index (conditional complexity)

void aws_cryptosdk_private_derive_key_harness() {
    struct aws_cryptosdk_alg_properties *props = ensure_alg_properties_attempt_allocation(MAX_STRING_LEN);
    struct content_key *content_key            = ensure_content_key_attempt_allocation();
    struct data_key *data_key                  = ensure_data_key_attempt_allocation();
    struct aws_byte_buf *message_id            = malloc(sizeof(*message_id));
    struct aws_byte_buf *commitment            = malloc(sizeof(*commitment));

    /* Assumptions */
    __CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(props));

    __CPROVER_assume(aws_cryptosdk_content_key_is_valid(content_key));

    __CPROVER_assume(aws_cryptosdk_data_key_is_valid(data_key));

    __CPROVER_assume(IMPLIES(message_id != NULL, aws_byte_buf_is_bounded(message_id, MAX_BUFFER_SIZE)));
    ensure_byte_buf_has_allocated_buffer_member(message_id);
    __CPROVER_assume(aws_byte_buf_is_valid(message_id));

    __CPROVER_assume(IMPLIES(commitment != NULL, aws_byte_buf_is_bounded(commitment, MAX_BUFFER_SIZE)));
    ensure_byte_buf_has_allocated_buffer_member(commitment);
    __CPROVER_assume(aws_byte_buf_is_valid(commitment));

    /* Save current state of the data structure */
    struct aws_byte_buf *old_message_id = message_id;
    struct store_byte_from_buffer old_byte_from_message_id;
    save_byte_from_array(message_id->buffer, message_id->len, &old_byte_from_message_id);

    struct aws_byte_buf *old_commitment = commitment;
    struct store_byte_from_buffer old_byte_from_commitment;
    save_byte_from_array(commitment->buffer, commitment->len, &old_byte_from_commitment);

    /* Operation under verification */
    int rv = aws_cryptosdk_private_derive_key(props, content_key, data_key, commitment, message_id);

    /* Postconditions */
    assert(aws_cryptosdk_alg_properties_is_valid(props));
    assert(aws_cryptosdk_content_key_is_valid(content_key));
    assert(aws_cryptosdk_data_key_is_valid(data_key));
    assert(aws_byte_buf_is_valid(message_id));
    assert_byte_buf_equivalence(message_id, old_message_id, &old_byte_from_message_id);
    assert(aws_byte_buf_is_valid(commitment));
    assert_byte_buf_equivalence(commitment, old_commitment, &old_byte_from_commitment);
    if (props->msg_format_version == AWS_CRYPTOSDK_HEADER_VERSION_1_0) {
        if (rv == AWS_CRYPTOSDK_ERR_CRYPTO_UNKNOWN) {
            assert(commitment->len != 0);
        } else {
            if (rv == AWS_CRYPTOSDK_ERR_UNSUPPORTED_FORMAT) {
                assert(message_id->len != MSG_ID_LEN);
            } else if (rv == AWS_OP_SUCCESS && aws_cryptosdk_which_sha(props->alg_id) == AWS_CRYPTOSDK_NOSHA) {
                assert(key_contents_match(content_key, data_key, props->data_key_len));
            }
        }
    } else if (props->msg_format_version == AWS_CRYPTOSDK_HEADER_VERSION_2_0) {
        if (rv == AWS_CRYPTOSDK_ERR_CRYPTO_UNKNOWN) {
            assert(commitment->capacity < props->commitment_len);
        } else if (rv == AWS_CRYPTOSDK_ERR_UNSUPPORTED_FORMAT) {
            assert(message_id->len != MSG_ID_LEN_V2 || aws_cryptosdk_which_sha(props->alg_id) == AWS_CRYPTOSDK_NOSHA);
        }
    } else {
        assert(rv == AWS_CRYPTOSDK_ERR_UNSUPPORTED_FORMAT);
    }
}