update cbmc

Author: lrstewart

tests/cbmc/include/cbmc_proof/cbmc_utils.h

@@ -47,13 +47,8 @@ struct rc_keys_from_evp_pkey_ctx {
     int pkey_eckey_refs;
 };
 
-/**
- * In the `rc_keys_from_hash_state`, we store two `rc_keys_from_evp_pkey_ctx` objects:
- * one for the `evp` field and another for `evp_md5_secondary` field.
- */
 struct rc_keys_from_hash_state {
     struct rc_keys_from_evp_pkey_ctx evp;
-    struct rc_keys_from_evp_pkey_ctx evp_md5;
 };
 
 /**

tests/cbmc/proofs/s2n_hash_const_time_get_currently_in_hash_block/Makefile

@@ -22,7 +22,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
-PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
+PROOF_SOURCES += $(PROOF_STUB)/s2n_evp_signing_supported.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
 

tests/cbmc/proofs/s2n_hash_copy/Makefile

@@ -25,7 +25,7 @@ PROOF_SOURCES += $(OPENSSL_SOURCE)/ec_override.c
 PROOF_SOURCES += $(OPENSSL_SOURCE)/evp_override.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
-PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
+PROOF_SOURCES += $(PROOF_STUB)/s2n_evp_signing_supported.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c

tests/cbmc/proofs/s2n_hash_digest/Makefile

@@ -27,7 +27,7 @@ PROOF_SOURCES += $(OPENSSL_SOURCE)/md5_override.c
 PROOF_SOURCES += $(OPENSSL_SOURCE)/sha_override.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
-PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
+PROOF_SOURCES += $(PROOF_STUB)/s2n_evp_signing_supported.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c

tests/cbmc/proofs/s2n_hash_free/Makefile

@@ -24,7 +24,7 @@ PROOF_SOURCES += $(OPENSSL_SOURCE)/ec_override.c
 PROOF_SOURCES += $(OPENSSL_SOURCE)/evp_override.c
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
-PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
+PROOF_SOURCES += $(PROOF_STUB)/s2n_evp_signing_supported.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c

tests/cbmc/proofs/s2n_hash_free/s2n_hash_free_harness.c

@@ -13,7 +13,7 @@
  * permissions and limitations under the License.
  */
 
-#include "crypto/s2n_fips.h"
+#include "crypto/s2n_evp_signing.h"
 #include "crypto/s2n_hash.h"
 
 #include <cbmc_proof/make_common_datastructures.h>
@@ -35,9 +35,8 @@ 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()) {
+        if (s2n_evp_signing_supported()) {
             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);
@@ -47,11 +46,10 @@ void s2n_hash_free_harness()
 
     /* 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`,
+        /* 1. `free` leftover EVP_MD_CTX objects if `s2n_evp_signing_supported`,
               since `s2n_hash_free` is a NO-OP in that case. */
-        if (!s2n_is_in_fips_mode()) {
+        if (!s2n_evp_signing_supported()) {
             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),

tests/cbmc/proofs/s2n_hash_get_currently_in_hash_total/Makefile

@@ -22,7 +22,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
-PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
+PROOF_SOURCES += $(PROOF_STUB)/s2n_evp_signing_supported.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
 

tests/cbmc/proofs/s2n_hash_init/Makefile

@@ -24,7 +24,7 @@ PROOF_SOURCES += $(OPENSSL_SOURCE)/md5_override.c
 PROOF_SOURCES += $(OPENSSL_SOURCE)/sha_override.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
-PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
+PROOF_SOURCES += $(PROOF_STUB)/s2n_evp_signing_supported.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c

tests/cbmc/proofs/s2n_hash_new/Makefile

@@ -22,7 +22,7 @@ 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
+PROOF_SOURCES += $(PROOF_STUB)/s2n_evp_signing_supported.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c