diff --git a/crypto/s2n_evp.c b/crypto/s2n_evp.c index 8ae88205e7e..d0adbb1acfc 100644 --- a/crypto/s2n_evp.c +++ b/crypto/s2n_evp.c @@ -15,39 +15,6 @@ #include "crypto/s2n_evp.h" -#include "crypto/s2n_fips.h" -#include "error/s2n_errno.h" -#include "utils/s2n_safety.h" - -int s2n_digest_allow_md5_for_fips(struct s2n_evp_digest *evp_digest) -{ - POSIX_ENSURE_REF(evp_digest); - /* This is only to be used for EVP digests that will require MD5 to be used - * to comply with the TLS 1.0 and 1.1 RFC's for the PRF. MD5 cannot be used - * outside of the TLS 1.0 and 1.1 PRF when in FIPS mode. - */ - S2N_ERROR_IF(!s2n_is_in_fips_mode() || (evp_digest->ctx == NULL), S2N_ERR_ALLOW_MD5_FOR_FIPS_FAILED); - -#if !defined(OPENSSL_IS_BORINGSSL) && !defined(OPENSSL_IS_AWSLC) - EVP_MD_CTX_set_flags(evp_digest->ctx, EVP_MD_CTX_FLAG_NON_FIPS_ALLOW); -#endif - return S2N_SUCCESS; -} - -S2N_RESULT s2n_digest_is_md5_allowed_for_fips(struct s2n_evp_digest *evp_digest, bool *out) -{ - RESULT_ENSURE_REF(out); - *out = false; -#if !defined(OPENSSL_IS_BORINGSSL) && !defined(OPENSSL_IS_AWSLC) - if (s2n_is_in_fips_mode() && evp_digest && evp_digest->ctx && EVP_MD_CTX_test_flags(evp_digest->ctx, EVP_MD_CTX_FLAG_NON_FIPS_ALLOW)) { - /* s2n is in FIPS mode and the EVP digest allows MD5. */ - *out = true; - } -#else - if (s2n_is_in_fips_mode()) { - /* If s2n is in FIPS mode and built with AWS-LC or BoringSSL, there are no flags to check in the EVP digest to allow MD5. */ - *out = true; - } -#endif - return S2N_RESULT_OK; -} +/* + * TODO: update all CBMC proofs that depend on this file, then delete. + */ diff --git a/crypto/s2n_evp.h b/crypto/s2n_evp.h index 088deb888c7..8764d1ade81 100644 --- a/crypto/s2n_evp.h +++ b/crypto/s2n_evp.h @@ -51,6 +51,3 @@ struct s2n_evp_hmac_state { */ #define S2N_EVP_PKEY_CTX_set_signature_md(ctx, md) \ EVP_PKEY_CTX_set_signature_md(ctx, (EVP_MD *) (uintptr_t) md) - -int s2n_digest_allow_md5_for_fips(struct s2n_evp_digest *evp_digest); -S2N_RESULT s2n_digest_is_md5_allowed_for_fips(struct s2n_evp_digest *evp_digest, bool *out); diff --git a/crypto/s2n_hash.c b/crypto/s2n_hash.c index f249cd63088..8bd57ba563b 100644 --- a/crypto/s2n_hash.c +++ b/crypto/s2n_hash.c @@ -113,8 +113,6 @@ bool s2n_hash_is_available(s2n_hash_algorithm alg) switch (alg) { case S2N_HASH_MD5: case S2N_HASH_MD5_SHA1: - /* return false if in FIPS mode, as MD5 algs are not available in FIPS mode. */ - return !s2n_is_in_fips_mode(); case S2N_HASH_NONE: case S2N_HASH_SHA1: case S2N_HASH_SHA224: @@ -301,20 +299,6 @@ static int s2n_evp_hash_new(struct s2n_hash_state *state) return S2N_SUCCESS; } -static int s2n_evp_hash_allow_md5_for_fips(struct s2n_hash_state *state) -{ - /* This is only to be used for s2n_hash_states that will require MD5 to be used - * to comply with the TLS 1.0 and 1.1 RFC's for the PRF. MD5 cannot be used - * outside of the TLS 1.0 and 1.1 PRF when in FIPS mode. When needed, this must - * be called prior to s2n_hash_init(). - */ - POSIX_GUARD(s2n_digest_allow_md5_for_fips(&state->digest.high_level.evp)); - if (s2n_use_custom_md5_sha1()) { - POSIX_GUARD(s2n_digest_allow_md5_for_fips(&state->digest.high_level.evp_md5_secondary)); - } - return S2N_SUCCESS; -} - static int s2n_evp_hash_init(struct s2n_hash_state *state, s2n_hash_algorithm alg) { POSIX_ENSURE_REF(state->digest.high_level.evp.ctx); @@ -419,32 +403,16 @@ static int s2n_evp_hash_copy(struct s2n_hash_state *to, struct s2n_hash_state *f POSIX_GUARD_OSSL(EVP_MD_CTX_copy_ex(to->digest.high_level.evp_md5_secondary.ctx, from->digest.high_level.evp_md5_secondary.ctx), S2N_ERR_HASH_COPY_FAILED); } - bool is_md5_allowed_for_fips = false; - POSIX_GUARD_RESULT(s2n_digest_is_md5_allowed_for_fips(&from->digest.high_level.evp, &is_md5_allowed_for_fips)); - if (is_md5_allowed_for_fips && (from->alg == S2N_HASH_MD5 || from->alg == S2N_HASH_MD5_SHA1)) { - POSIX_GUARD(s2n_hash_allow_md5_for_fips(to)); - } return S2N_SUCCESS; } static int s2n_evp_hash_reset(struct s2n_hash_state *state) { - int reset_md5_for_fips = 0; - bool is_md5_allowed_for_fips = false; - POSIX_GUARD_RESULT(s2n_digest_is_md5_allowed_for_fips(&state->digest.high_level.evp, &is_md5_allowed_for_fips)); - if ((state->alg == S2N_HASH_MD5 || state->alg == S2N_HASH_MD5_SHA1) && is_md5_allowed_for_fips) { - reset_md5_for_fips = 1; - } - POSIX_GUARD_OSSL(S2N_EVP_MD_CTX_RESET(state->digest.high_level.evp.ctx), S2N_ERR_HASH_WIPE_FAILED); if (state->alg == S2N_HASH_MD5_SHA1 && s2n_use_custom_md5_sha1()) { POSIX_GUARD_OSSL(S2N_EVP_MD_CTX_RESET(state->digest.high_level.evp_md5_secondary.ctx), S2N_ERR_HASH_WIPE_FAILED); } - if (reset_md5_for_fips) { - POSIX_GUARD(s2n_hash_allow_md5_for_fips(state)); - } - /* hash_init resets the ready_for_input and currently_in_hash fields. */ return s2n_evp_hash_init(state, state->alg); } @@ -465,7 +433,6 @@ static int s2n_evp_hash_free(struct s2n_hash_state *state) static const struct s2n_hash s2n_low_level_hash = { .alloc = &s2n_low_level_hash_new, - .allow_md5_for_fips = NULL, .init = &s2n_low_level_hash_init, .update = &s2n_low_level_hash_update, .digest = &s2n_low_level_hash_digest, @@ -476,7 +443,6 @@ static const struct s2n_hash s2n_low_level_hash = { static const struct s2n_hash s2n_evp_hash = { .alloc = &s2n_evp_hash_new, - .allow_md5_for_fips = &s2n_evp_hash_allow_md5_for_fips, .init = &s2n_evp_hash_init, .update = &s2n_evp_hash_update, .digest = &s2n_evp_hash_digest, @@ -514,19 +480,6 @@ S2N_RESULT s2n_hash_state_validate(struct s2n_hash_state *state) return S2N_RESULT_OK; } -int s2n_hash_allow_md5_for_fips(struct s2n_hash_state *state) -{ - POSIX_ENSURE_REF(state); - /* Ensure that hash_impl is set, as it may have been reset for s2n_hash_state on s2n_connection_wipe. - * When in FIPS mode, the EVP API's must be used for hashes. - */ - POSIX_GUARD(s2n_hash_set_impl(state)); - - POSIX_ENSURE_REF(state->hash_impl->allow_md5_for_fips); - - return state->hash_impl->allow_md5_for_fips(state); -} - int s2n_hash_init(struct s2n_hash_state *state, s2n_hash_algorithm alg) { POSIX_ENSURE_REF(state); @@ -535,15 +488,8 @@ int s2n_hash_init(struct s2n_hash_state *state, s2n_hash_algorithm alg) */ POSIX_GUARD(s2n_hash_set_impl(state)); - bool is_md5_allowed_for_fips = false; - POSIX_GUARD_RESULT(s2n_digest_is_md5_allowed_for_fips(&state->digest.high_level.evp, &is_md5_allowed_for_fips)); - - if (s2n_hash_is_available(alg) || ((alg == S2N_HASH_MD5 || alg == S2N_HASH_MD5_SHA1) && is_md5_allowed_for_fips)) { - /* s2n will continue to initialize an "unavailable" hash when s2n is in FIPS mode and - * FIPS is forcing the hash to be made available. - */ + if (s2n_hash_is_available(alg)) { POSIX_ENSURE_REF(state->hash_impl->init); - return state->hash_impl->init(state, alg); } else { POSIX_BAIL(S2N_ERR_HASH_INVALID_ALGORITHM); diff --git a/crypto/s2n_hash.h b/crypto/s2n_hash.h index 5b4b20d6534..03643a03e9c 100644 --- a/crypto/s2n_hash.h +++ b/crypto/s2n_hash.h @@ -77,7 +77,6 @@ struct s2n_hash_state { */ struct s2n_hash { int (*alloc)(struct s2n_hash_state *state); - int (*allow_md5_for_fips)(struct s2n_hash_state *state); int (*init)(struct s2n_hash_state *state, s2n_hash_algorithm alg); int (*update)(struct s2n_hash_state *state, const void *data, uint32_t size); int (*digest)(struct s2n_hash_state *state, void *out, uint32_t size); @@ -94,7 +93,6 @@ bool s2n_hash_is_available(s2n_hash_algorithm alg); int s2n_hash_is_ready_for_input(struct s2n_hash_state *state); int s2n_hash_new(struct s2n_hash_state *state); S2N_RESULT s2n_hash_state_validate(struct s2n_hash_state *state); -int s2n_hash_allow_md5_for_fips(struct s2n_hash_state *state); int s2n_hash_init(struct s2n_hash_state *state, s2n_hash_algorithm alg); int s2n_hash_update(struct s2n_hash_state *state, const void *data, uint32_t size); int s2n_hash_digest(struct s2n_hash_state *state, void *out, uint32_t size); diff --git a/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips/Makefile b/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips/Makefile deleted file mode 100644 index b057f1c44ce..00000000000 --- a/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips/Makefile +++ /dev/null @@ -1,32 +0,0 @@ -# -# -# Licensed under the Apache License, Version 2.0 (the "License"). You may not use -# this file except in compliance with the License. A copy of the License is -# located at -# -# http://aws.amazon.com/apache2.0/ -# -# or in the "license" file accompanying this file. This file is distributed on an -# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or -# implied. See the License for the specific language governing permissions and -# limitations under the License. - -# Expected runtime is less than 5 seconds. - -CBMCFLAGS += - -PROOF_UID = s2n_digest_allow_md5_for_fips -HARNESS_ENTRY = $(PROOF_UID)_harness -HARNESS_FILE = $(HARNESS_ENTRY).c - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) -PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c -PROOF_SOURCES += $(OPENSSL_SOURCE)/evp_override.c -PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c -PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c - -PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c - -UNWINDSET += - -include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips/cbmc-proof.txt b/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips/cbmc-proof.txt deleted file mode 100644 index 6ed46f1258c..00000000000 --- a/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips/cbmc-proof.txt +++ /dev/null @@ -1 +0,0 @@ -# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips/s2n_digest_allow_md5_for_fips_harness.c b/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips/s2n_digest_allow_md5_for_fips_harness.c deleted file mode 100644 index 6f9d3e6b5d0..00000000000 --- a/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips/s2n_digest_allow_md5_for_fips_harness.c +++ /dev/null @@ -1,40 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * - * Licensed under the Apache License, Version 2.0 (the "License"). - * You may not use this file except in compliance with the License. - * A copy of the License is located at - * - * http://aws.amazon.com/apache2.0 - * - * or in the "license" file accompanying this file. This file is distributed - * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either - * express or implied. See the License for the specific language governing - * permissions and limitations under the License. - */ - -#include - -#include "crypto/s2n_fips.h" -#include "crypto/s2n_evp.h" - -#include - -void s2n_digest_allow_md5_for_fips_harness() -{ - /* Non-deterministic inputs. */ - struct s2n_evp_digest *evp_digest = cbmc_allocate_s2n_evp_digest(); - - /* Save previous state. */ - unsigned long old_flags; - if (evp_digest != NULL && evp_digest->ctx != NULL) old_flags = evp_digest->ctx->flags; - - /* Operation under verification. */ - if (s2n_digest_allow_md5_for_fips(evp_digest) == S2N_SUCCESS) { - /* Post-conditions. */ - assert(evp_digest != NULL); - assert(evp_digest->ctx != NULL); - assert(s2n_is_in_fips_mode()); - assert(evp_digest->ctx->flags == (old_flags | EVP_MD_CTX_FLAG_NON_FIPS_ALLOW)); - } -} diff --git a/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips_boringssl_awslc/Makefile b/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips_boringssl_awslc/Makefile deleted file mode 100644 index 69cca2d3ad4..00000000000 --- a/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips_boringssl_awslc/Makefile +++ /dev/null @@ -1,35 +0,0 @@ -# -# -# Licensed under the Apache License, Version 2.0 (the "License"). You may not use -# this file except in compliance with the License. A copy of the License is -# located at -# -# http://aws.amazon.com/apache2.0/ -# -# or in the "license" file accompanying this file. This file is distributed on an -# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or -# implied. See the License for the specific language governing permissions and -# limitations under the License. - -# Expected runtime is less than 5 seconds. - -DEFINES += -DOPENSSL_IS_BORINGSSL=1 -DEFINES += -DOPENSSL_IS_AWSLC=1 - -CBMCFLAGS += - -PROOF_UID = s2n_digest_allow_md5_for_fips_boringssl_awslc -HARNESS_ENTRY = $(PROOF_UID)_harness -HARNESS_FILE = $(HARNESS_ENTRY).c - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) -PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c -PROOF_SOURCES += $(OPENSSL_SOURCE)/evp_override.c -PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c -PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c - -PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c - -UNWINDSET += - -include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips_boringssl_awslc/cbmc-proof.txt b/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips_boringssl_awslc/cbmc-proof.txt deleted file mode 100644 index 6ed46f1258c..00000000000 --- a/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips_boringssl_awslc/cbmc-proof.txt +++ /dev/null @@ -1 +0,0 @@ -# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips_boringssl_awslc/s2n_digest_allow_md5_for_fips_boringssl_awslc_harness.c b/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips_boringssl_awslc/s2n_digest_allow_md5_for_fips_boringssl_awslc_harness.c deleted file mode 100644 index 2aa159b7251..00000000000 --- a/tests/cbmc/proofs/s2n_digest_allow_md5_for_fips_boringssl_awslc/s2n_digest_allow_md5_for_fips_boringssl_awslc_harness.c +++ /dev/null @@ -1,40 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * - * Licensed under the Apache License, Version 2.0 (the "License"). - * You may not use this file except in compliance with the License. - * A copy of the License is located at - * - * http://aws.amazon.com/apache2.0 - * - * or in the "license" file accompanying this file. This file is distributed - * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either - * express or implied. See the License for the specific language governing - * permissions and limitations under the License. - */ - -#include - -#include "api/s2n.h" -#include "crypto/s2n_evp.h" -#include "crypto/s2n_fips.h" - -#include - -void s2n_digest_allow_md5_for_fips_boringssl_awslc_harness() -{ - /* Non-deterministic inputs. */ - struct s2n_evp_digest *evp_digest = cbmc_allocate_s2n_evp_digest(); - - /* Save previous state. */ - unsigned long old_flags; - if (evp_digest != NULL && evp_digest->ctx != NULL) old_flags = evp_digest->ctx->flags; - - /* Operation under verification. */ - if (s2n_digest_allow_md5_for_fips(evp_digest) == S2N_SUCCESS) { - /* Post-conditions. */ - assert(evp_digest != NULL); - assert(evp_digest->ctx != NULL); - assert(s2n_is_in_fips_mode()); - } -} diff --git a/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/Makefile b/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/Makefile deleted file mode 100644 index 18300977db4..00000000000 --- a/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/Makefile +++ /dev/null @@ -1,32 +0,0 @@ -# -# -# Licensed under the Apache License, Version 2.0 (the "License"). You may not use -# this file except in compliance with the License. A copy of the License is -# located at -# -# http://aws.amazon.com/apache2.0/ -# -# or in the "license" file accompanying this file. This file is distributed on an -# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or -# implied. See the License for the specific language governing permissions and -# limitations under the License. - -# Expected runtime is less than 5 seconds. - -CBMCFLAGS += - -PROOF_UID = s2n_digest_is_md5_allowed_for_fips -HARNESS_ENTRY = $(PROOF_UID)_harness -HARNESS_FILE = $(HARNESS_ENTRY).c - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) -PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c -PROOF_SOURCES += $(OPENSSL_SOURCE)/evp_override.c -PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c -PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c - -PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c - -UNWINDSET += - -include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/cbmc-proof.txt b/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/cbmc-proof.txt deleted file mode 100644 index 6ed46f1258c..00000000000 --- a/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/cbmc-proof.txt +++ /dev/null @@ -1 +0,0 @@ -# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/s2n_digest_is_md5_allowed_for_fips_harness.c b/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/s2n_digest_is_md5_allowed_for_fips_harness.c deleted file mode 100644 index d0fd3fcdd7a..00000000000 --- a/tests/cbmc/proofs/s2n_digest_is_md5_allowed_for_fips/s2n_digest_is_md5_allowed_for_fips_harness.c +++ /dev/null @@ -1,38 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * - * Licensed under the Apache License, Version 2.0 (the "License"). - * You may not use this file except in compliance with the License. - * A copy of the License is located at - * - * http://aws.amazon.com/apache2.0 - * - * or in the "license" file accompanying this file. This file is distributed - * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either - * express or implied. See the License for the specific language governing - * permissions and limitations under the License. - */ - -#include - -#include "crypto/s2n_fips.h" -#include "crypto/s2n_evp.h" -#include "utils/s2n_result.h" - -#include - -void s2n_digest_is_md5_allowed_for_fips_harness() -{ - /* Non-deterministic inputs. */ - struct s2n_evp_digest *evp_digest = cbmc_allocate_s2n_evp_digest(); - bool *out = malloc(sizeof(*out)); - - /* Operation under verification. */ - if (s2n_result_is_ok(s2n_digest_is_md5_allowed_for_fips(evp_digest, out)) && *out) { - /* Post-conditions. */ - assert(evp_digest != NULL); - assert(evp_digest->ctx != NULL); - assert(s2n_is_in_fips_mode()); - assert((evp_digest->ctx->flags & EVP_MD_CTX_FLAG_NON_FIPS_ALLOW)); - } -} diff --git a/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/Makefile b/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/Makefile deleted file mode 100644 index c0c046fd13b..00000000000 --- a/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/Makefile +++ /dev/null @@ -1,42 +0,0 @@ -# -# -# Licensed under the Apache License, Version 2.0 (the "License"). You may not use -# this file except in compliance with the License. A copy of the License is -# located at -# -# http://aws.amazon.com/apache2.0/ -# -# or in the "license" file accompanying this file. This file is distributed on an -# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or -# implied. See the License for the specific language governing permissions and -# limitations under the License. - -# Expected runtime is less than 20 seconds. - -CBMCFLAGS += - -PROOF_UID = s2n_hash_allow_md5_for_fips -HARNESS_ENTRY = $(PROOF_UID)_harness -HARNESS_FILE = $(HARNESS_ENTRY).c - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) -PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c -PROOF_SOURCES += $(OPENSSL_SOURCE)/evp_override.c -PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c - -PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c -PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.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_new -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_evp_hash_new -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 -REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free - -UNWINDSET += - -include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/cbmc-proof.txt b/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/cbmc-proof.txt deleted file mode 100644 index 6ed46f1258c..00000000000 --- a/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/cbmc-proof.txt +++ /dev/null @@ -1 +0,0 @@ -# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/s2n_hash_allow_md5_for_fips_harness.c b/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/s2n_hash_allow_md5_for_fips_harness.c deleted file mode 100644 index f84dce8fa39..00000000000 --- a/tests/cbmc/proofs/s2n_hash_allow_md5_for_fips/s2n_hash_allow_md5_for_fips_harness.c +++ /dev/null @@ -1,35 +0,0 @@ -/* - * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. - * - * Licensed under the Apache License, Version 2.0 (the "License"). - * You may not use this file except in compliance with the License. - * A copy of the License is located at - * - * http://aws.amazon.com/apache2.0 - * - * or in the "license" file accompanying this file. This file is distributed - * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either - * express or implied. See the License for the specific language governing - * permissions and limitations under the License. - */ - -#include - -#include "crypto/s2n_fips.h" -#include "crypto/s2n_hash.h" - -#include - -void s2n_hash_allow_md5_for_fips_harness() -{ - /* Non-deterministic inputs. */ - struct s2n_hash_state *state = cbmc_allocate_s2n_hash_state(); - - /* Operation under verification. */ - if (s2n_hash_allow_md5_for_fips(state) == S2N_SUCCESS) { - /* Post-conditions. */ - assert(s2n_result_is_ok(s2n_hash_state_validate(state))); - assert(IMPLIES(s2n_is_in_fips_mode(), state->hash_impl->allow_md5_for_fips != NULL)); - } - assert(IMPLIES(state != NULL && !s2n_is_in_fips_mode(), state->hash_impl->allow_md5_for_fips == NULL)); -} diff --git a/tests/cbmc/proofs/s2n_hash_is_available/s2n_hash_is_available_harness.c b/tests/cbmc/proofs/s2n_hash_is_available/s2n_hash_is_available_harness.c index adec1521d59..515e8280dfc 100644 --- a/tests/cbmc/proofs/s2n_hash_is_available/s2n_hash_is_available_harness.c +++ b/tests/cbmc/proofs/s2n_hash_is_available/s2n_hash_is_available_harness.c @@ -32,7 +32,6 @@ void s2n_hash_is_available_harness() switch (alg) { case S2N_HASH_MD5: case S2N_HASH_MD5_SHA1: - assert(is_available == !s2n_is_in_fips_mode()); break; case S2N_HASH_NONE: case S2N_HASH_SHA1: case S2N_HASH_SHA224: diff --git a/tests/unit/s2n_ecdsa_test.c b/tests/unit/s2n_ecdsa_test.c index 199b3fe63e0..a768906baa1 100644 --- a/tests/unit/s2n_ecdsa_test.c +++ b/tests/unit/s2n_ecdsa_test.c @@ -164,6 +164,11 @@ int main(int argc, char **argv) continue; } + if (hash_alg == S2N_HASH_MD5 || hash_alg == S2N_HASH_MD5_SHA1) { + /* MD5 is only used for method; RESULT_ENSURE_REF(method); RESULT_GUARD_POSIX(s2n_hash_new(&fingerprint->hash)); - s2n_hash_allow_md5_for_fips(&fingerprint->hash); RESULT_GUARD_POSIX(s2n_hash_init(&fingerprint->hash, method->hash)); return S2N_RESULT_OK; } diff --git a/tls/s2n_handshake_hashes.c b/tls/s2n_handshake_hashes.c index 591e2251f48..29c1d1566ef 100644 --- a/tls/s2n_handshake_hashes.c +++ b/tls/s2n_handshake_hashes.c @@ -67,20 +67,6 @@ static S2N_RESULT s2n_handshake_hashes_free_hashes(struct s2n_handshake_hashes * static S2N_RESULT s2n_handshake_hashes_init_hashes(struct s2n_handshake_hashes *hashes) { - /* Allow MD5 for hash states that are used by the PRF. This is required - * to comply with the TLS 1.0 and 1.1 RFCs and is approved as per - * NIST Special Publication 800-52 Revision 1. - */ - if (s2n_is_in_fips_mode()) { - RESULT_GUARD_POSIX(s2n_hash_allow_md5_for_fips(&hashes->md5)); - - /* Do not check s2n_hash_is_available before initialization. Allow MD5 and - * SHA-1 for both fips and non-fips mode. This is required to perform the - * signature checks in the CertificateVerify message in TLS 1.0 and TLS 1.1. - * This is approved per Nist SP 800-52r1.*/ - RESULT_GUARD_POSIX(s2n_hash_allow_md5_for_fips(&hashes->md5_sha1)); - } - RESULT_GUARD_POSIX(s2n_hash_init(&hashes->md5, S2N_HASH_MD5)); RESULT_GUARD_POSIX(s2n_hash_init(&hashes->sha1, S2N_HASH_SHA1)); RESULT_GUARD_POSIX(s2n_hash_init(&hashes->sha224, S2N_HASH_SHA224)); diff --git a/tls/s2n_prf.c b/tls/s2n_prf.c index 614a8818fa8..168cd06379e 100644 --- a/tls/s2n_prf.c +++ b/tls/s2n_prf.c @@ -152,10 +152,6 @@ static int s2n_sslv3_prf(struct s2n_connection *conn, struct s2n_blob *secret, s struct s2n_hash_state *md5 = workspace; POSIX_GUARD(s2n_hash_reset(md5)); - /* FIPS specifically allows MD5 for the legacy PRF */ - if (s2n_is_in_fips_mode() && conn->actual_protocol_version < S2N_TLS12) { - POSIX_GUARD(s2n_hash_allow_md5_for_fips(workspace)); - } POSIX_GUARD(s2n_hash_init(md5, S2N_HASH_MD5)); POSIX_GUARD(s2n_hash_update(md5, secret->data, secret->size)); POSIX_GUARD(s2n_hash_update(md5, sha_digest, sizeof(sha_digest))); @@ -189,11 +185,6 @@ static int s2n_evp_pkey_p_hash_digest_init(struct s2n_prf_working_space *ws) POSIX_ENSURE_REF(ws->p_hash.evp_hmac.evp_digest.ctx); POSIX_ENSURE_REF(ws->p_hash.evp_hmac.ctx.evp_pkey); - /* Ignore the MD5 check when in FIPS mode to comply with the TLS 1.0 RFC */ - if (s2n_is_in_fips_mode()) { - POSIX_GUARD(s2n_digest_allow_md5_for_fips(&ws->p_hash.evp_hmac.evp_digest)); - } - POSIX_GUARD_OSSL(EVP_DigestSignInit(ws->p_hash.evp_hmac.evp_digest.ctx, NULL, ws->p_hash.evp_hmac.evp_digest.md, NULL, ws->p_hash.evp_hmac.ctx.evp_pkey), S2N_ERR_P_HASH_INIT_FAILED); diff --git a/tls/s2n_server_key_exchange.c b/tls/s2n_server_key_exchange.c index 0e710950270..bbea50fd63b 100644 --- a/tls/s2n_server_key_exchange.c +++ b/tls/s2n_server_key_exchange.c @@ -52,11 +52,6 @@ int s2n_server_key_recv(struct s2n_connection *conn) const struct s2n_signature_scheme *active_sig_scheme = conn->handshake_params.server_cert_sig_scheme; POSIX_ENSURE_REF(active_sig_scheme); - /* FIPS specifically allows MD5 for actual_protocol_version < S2N_TLS12) { - POSIX_GUARD(s2n_hash_allow_md5_for_fips(signature_hash)); - } - POSIX_GUARD(s2n_hash_init(signature_hash, active_sig_scheme->hash_alg)); POSIX_GUARD(s2n_hash_update(signature_hash, conn->handshake_params.client_random, S2N_TLS_RANDOM_DATA_LEN)); POSIX_GUARD(s2n_hash_update(signature_hash, conn->handshake_params.server_random, S2N_TLS_RANDOM_DATA_LEN)); @@ -267,11 +262,6 @@ int s2n_server_key_send(struct s2n_connection *conn) POSIX_GUARD(s2n_stuffer_write_uint16(out, sig_scheme->iana_value)); } - /* FIPS specifically allows MD5 for actual_protocol_version < S2N_TLS12) { - POSIX_GUARD(s2n_hash_allow_md5_for_fips(signature_hash)); - } - /* Add the random data to the hash */ POSIX_GUARD(s2n_hash_init(signature_hash, sig_scheme->hash_alg)); POSIX_GUARD(s2n_hash_update(signature_hash, conn->handshake_params.client_random, S2N_TLS_RANDOM_DATA_LEN));