Skip to content

refactor: always use EVP hashing #5121

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Feb 20, 2025
Merged

refactor: always use EVP hashing #5121

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
911c7ca
refactor: always use EVP hashing
lrstewart Feb 18, 2025
152933e
disable HMAC SAW proof that requires low-level :/
lrstewart Feb 20, 2025
fb0b3dd
just remove the saw test completely
lrstewart Feb 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 0 additions & 10 deletions codebuild/spec/buildspec_generalbatch.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,16 +16,6 @@ version: 0.2

batch:
build-list:
- buildspec: codebuild/spec/buildspec_ubuntu.yml
env:
compute-type: BUILD_GENERAL1_LARGE
image: 024603541914.dkr.ecr.us-west-2.amazonaws.com/docker:ubuntu18codebuild
privileged-mode: true
variables:
GCC_VERSION: NONE
SAW: true
TESTS: sawHMACPlus
identifier: sawHMACPlus
- buildspec: codebuild/spec/buildspec_ubuntu.yml
env:
compute-type: BUILD_GENERAL1_LARGE
Expand Down
181 changes: 7 additions & 174 deletions crypto/s2n_hash.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,14 +35,14 @@ static bool s2n_use_custom_md5_sha1()
#endif
}

static bool s2n_use_evp_impl()
{
return s2n_is_in_fips_mode();
}

/* This is currently only used by s2n_evp_signing
* to determine whether or not to use EVP signing.
* Historically we only used EVP signing for FIPS.
* To avoid a premature behavior change, consider FIPS a requirement.
*/
bool s2n_hash_evp_fully_supported()
{
return s2n_use_evp_impl() && !s2n_use_custom_md5_sha1();
return s2n_is_in_fips_mode() && !s2n_use_custom_md5_sha1();
}

S2N_RESULT s2n_hash_algorithms_init()
Expand Down Expand Up @@ -174,160 +174,6 @@ int s2n_hash_is_ready_for_input(struct s2n_hash_state *state)
return state->is_ready_for_input;
}

static int s2n_low_level_hash_new(struct s2n_hash_state *state)
{
/* s2n_hash_new will always call the corresponding implementation of the s2n_hash
* being used. For the s2n_low_level_hash implementation, new is a no-op.
*/

*state = (struct s2n_hash_state){ 0 };
return S2N_SUCCESS;
}

static int s2n_low_level_hash_init(struct s2n_hash_state *state, s2n_hash_algorithm alg)
{
switch (alg) {
case S2N_HASH_NONE:
break;
case S2N_HASH_MD5:
POSIX_GUARD_OSSL(MD5_Init(&state->digest.low_level.md5), S2N_ERR_HASH_INIT_FAILED);
break;
case S2N_HASH_SHA1:
POSIX_GUARD_OSSL(SHA1_Init(&state->digest.low_level.sha1), S2N_ERR_HASH_INIT_FAILED);
break;
case S2N_HASH_SHA224:
POSIX_GUARD_OSSL(SHA224_Init(&state->digest.low_level.sha224), S2N_ERR_HASH_INIT_FAILED);
break;
case S2N_HASH_SHA256:
POSIX_GUARD_OSSL(SHA256_Init(&state->digest.low_level.sha256), S2N_ERR_HASH_INIT_FAILED);
break;
case S2N_HASH_SHA384:
POSIX_GUARD_OSSL(SHA384_Init(&state->digest.low_level.sha384), S2N_ERR_HASH_INIT_FAILED);
break;
case S2N_HASH_SHA512:
POSIX_GUARD_OSSL(SHA512_Init(&state->digest.low_level.sha512), S2N_ERR_HASH_INIT_FAILED);
break;
case S2N_HASH_MD5_SHA1:
POSIX_GUARD_OSSL(SHA1_Init(&state->digest.low_level.md5_sha1.sha1), S2N_ERR_HASH_INIT_FAILED);
POSIX_GUARD_OSSL(MD5_Init(&state->digest.low_level.md5_sha1.md5), S2N_ERR_HASH_INIT_FAILED);
break;

default:
POSIX_BAIL(S2N_ERR_HASH_INVALID_ALGORITHM);
}

state->alg = alg;
state->is_ready_for_input = 1;
state->currently_in_hash = 0;

return 0;
}

