Incorporated comments.

Author: Christopher Wagner

tests/cbmc/proofs/s2n_safety_constant_time_equals/Makefile

@@ -11,22 +11,26 @@
 # implied. See the License for the specific language governing permissions and
 # limitations under the License.
 
-# Expected runtime is 60 seconds.
 
-CBMCFLAGS +=
+# Expected runtime is 40 seconds.
 MAX_ARR_LEN = 10
 DEFINES += -DMAX_ARR_LEN=$(MAX_ARR_LEN)
 
-DEPENDENCIES += $(HELPERDIR)/source/cbmc_utils.c
-DEPENDENCIES += $(HELPERDIR)/source/make_common_datastructures.c
-DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
-DEPENDENCIES += $(SRCDIR)/stuffer/s2n_stuffer.c
-DEPENDENCIES += $(SRCDIR)/utils/s2n_blob.c
-DEPENDENCIES += $(SRCDIR)/utils/s2n_ensure.c
-DEPENDENCIES += $(SRCDIR)/utils/s2n_mem.c
-DEPENDENCIES += $(SRCDIR)/utils/s2n_safety.c
+CBMCFLAGS +=
+
+HARNESS_ENTRY = s2n_safety_constant_time_equals_harness
+HARNESS_FILE = $(HARNESS_ENTRY).c
+
+PROOF_SOURCES += $(HARNESS_FILE)
+PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
+PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_SOURCE)/proof_allocators.c
 
-ENTRY = s2n_safety_constant_time_equals_harness
+PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 # We abstract these functions because manual inspection demonstrates they are unreachable.
 REMOVE_FUNCTION_BODY += --remove-function-body s2n_blob_slice

tests/cbmc/proofs/s2n_safety_constant_time_equals/s2n_safety_constant_time_equals_harness.c

@@ -14,14 +14,12 @@
  */
 
 #include "api/s2n.h"
-#include "stuffer/s2n_stuffer.h"
 #include "utils/s2n_safety.h"
 
 #include <sys/param.h>
 #include <assert.h>
 
 #include <cbmc_proof/cbmc_utils.h>
-#include <cbmc_proof/make_common_datastructures.h>
 #include <cbmc_proof/proof_allocators.h>
 
 void s2n_safety_constant_time_equals_harness() {
@@ -40,10 +38,7 @@ void s2n_safety_constant_time_equals_harness() {
     __CPROVER_assume(S2N_IMPLIES(len != 0, a != NULL && b != NULL));
 
     /* Check logical equivalence of s2n_constant_time_equals against element equality */
-    bool result = s2n_constant_time_equals(a, b, len);
-    if(result) {
+    if(s2n_constant_time_equals(a, b, len)) {
         assert(__CPROVER_forall {size_t i; (i >=0 && i < len) ==> (a[i] == b[i])});
-    }/* else { 
-        assert(__CPROVER_exists {size_t i; (i >= 0 && i < len) && (a[i] != b[i])}));
-    }*/
+    }
 }

utils/s2n_safety.c

@@ -55,12 +55,14 @@ pid_t s2n_actual_getpid()
  * Returns:
  *  Whether all bytes in arrays "a" and "b" are identical
  */
-bool 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 bool 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);