int __CPROVER_file_local_session_decrypt_c_derive_data_key()

in verification/cbmc/proofs/derive_data_key/derive_data_key_harness.c [26:86]

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

int __CPROVER_file_local_session_decrypt_c_derive_data_key(
    struct aws_cryptosdk_session *session, struct aws_cryptosdk_dec_materials *materials);

void derive_data_key_harness() {
    /* Setup functions include nondet. allocation and common assumptions */
    struct aws_cryptosdk_session *session =
        session_setup(MAX_TABLE_SIZE, MAX_TRACE_LIST_ITEMS, MAX_EDK_LIST_ITEMS, MAX_BUFFER_SIZE, MAX_STRING_LEN);
    struct aws_cryptosdk_dec_materials *materials =
        dec_materials_setup(MAX_TRACE_LIST_ITEMS, MAX_BUFFER_SIZE, MAX_STRING_LEN);

    /* Assumptions */
    if (session->alg_props == NULL) {
        struct aws_cryptosdk_alg_properties *props = ensure_alg_properties_attempt_allocation(MAX_STRING_LEN);
        __CPROVER_assume(aws_cryptosdk_alg_properties_is_valid(props));
        session->alg_props = props;
    }
    __CPROVER_assume(aws_cryptosdk_commitment_policy_is_valid(session->commitment_policy));
    __CPROVER_assume(session->alg_props->commitment_len <= sizeof(session->key_commitment_arr));

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

    struct aws_byte_buf *old_alg_suite_data = &session->header.alg_suite_data;
    struct store_byte_from_buffer old_byte_from_alg_suite_data;
    save_byte_from_array(
        session->header.alg_suite_data.buffer, session->header.alg_suite_data.len, &old_byte_from_alg_suite_data);

    struct aws_byte_buf *old_unencrypted_data_key = &materials->unencrypted_data_key;
    struct store_byte_from_buffer old_byte_from_unencrypted_data_key;
    save_byte_from_array(
        materials->unencrypted_data_key.buffer,
        materials->unencrypted_data_key.len,
        &old_byte_from_unencrypted_data_key);

    /* Operation under verification */
    int rv = __CPROVER_file_local_session_decrypt_c_derive_data_key(session, materials);

    /* Postconditions */
    if (rv == AWS_OP_ERR) {
        int last_err = aws_last_error();
        if (session->alg_props->msg_format_version == AWS_CRYPTOSDK_HEADER_VERSION_1_0) {
            if (last_err == AWS_CRYPTOSDK_ERR_UNSUPPORTED_FORMAT) {
                assert(session->header.message_id.len != MSG_ID_LEN);
            }
        } else if (session->alg_props->msg_format_version == AWS_CRYPTOSDK_HEADER_VERSION_2_0) {
            if (last_err == AWS_CRYPTOSDK_ERR_UNSUPPORTED_FORMAT) {
                assert(
                    session->header.message_id.len != MSG_ID_LEN_V2 ||
                    aws_cryptosdk_which_sha(session->alg_props->alg_id) == AWS_CRYPTOSDK_NOSHA);
            }
        }
    }
    assert(aws_cryptosdk_session_is_valid(session));
    assert(aws_cryptosdk_dec_materials_is_valid(materials));
    assert_byte_buf_equivalence(&session->header.alg_suite_data, old_alg_suite_data, &old_byte_from_alg_suite_data);
    assert_byte_buf_equivalence(&session->header.message_id, old_message_id, &old_byte_from_message_id);
    assert_byte_buf_equivalence(
        &materials->unencrypted_data_key, old_unencrypted_data_key, &old_byte_from_unencrypted_data_key);
}