static int s2n_low_level_hash_update(struct s2n_hash_state *state, const void *data, uint32_t size)
{
POSIX_ENSURE(state->is_ready_for_input, S2N_ERR_HASH_NOT_READY);

switch (state->alg) {
case S2N_HASH_NONE:
break;
case S2N_HASH_MD5:
POSIX_GUARD_OSSL(MD5_Update(&state->digest.low_level.md5, data, size), S2N_ERR_HASH_UPDATE_FAILED);
break;
case S2N_HASH_SHA1:
POSIX_GUARD_OSSL(SHA1_Update(&state->digest.low_level.sha1, data, size), S2N_ERR_HASH_UPDATE_FAILED);
break;
case S2N_HASH_SHA224:
POSIX_GUARD_OSSL(SHA224_Update(&state->digest.low_level.sha224, data, size), S2N_ERR_HASH_UPDATE_FAILED);
break;
case S2N_HASH_SHA256:
POSIX_GUARD_OSSL(SHA256_Update(&state->digest.low_level.sha256, data, size), S2N_ERR_HASH_UPDATE_FAILED);
break;
case S2N_HASH_SHA384:
POSIX_GUARD_OSSL(SHA384_Update(&state->digest.low_level.sha384, data, size), S2N_ERR_HASH_UPDATE_FAILED);
break;
case S2N_HASH_SHA512:
POSIX_GUARD_OSSL(SHA512_Update(&state->digest.low_level.sha512, data, size), S2N_ERR_HASH_UPDATE_FAILED);
break;
case S2N_HASH_MD5_SHA1:
POSIX_GUARD_OSSL(SHA1_Update(&state->digest.low_level.md5_sha1.sha1, data, size), S2N_ERR_HASH_UPDATE_FAILED);
POSIX_GUARD_OSSL(MD5_Update(&state->digest.low_level.md5_sha1.md5, data, size), S2N_ERR_HASH_UPDATE_FAILED);
break;
default:
POSIX_BAIL(S2N_ERR_HASH_INVALID_ALGORITHM);
}

POSIX_ENSURE(size <= (UINT64_MAX - state->currently_in_hash), S2N_ERR_INTEGER_OVERFLOW);
state->currently_in_hash += size;

return S2N_SUCCESS;
}

static int s2n_low_level_hash_digest(struct s2n_hash_state *state, void *out, uint32_t size)
{
POSIX_ENSURE(state->is_ready_for_input, S2N_ERR_HASH_NOT_READY);

switch (state->alg) {
case S2N_HASH_NONE:
break;
case S2N_HASH_MD5:
POSIX_ENSURE_EQ(size, MD5_DIGEST_LENGTH);
POSIX_GUARD_OSSL(MD5_Final(out, &state->digest.low_level.md5), S2N_ERR_HASH_DIGEST_FAILED);
break;
case S2N_HASH_SHA1:
POSIX_ENSURE_EQ(size, SHA_DIGEST_LENGTH);
POSIX_GUARD_OSSL(SHA1_Final(out, &state->digest.low_level.sha1), S2N_ERR_HASH_DIGEST_FAILED);
break;
case S2N_HASH_SHA224:
POSIX_ENSURE_EQ(size, SHA224_DIGEST_LENGTH);
POSIX_GUARD_OSSL(SHA224_Final(out, &state->digest.low_level.sha224), S2N_ERR_HASH_DIGEST_FAILED);
break;
case S2N_HASH_SHA256:
POSIX_ENSURE_EQ(size, SHA256_DIGEST_LENGTH);
POSIX_GUARD_OSSL(SHA256_Final(out, &state->digest.low_level.sha256), S2N_ERR_HASH_DIGEST_FAILED);
break;
case S2N_HASH_SHA384:
POSIX_ENSURE_EQ(size, SHA384_DIGEST_LENGTH);
POSIX_GUARD_OSSL(SHA384_Final(out, &state->digest.low_level.sha384), S2N_ERR_HASH_DIGEST_FAILED);
break;
case S2N_HASH_SHA512:
POSIX_ENSURE_EQ(size, SHA512_DIGEST_LENGTH);
POSIX_GUARD_OSSL(SHA512_Final(out, &state->digest.low_level.sha512), S2N_ERR_HASH_DIGEST_FAILED);
break;
case S2N_HASH_MD5_SHA1:
POSIX_ENSURE_EQ(size, MD5_DIGEST_LENGTH + SHA_DIGEST_LENGTH);
POSIX_GUARD_OSSL(SHA1_Final(((uint8_t *) out) + MD5_DIGEST_LENGTH, &state->digest.low_level.md5_sha1.sha1), S2N_ERR_HASH_DIGEST_FAILED);
POSIX_GUARD_OSSL(MD5_Final(out, &state->digest.low_level.md5_sha1.md5), S2N_ERR_HASH_DIGEST_FAILED);
break;
default:
POSIX_BAIL(S2N_ERR_HASH_INVALID_ALGORITHM);
}

state->currently_in_hash = 0;
state->is_ready_for_input = 0;
return 0;
}

