Adds a proof harness for s2n_hmac_update (aws#2531)

* Adds a proof harness for s2n_hmac_update * Avoids unsigned-arithmetic overflow * Updates SAW and SideTrail proofs * Lexicographic order * Removes bounded_malloc from s2n_hmac_update proof * Prevent overflow using s2n_add_overflow Signed-off-by: Felipe R. Monteiro <[email protected]>
jakemas · Jan 29, 2021 · a1f92e6 · a1f92e6
1 parent 09d182e
commit a1f92e6
Show file tree

Hide file tree

Showing 6 changed files with 97 additions and 7 deletions.
diff --git a/crypto/s2n_hmac.c b/crypto/s2n_hmac.c
@@ -269,7 +269,7 @@ int s2n_hmac_update(struct s2n_hmac_state *state, const void *in, uint32_t size)
     const uint32_t HIGHEST_32_BIT = 4294949760;
     ENSURE_POSIX(size <= (UINT32_MAX - HIGHEST_32_BIT), S2N_ERR_INTEGER_OVERFLOW);
     uint32_t value = (HIGHEST_32_BIT + size) % state->hash_block_size;
-    state->currently_in_hash_block += value;
+    GUARD(s2n_add_overflow(state->currently_in_hash_block, value, &state->currently_in_hash_block));
     state->currently_in_hash_block %= state->hash_block_size;
 
     return s2n_hash_update(&state->inner, in, size);

diff --git a/tests/cbmc/proofs/s2n_hmac_update/Makefile b/tests/cbmc/proofs/s2n_hmac_update/Makefile
@@ -0,0 +1,46 @@
+# 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.
+
+# Expected runtime is less than a minute.
+
+CBMCFLAGS +=
+
+PROOF_UID = s2n_hmac_update
+HARNESS_ENTRY = $(PROOF_UID)_harness
+HARNESS_FILE = $(HARNESS_ENTRY).c
+
+PROOF_SOURCES += $(OPENSSL_SOURCE)/bn_override.c
+PROOF_SOURCES += $(OPENSSL_SOURCE)/ec_override.c
+PROOF_SOURCES += $(OPENSSL_SOURCE)/evp_override.c
+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_SOURCE)/proof_allocators.c
+PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
+PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
+
+PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hmac.c
+PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
+PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_evp.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
+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_hash_digest_size
+REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_digest
+
+UNWINDSET +=
+
+include ../Makefile.common
diff --git a/tests/cbmc/proofs/s2n_hmac_update/cbmc-batch.yaml b/tests/cbmc/proofs/s2n_hmac_update/cbmc-batch.yaml
@@ -0,0 +1,4 @@
+:
+  This file marks this directory as containing a CBMC proof. This file
+  is automatically clobbered in CI and replaced with parameters for
+  running the proof.
diff --git a/tests/cbmc/proofs/s2n_hmac_update/s2n_hmac_update_harness.c b/tests/cbmc/proofs/s2n_hmac_update/s2n_hmac_update_harness.c
@@ -0,0 +1,39 @@
+/*
+ * 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 "crypto/s2n_hmac.h"
+
+#include <cbmc_proof/make_common_datastructures.h>
+#include <cbmc_proof/proof_allocators.h>
+
+void s2n_hmac_update_harness()
+{
+    /* Non-deterministic inputs. */
+    struct s2n_hmac_state *state = cbmc_allocate_s2n_hmac_state();
+    uint32_t size;
+    void *in = malloc(size);
+
+    /* Assumptions. */
+    __CPROVER_assume(s2n_result_is_ok(s2n_hmac_state_validate(state)));
+    __CPROVER_file_local_s2n_hash_c_s2n_hash_set_impl(&state->inner);
+
+    /* Operation under verification. */
+    if (s2n_hmac_update(state, in, size) == S2N_SUCCESS)
+    {
+        /* Post-conditions. */
+        assert(s2n_result_is_ok(s2n_hmac_state_validate(state)));
+        assert(state->inner.hash_impl->update != NULL);
+    }
+}
diff --git a/tests/saw/HMAC/spec/HMAC.saw b/tests/saw/HMAC/spec/HMAC.saw
@@ -357,6 +357,7 @@ let hmac_update_spec
     let uint32_max = {{~0 : [32]}};
     let highest_32_bit = {{4294949760 : [32]}};
     crucible_precond {{ size <= uint32_max - highest_32_bit }};
+    crucible_precond {{ ((highest_32_bit + size) % (0 # st0.hash_block_size)) <= uint32_max - st0.currently_in_hash_block }};
 
     pmsg <- crucible_symbolic_alloc true 1 {{ (0 # size) : [64] }};
     msg <- crucible_fresh_cryptol_var "msg" {| ByteArray |};

diff --git a/tests/sidetrail/working/patches/hmac.patch b/tests/sidetrail/working/patches/hmac.patch
@@ -13,15 +13,15 @@ index 3405781..3beeacf 100644
 
  int s2n_hash_hmac_alg(s2n_hash_algorithm hash_alg, s2n_hmac_algorithm *out)
 @@ -268,7 +271,7 @@ int s2n_hmac_update(struct s2n_hmac_state *state, const void *in, uint32_t size)
+      */
      const uint32_t HIGHEST_32_BIT = 4294949760;
      ENSURE_POSIX(size <= (UINT32_MAX - HIGHEST_32_BIT), S2N_ERR_INTEGER_OVERFLOW);
-     uint32_t value = (HIGHEST_32_BIT + size) % state->hash_block_size;
--    state->currently_in_hash_block += value;
-+    state->currently_in_hash_block += (size) % state->hash_block_size;
+-    uint32_t value = (HIGHEST_32_BIT + size) % state->hash_block_size;
++    uint32_t value = (size) % state->hash_block_size;
+     GUARD(s2n_add_overflow(state->currently_in_hash_block, value, &state->currently_in_hash_block));
      state->currently_in_hash_block %= state->hash_block_size;
 
-     return s2n_hash_update(&state->inner, in, size);
-@@ -360,8 +363,8 @@ int s2n_hmac_copy(struct s2n_hmac_state *to, struct s2n_hmac_state *from)
+@@ -361,8 +364,8 @@ int s2n_hmac_copy(struct s2n_hmac_state *to, struct s2n_hmac_state *from)
      GUARD(s2n_hash_copy(&to->outer_just_key, &from->outer_just_key));
 
 
@@ -32,7 +32,7 @@ index 3405781..3beeacf 100644
      POSTCONDITION_POSIX(s2n_hmac_state_validate(to));
      POSTCONDITION_POSIX(s2n_hmac_state_validate(from));
      return S2N_SUCCESS;
-@@ -371,25 +374,25 @@ int s2n_hmac_copy(struct s2n_hmac_state *to, struct s2n_hmac_state *from)
+@@ -372,25 +375,25 @@ int s2n_hmac_copy(struct s2n_hmac_state *to, struct s2n_hmac_state *from)
  /* Preserve the handlers for hmac state pointers to avoid re-allocation
   * Only valid if the HMAC is in EVP mode
   */