Created draft proof for s2n_constant_time_equals (aws#2072)

* Created patrial proof for s2n_constant_time_equals

* Incorporated comments.

* Updated return type of s2n_constant_time_equals definitions.

* Added disambiguating parentheses.

* Incorporated additional comments.

tests/cbmc/proofs/s2n_safety_constant_time_equals/Makefile

@@ -0,0 +1,31 @@
+# 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 40 seconds.
+MAX_ARR_LEN = 10
+DEFINES += -DMAX_ARR_LEN=$(MAX_ARR_LEN)
+
+CBMCFLAGS +=
+
+HARNESS_ENTRY = s2n_safety_constant_time_equals_harness
+HARNESS_FILE = $(HARNESS_ENTRY).c
+
+PROOF_SOURCES += $(HARNESS_FILE)
+PROOF_SOURCES += $(PROOF_SOURCE)/proof_allocators.c
+
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
+
+UNWINDSET += s2n_constant_time_equals.0:$(call addone,$(MAX_ARR_LEN))
+
+include ../Makefile.common

tests/cbmc/proofs/s2n_safety_constant_time_equals/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.

tests/cbmc/proofs/s2n_safety_constant_time_equals/s2n_safety_constant_time_equals_harness.c

@@ -0,0 +1,42 @@
+/*
+ * 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 "api/s2n.h"
+#include "utils/s2n_safety.h"
+
+#include <sys/param.h>
+#include <assert.h>
+
+#include <cbmc_proof/proof_allocators.h>
+
+void s2n_safety_constant_time_equals_harness() {
+    /* Non-deterministic inputs. */
+    uint32_t len;
+    uint32_t alen;
+    uint32_t blen;
+    __CPROVER_assume(len < MAX_ARR_LEN);
+    __CPROVER_assume(alen >= len);
+    __CPROVER_assume(blen >= len);
+    uint8_t * a = can_fail_malloc(alen);
+    uint8_t * b = can_fail_malloc(blen);
+
+    /* Pre-conditions. */
+    __CPROVER_assume(S2N_IMPLIES(len != 0, a != NULL && b != NULL));
+
+    /* Check logical equivalence of s2n_constant_time_equals against element equality */
+    if(s2n_constant_time_equals(a, b, len)) {
+        assert(__CPROVER_forall {size_t i; (i >=0 && i < len) ==> (a[i] == b[i])});
+    }
+}

tests/fuzz/LD_PRELOAD/s2n_client_fuzz_test_overrides.c

@@ -39,7 +39,7 @@ int RSA_verify(int dtype, const unsigned char *m, unsigned int m_len,
     return 1;
 }
 
-int s2n_constant_time_equals(const uint8_t *a, const uint8_t *b, uint32_t len)
+bool s2n_constant_time_equals(const uint8_t *a, const uint8_t *b, uint32_t len)
 {
     /* Allow all signatures checked with s2n_constant_time_equals to always pass verification even if they are invalid
      * in order to aid code coverage with server fuzz test.

tests/fuzz/LD_PRELOAD/s2n_server_fuzz_test_overrides.c

@@ -39,7 +39,7 @@ int RSA_verify(int dtype, const unsigned char *m, unsigned int m_len,
     return 1;
 }
 
-int s2n_constant_time_equals(const uint8_t *a, const uint8_t *b, uint32_t len)
+bool s2n_constant_time_equals(const uint8_t *a, const uint8_t *b, uint32_t len)
 {
     /* Allow all signatures checked with s2n_constant_time_equals to always pass verification even if they are invalid
      * in order to aid code coverage with server fuzz test.

tests/sidetrail/working/patches/safety.patch

@@ -2,7 +2,7 @@
 +++ utils/s2n_safety.c	2018-02-09 10:28:30.000000000 -0500
 @@ -55,14 +65,12 @@
   */
- int s2n_constant_time_equals(const uint8_t * a, const uint8_t * b, uint32_t len)
+ bool s2n_constant_time_equals(const uint8_t * a, const uint8_t * b, uint32_t len)
  {
 -    S2N_PUBLIC_INPUT(a);
 -    S2N_PUBLIC_INPUT(b);

tests/sidetrail/working/s2n-cbc/patches/safety.patch

@@ -4,7 +4,7 @@ index 3af0262..261285a 100644
 +++ b/tests/sidetrail/working/s2n-cbc/utils/s2n_safety.c
 @@ -55,8 +55,8 @@ pid_t s2n_actual_getpid()
   */
- int s2n_constant_time_equals(const uint8_t * a, const uint8_t * b, uint32_t len)
+ bool s2n_constant_time_equals(const uint8_t * a, const uint8_t * b, uint32_t len)
  {
 -    S2N_PUBLIC_INPUT(a);
 -    S2N_PUBLIC_INPUT(b);

utils/s2n_safety.c

@@ -55,12 +55,14 @@ pid_t s2n_actual_getpid()
  * Returns:
  *  Whether all bytes in arrays "a" and "b" are identical
  */
-int s2n_constant_time_equals(const uint8_t * a, const uint8_t * b, uint32_t len)
+bool s2n_constant_time_equals(const uint8_t * a, const uint8_t * b, const uint32_t len)
 {
     S2N_PUBLIC_INPUT(a);
     S2N_PUBLIC_INPUT(b);
     S2N_PUBLIC_INPUT(len);
 
+    PRECONDITION_POSIX(len == 0 || (a != NULL && b != NULL));
+
     uint8_t xor = 0;
     for (int i = 0; i < len; i++) {
         /* Invariants must hold for each execution of the loop

utils/s2n_safety.h

@@ -307,7 +307,7 @@ int s2n_in_unit_test_set(bool newval);
 extern pid_t s2n_actual_getpid();
 
 /* Returns 1 if a and b are equal, in constant time */
-extern int s2n_constant_time_equals(const uint8_t * a, const uint8_t * b, uint32_t len);
+extern bool s2n_constant_time_equals(const uint8_t * a, const uint8_t * b, const uint32_t len);
 
 /* Copy src to dst, or don't copy it, in constant time */
 extern int s2n_constant_time_copy_or_dont(uint8_t * dst, const uint8_t * src, uint32_t len, uint8_t dont);