static int s2n_low_level_hash_copy(struct s2n_hash_state *to, struct s2n_hash_state *from)
{
POSIX_CHECKED_MEMCPY(to, from, sizeof(struct s2n_hash_state));
return 0;
}

static int s2n_low_level_hash_reset(struct s2n_hash_state *state)
{
/* hash_init resets the ready_for_input and currently_in_hash fields. */
return s2n_low_level_hash_init(state, state->alg);
}

static int s2n_low_level_hash_free(struct s2n_hash_state *state)
{
/* s2n_hash_free will always call the corresponding implementation of the s2n_hash
* being used. For the s2n_low_level_hash implementation, free is a no-op.
*/
state->is_ready_for_input = 0;
return S2N_SUCCESS;
}

static int s2n_evp_hash_new(struct s2n_hash_state *state)
{
POSIX_ENSURE_REF(state->digest.high_level.evp.ctx = S2N_EVP_MD_CTX_NEW());
Expand Down Expand Up @@ -480,16 +326,6 @@ static int s2n_evp_hash_free(struct s2n_hash_state *state)
return S2N_SUCCESS;
}

static const struct s2n_hash s2n_low_level_hash = {
.alloc = &s2n_low_level_hash_new,
.init = &s2n_low_level_hash_init,
.update = &s2n_low_level_hash_update,
.digest = &s2n_low_level_hash_digest,
.copy = &s2n_low_level_hash_copy,
.reset = &s2n_low_level_hash_reset,
.free = &s2n_low_level_hash_free,
};

