void aws_cryptosdk_aes_gcm_encrypt_harness()

in verification/cbmc/proofs/aws_cryptosdk_aes_gcm_encrypt/aws_cryptosdk_aes_gcm_encrypt_harness.c [23:87]

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

void aws_cryptosdk_aes_gcm_encrypt_harness() {
    /* Nondet Input */
    struct aws_byte_buf cipher;
    struct aws_byte_buf tag;
    struct aws_byte_cursor plain;
    struct aws_byte_cursor iv;
    struct aws_byte_cursor aad;
    struct aws_string *key;

    /* Assumptions */
    __CPROVER_assume(aws_byte_buf_is_bounded(&cipher, MAX_BUFFER_SIZE));
    ensure_byte_buf_has_allocated_buffer_member(&cipher);
    __CPROVER_assume(cipher.buffer != NULL);
    __CPROVER_assume(aws_byte_buf_is_valid(&cipher));

    __CPROVER_assume(aws_byte_buf_is_bounded(&tag, MAX_BUFFER_SIZE));
    ensure_byte_buf_has_allocated_buffer_member(&tag);
    __CPROVER_assume(aws_byte_buf_is_valid(&tag));

    __CPROVER_assume(aws_byte_cursor_is_bounded(&plain, MAX_BUFFER_SIZE));
    ensure_byte_cursor_has_allocated_buffer_member(&plain);
    __CPROVER_assume(aws_byte_cursor_is_valid(&plain));

    __CPROVER_assume(aws_byte_cursor_is_bounded(&iv, MAX_BUFFER_SIZE));
    ensure_byte_cursor_has_allocated_buffer_member(&iv);
    __CPROVER_assume(aws_byte_cursor_is_valid(&iv));

    __CPROVER_assume(aws_byte_cursor_is_bounded(&aad, MAX_BUFFER_SIZE));
    ensure_byte_cursor_has_allocated_buffer_member(&aad);
    __CPROVER_assume(aws_byte_cursor_is_valid(&aad));

    key = ensure_string_is_allocated_nondet_length();
    __CPROVER_assume(key != NULL);
    __CPROVER_assume(aws_string_is_valid(key));

    /* Save current state of the data structure */
    struct aws_byte_cursor old_plain = plain;
    struct store_byte_from_buffer old_byte_from_plain;
    save_byte_from_array(plain.ptr, plain.len, &old_byte_from_plain);

    struct aws_byte_cursor old_iv = iv;
    struct store_byte_from_buffer old_byte_from_iv;
    save_byte_from_array(iv.ptr, iv.len, &old_byte_from_iv);

    struct aws_byte_cursor old_aad = aad;
    struct store_byte_from_buffer old_byte_from_aad;
    save_byte_from_array(aad.ptr, aad.len, &old_byte_from_aad);

    /* Operation under verification */
    if (aws_cryptosdk_aes_gcm_encrypt(&cipher, &tag, plain, iv, aad, key) == AWS_OP_SUCCESS) {
        /* Postconditions */
        assert(cipher.len == plain.len);
    }
    /* Postconditions */
    assert(aws_byte_buf_is_valid(&cipher));
    if (plain.len != 0) {
        assert_byte_from_buffer_matches(plain.ptr, &old_byte_from_plain);
    }
    if (iv.len != 0) {
        assert_byte_from_buffer_matches(iv.ptr, &old_byte_from_iv);
    }
    if (aad.len != 0) {
        assert_byte_from_buffer_matches(aad.ptr, &old_byte_from_aad);
    }
}