int aws_cryptosdk_hkdf()

in verification/cbmc/proofs/aws_cryptosdk_hkdf/aws_cryptosdk_hkdf_harness.c [22:81]

• 43 lines of code
• 1 McCabe index (conditional complexity)

int aws_cryptosdk_hkdf(
    struct aws_byte_buf *okm,
    enum aws_cryptosdk_sha_version which_sha,
    const struct aws_byte_buf *salt,
    const struct aws_byte_buf *ikm,
    const struct aws_byte_buf *info);

void aws_cryptosdk_hkdf_harness() {
    /* arguments */

    struct aws_byte_buf okm;
    enum aws_cryptosdk_alg_id alg_id;
    enum aws_cryptosdk_sha_version which_sha = aws_cryptosdk_which_sha(alg_id);

    struct aws_byte_buf salt;
    struct aws_byte_buf ikm;
    struct aws_byte_buf info;

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

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

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

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

    /* save current state of the data structure */
    struct aws_byte_buf old_salt = salt;
    struct store_byte_from_buffer old_byte_from_salt;
    save_byte_from_array(salt.buffer, salt.len, &old_byte_from_salt);

    struct aws_byte_buf old_ikm = ikm;
    struct store_byte_from_buffer old_byte_from_ikm;
    save_byte_from_array(ikm.buffer, ikm.len, &old_byte_from_ikm);

    struct aws_byte_buf old_info = info;
    struct store_byte_from_buffer old_byte_from_info;
    save_byte_from_array(info.buffer, info.len, &old_byte_from_info);

    aws_cryptosdk_hkdf(&okm, which_sha, &salt, &ikm, &info);

    /* assertions */
    assert(aws_byte_buf_is_valid(&salt));
    assert(aws_byte_buf_is_valid(&ikm));
    assert(aws_byte_buf_is_valid(&info));

    assert_byte_buf_equivalence(&salt, &old_salt, &old_byte_from_salt);
    assert_byte_buf_equivalence(&ikm, &old_ikm, &old_byte_from_ikm);
    assert_byte_buf_equivalence(&info, &old_info, &old_byte_from_info);

    assert(aws_byte_buf_is_valid(&okm));
}