static const struct s2n_hash s2n_evp_hash = {
.alloc = &s2n_evp_hash_new,
.init = &s2n_evp_hash_init,
Expand All @@ -502,10 +338,7 @@ static const struct s2n_hash s2n_evp_hash = {

static int s2n_hash_set_impl(struct s2n_hash_state *state)
{
state->hash_impl = &s2n_low_level_hash;
if (s2n_use_evp_impl()) {
state->hash_impl = &s2n_evp_hash;
}
state->hash_impl = &s2n_evp_hash;
return S2N_SUCCESS;
}

Expand Down
23 changes: 4 additions & 19 deletions crypto/s2n_hash.h
View file
Open in desktop
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Running our s2n_mem_usage_test with outputs, I see "VmData after handshakes" as 24391680 before this change and 23609344 after. With 252 connections used for testing, that's ~3k bytes saved per connection.

Should the thresholds in s2n_mem_usage_test be reduced at all?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure it's enough of a benefit for that.

Min VmData diff allowed:       21288960
Max VmData diff allowed:       28385280

So 24391680 was pretty much right in the middle of that window, and 23609344 doesn't seem like enough of an adjustment to deal with updating the test, which can be tricky to get right for all envs :(

Maybe I should update it in a separate PR, so we can easily revert it if it causes issues? There are some other tweaks I'd like to try to make to that test to make it less difficult to deal with.

Original file line number Diff line number Diff line change
Expand Up @@ -37,43 +37,28 @@ typedef enum {
S2N_HASH_ALGS_COUNT
} s2n_hash_algorithm;

/* The low_level_digest stores all OpenSSL structs that are alg-specific to be used with OpenSSL's low-level hash API's. */
union s2n_hash_low_level_digest {
MD5_CTX md5;
SHA_CTX sha1;
SHA256_CTX sha224;
SHA256_CTX sha256;
SHA512_CTX sha384;
SHA512_CTX sha512;
struct {
MD5_CTX md5;
SHA_CTX sha1;
} md5_sha1;
};

/* The evp_digest stores all OpenSSL structs to be used with OpenSSL's EVP hash API's. */
struct s2n_hash_evp_digest {
struct s2n_evp_digest evp;
/* Always store a secondary evp_digest to allow resetting a hash_state to MD5_SHA1 from another alg. */
struct s2n_evp_digest evp_md5_secondary;
};

/* s2n_hash_state stores the s2n_hash implementation being used (low-level or EVP),
* the hash algorithm being used at the time, and either low_level or high_level (EVP) OpenSSL digest structs.
/* s2n_hash_state stores the state and a reference to the implementation being used.
* Currently only EVP hashing is supported, so the only state are EVP_MD contexts.
*/
struct s2n_hash_state {
const struct s2n_hash *hash_impl;
s2n_hash_algorithm alg;
uint8_t is_ready_for_input;
uint64_t currently_in_hash;
union {
union s2n_hash_low_level_digest low_level;
struct s2n_hash_evp_digest high_level;
} digest;
};

/* The s2n hash implementation is abstracted to allow for separate implementations, using
* either OpenSSL's low-level algorithm-specific API's or OpenSSL's EVP API's.
/* The s2n hash implementation is abstracted to allow for separate implementations.
* Currently the only implementation uses the EVP APIs.
*/
Comment on lines -75 to 62
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know we only have one implementation now, but it seemed like a bit of a waste to rip out the mechanism to handle multiple implementations. We might need another implementation someday, and I don't think this abstraction adds much complexity.

struct s2n_hash {
int (*alloc)(struct s2n_hash_state *state);
Expand Down
4 changes: 0 additions & 4 deletions tests/cbmc/proofs/s2n_hash_copy/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,10 +36,6 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_init
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_new
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset

UNWINDSET +=

Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_digest/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

# We abstract these functions because manual inspection demonstrates they are unreachable.
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_update
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_update

UNWINDSET +=

Expand Down
3 changes: 0 additions & 3 deletions tests/cbmc/proofs/s2n_hash_free/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,9 +33,6 @@ PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_init
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_new
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset

UNWINDSET +=

Expand Down
19 changes: 6 additions & 13 deletions tests/cbmc/proofs/s2n_hash_free/s2n_hash_free_harness.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,24 +35,17 @@ void s2n_hash_free_harness()
assert(s2n_hash_free(state) == S2N_SUCCESS);
if (state != NULL) {
assert(state->hash_impl->free != NULL);
if (s2n_is_in_fips_mode()) {
assert(state->digest.high_level.evp.ctx == NULL);
assert(state->digest.high_level.evp_md5_secondary.ctx == NULL);
assert_rc_decrement_on_hash_state(&saved_hash_state);
} else {
assert_rc_unchanged_on_hash_state(&saved_hash_state);
}
assert(state->digest.high_level.evp.ctx == NULL);
assert(state->digest.high_level.evp_md5_secondary.ctx == NULL);
assert_rc_decrement_on_hash_state(&saved_hash_state);
assert(state->is_ready_for_input == 0);
}

/* Cleanup after expected error cases, for memory leak check. */
if (state != NULL) {
/* 1. `free` leftover EVP_MD_CTX objects if `s2n_is_in_fips_mode`,
since `s2n_hash_free` is a NO-OP in that case. */
if (!s2n_is_in_fips_mode()) {
S2N_EVP_MD_CTX_FREE(state->digest.high_level.evp.ctx);
S2N_EVP_MD_CTX_FREE(state->digest.high_level.evp_md5_secondary.ctx);
}
/* 1. `free` leftover EVP_MD_CTX objects */
S2N_EVP_MD_CTX_FREE(state->digest.high_level.evp.ctx);
S2N_EVP_MD_CTX_FREE(state->digest.high_level.evp_md5_secondary.ctx);

/* 2. `free` leftover reference-counted keys (i.e. those with non-zero ref-count),
since they are not automatically `free`d until their ref count reaches 0. */
Expand Down
4 changes: 0 additions & 4 deletions tests/cbmc/proofs/s2n_hash_init/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,10 +30,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c

# We abstract these functions because manual inspection demonstrates they are unreachable.
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_copy
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_copy
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_new
Expand Down
3 changes: 0 additions & 3 deletions tests/cbmc/proofs/s2n_hash_new/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,6 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c

# We abstract these functions because manual inspection demonstrates they are unreachable.
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_init
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free
Expand Down
2 changes: 0 additions & 2 deletions tests/cbmc/proofs/s2n_hash_reset/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
# We abstract these functions because manual inspection demonstrates they are unreachable.
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_new
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new

UNWINDSET +=

Expand Down
1 change: 0 additions & 1 deletion tests/cbmc/proofs/s2n_hash_update/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

# We abstract these functions because manual inspection demonstrates they are unreachable.
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_digest
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_digest

UNWINDSET +=

Expand Down
4 changes: 0 additions & 4 deletions tests/cbmc/proofs/s2n_hmac_copy/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,10 +37,6 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_init
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_new
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset

UNWINDSET +=

Expand Down
3 changes: 0 additions & 3 deletions tests/cbmc/proofs/s2n_hmac_free/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,9 +34,6 @@ PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.c
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_init
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_new
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset

UNWINDSET +=

Expand Down
Loading
Loading