From d9243976430b6e94babd0d38c8778d0c8facf40e Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 13 Aug 2024 14:09:02 +0100 Subject: [PATCH 1/7] Update Makefile.common from PR#4703 to work with unbounded proofs Signed-off-by: Rod Chapman --- tests/cbmc/proofs/Makefile.common | 112 ++++++++++++++++++++---------- 1 file changed, 76 insertions(+), 36 deletions(-) diff --git a/tests/cbmc/proofs/Makefile.common b/tests/cbmc/proofs/Makefile.common index f4faa231c26..a34de06200a 100644 --- a/tests/cbmc/proofs/Makefile.common +++ b/tests/cbmc/proofs/Makefile.common @@ -4,7 +4,7 @@ # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. # SPDX-License-Identifier: MIT-0 -CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.8.8 +CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.10+ ################################################################ # The CBMC Starter Kit depends on the files Makefile.common and @@ -211,10 +211,13 @@ CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER) ifeq ($(strip $(ENABLE_POOLS)),) POOL = + INIT_POOLS = else ifeq ($(strip $(EXPENSIVE)),) POOL = + INIT_POOLS = else POOL = --pool expensive + INIT_POOLS = --pools expensive:1 endif # Similar to the pool feature above. If Litani is new enough, enable @@ -229,29 +232,31 @@ endif # # Each variable below controls a specific property checking flag # within CBMC. If desired, a property flag can be disabled within -# a particular proof by nulling the corresponding variable. For -# instance, the following line: +# a particular proof by nulling the corresponding variable when CBMC's default +# is not to perform such checks, or setting to --no--check when CBMC's +# default is to perform such checks. For instance, the following lines: # -# CHECK_FLAG_POINTER_CHECK = +# CBMC_FLAG_POINTER_CHECK = --no-pointer-check +# CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK = # -# would disable the --pointer-check CBMC flag within: +# would disable pointer checks and unsigned overflow checks with CBMC flag +# within: # * an entire project when added to Makefile-project-defines # * a specific proof when added to the harness Makefile -CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail -CBMC_FLAG_MALLOC_FAIL_NULL ?= --malloc-fail-null -CBMC_FLAG_BOUNDS_CHECK ?= --bounds-check +CBMC_FLAG_MALLOC_MAY_FAIL ?= # set to --no-malloc-may-fail to disable +CBMC_FLAG_BOUNDS_CHECK ?= # set to --no-bounds-check to disable CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check -CBMC_FLAG_DIV_BY_ZERO_CHECK ?= --div-by-zero-check +CBMC_FLAG_DIV_BY_ZERO_CHECK ?= # set to --no-div-by-zero-check to disable CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= --float-overflow-check CBMC_FLAG_NAN_CHECK ?= --nan-check -CBMC_FLAG_POINTER_CHECK ?= --pointer-check +CBMC_FLAG_POINTER_CHECK ?= #set to --no-pointer-check to disable CBMC_FLAG_POINTER_OVERFLOW_CHECK ?= --pointer-overflow-check -CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= --pointer-primitive-check -CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= --signed-overflow-check -CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= --undefined-shift-check +CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= # set to --no-pointer-primitive-check to disable +CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= # set to --no-signed-overflow-check to disable +CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= # set to --no-undefined-shift-check to disable CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK ?= --unsigned-overflow-check -CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions +CBMC_FLAG_UNWINDING_ASSERTIONS ?= # set to --no-unwinding-assertions to disable CBMC_DEFAULT_UNWIND ?= --unwind 1 CBMC_FLAG_FLUSH ?= --flush @@ -410,7 +415,7 @@ endif # Optional configuration library flags OPT_CONFIG_LIBRARY ?= -CBMC_OPT_CONFIG_LIBRARY := $(CBMC_FLAG_MALLOC_MAY_FAIL) $(CBMC_FLAG_MALLOC_FAIL_NULL) $(CBMC_STRING_ABSTRACTION) +CBMC_OPT_CONFIG_LIBRARY := $(CBMC_FLAG_MALLOC_MAY_FAIL) $(CBMC_STRING_ABSTRACTION) # Proof writers could add function contracts in their source code. # These contracts are ignored by default, but may be enabled in two distinct @@ -456,6 +461,24 @@ ifdef APPLY_LOOP_CONTRACTS endif endif +# The default unwind should only be used in DFCC mode without loop contracts. +# When loop contracts are applied, we only unwind specified loops. +# If any loops remain after loop contracts have been applied, CBMC might try +# to unwind the program indefinetly, because we do not pass default unwind +# (i.e., --unwind 1) to CBMC when in DFCC mode. +# We must not use a default unwind command in DFCC mode, because contract instrumentation +# introduces loops encoding write set inclusion checks that must be dynamically unwound during +# symex. +ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) +ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),) + UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) + UNWIND_0500_DESC="$(PROOF_UID): unwinding specified subset of loops" +else + UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_FLAG_UNWINDING_ASSERTIONS) + UNWIND_0500_DESC="$(PROOF_UID): unwinding all loops" +endif +endif + # Silence makefile output (eg, long litani commands) unless VERBOSE is set. ifndef VERBOSE MAKEFLAGS := $(MAKEFLAGS) -s @@ -609,7 +632,7 @@ $(REWRITTEN_SOURCES): # Build targets that make the relevant .goto files # Compile project sources -$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES) +$(PROJECT_GOTO)0100.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES) $(LITANI) add-job \ --command \ '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \ @@ -621,7 +644,7 @@ $(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES) --description "$(PROOF_UID): building project binary" # Compile proof sources -$(PROOF_GOTO)1.goto: $(PROOF_SOURCES) +$(PROOF_GOTO)0100.goto: $(PROOF_SOURCES) $(LITANI) add-job \ --command \ '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \ @@ -633,7 +656,7 @@ $(PROOF_GOTO)1.goto: $(PROOF_SOURCES) --description "$(PROOF_UID): building proof binary" # Remove function bodies from project sources -$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto +$(PROJECT_GOTO)0200.goto: $(PROJECT_GOTO)0100.goto $(LITANI) add-job \ --command \ '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \ @@ -645,7 +668,7 @@ $(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto --description "$(PROOF_UID): removing function bodies from project sources" # Link project and proof sources into the proof harness -$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto +$(HARNESS_GOTO)0100.goto: $(PROOF_GOTO)0100.goto $(PROJECT_GOTO)0200.goto $(LITANI) add-job \ --command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ $(LINK_FLAGS) -o $@' \ --inputs $^ \ @@ -656,7 +679,7 @@ $(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto --description "$(PROOF_UID): linking project to proof" # Restrict function pointers -$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto +$(HARNESS_GOTO)0200.goto: $(HARNESS_GOTO)0100.goto $(LITANI) add-job \ --command \ '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \ @@ -668,7 +691,7 @@ $(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto --description "$(PROOF_UID): restricting function pointers in project sources" # Fill static variable with unconstrained values -$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto +$(HARNESS_GOTO)0300.goto: $(HARNESS_GOTO)0200.goto ifneq ($(strip $(CODE_CONTRACTS)),) $(LITANI) add-job \ --command 'cp $^ $@' \ @@ -691,7 +714,7 @@ else endif # Link CPROVER library if DFCC mode is on -$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto +$(HARNESS_GOTO)0400.goto: $(HARNESS_GOTO)0300.goto ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) $(LITANI) add-job \ --command \ @@ -714,17 +737,17 @@ else endif # Early unwind all loops on DFCC mode; otherwise, only unwind loops in proof and project code -$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto +$(HARNESS_GOTO)0500.goto: $(HARNESS_GOTO)0400.goto ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \ --inputs $^ \ --outputs $@ \ --stdout-file $(LOGDIR)/unwind_loops-log.txt \ --pipeline-name "$(PROOF_UID)" \ --ci-stage build \ - --description "$(PROOF_UID): unwinding all loops" + --description $(UNWIND_0500_DESC) else ifneq ($(strip $(CODE_CONTRACTS)),) $(LITANI) add-job \ --command \ @@ -740,14 +763,14 @@ else --command 'cp $^ $@' \ --inputs $^ \ --outputs $@ \ - --stdout-file $(LOGDIR)/linking-library-models-log.txt \ + --stdout-file $(LOGDIR)/unwind_loops-log.txt \ --pipeline-name "$(PROOF_UID)" \ --ci-stage build \ --description "$(PROOF_UID): not unwinding loops" endif # Replace function contracts, check function contracts, instrument for loop contracts -$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto +$(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto $(LITANI) add-job \ --command \ '$(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \ @@ -759,7 +782,7 @@ $(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto --description "$(PROOF_UID): checking function contracts" # Omit initialization of unused global variables (reduces problem size) -$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto +$(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto $(LITANI) add-job \ --command \ '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \ @@ -771,7 +794,7 @@ $(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto --description "$(PROOF_UID): slicing global initializations" # Omit unused functions (sharpens coverage calculations) -$(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto +$(HARNESS_GOTO)0800.goto: $(HARNESS_GOTO)0700.goto $(LITANI) add-job \ --command \ '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \ @@ -783,7 +806,7 @@ $(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto --description "$(PROOF_UID): dropping unused functions" # Final name for proof harness -$(HARNESS_GOTO).goto: $(HARNESS_GOTO)8.goto +$(HARNESS_GOTO).goto: $(HARNESS_GOTO)0800.goto $(LITANI) add-job \ --command 'cp $< $@' \ --inputs $^ \ @@ -799,7 +822,7 @@ ifdef CBMCFLAGS ifeq ($(strip $(CODE_CONTRACTS)),) CBMCFLAGS += $(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_OPT_CONFIG_LIBRARY) else ifeq ($(strip $(USE_DYNAMIC_FRAMES)),) - CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_OPT_CONFIG_LIBRARY) + CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_OPT_CONFIG_LIBRARY) endif endif @@ -820,6 +843,23 @@ $(LOGDIR)/result.xml: $(HARNESS_GOTO).goto --stderr-file $(LOGDIR)/result-err-log.txt \ --description "$(PROOF_UID): checking safety properties" +$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto + $(LITANI) add-job \ + $(POOL) \ + --command \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \ + --inputs $^ \ + --outputs $@ \ + --ci-stage test \ + --stdout-file $@ \ + $(MEMORY_PROFILING) \ + --ignore-returns 10 \ + --timeout $(CBMC_TIMEOUT) \ + --pipeline-name "$(PROOF_UID)" \ + --tags "stats-group:safety checks" \ + --stderr-file $(LOGDIR)/result-err-log.txt \ + --description "$(PROOF_UID): checking safety properties" + $(LOGDIR)/property.xml: $(HARNESS_GOTO).goto $(LITANI) add-job \ --command \ @@ -885,7 +925,7 @@ litani-path: _goto: $(HARNESS_GOTO).goto goto: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _goto @ echo Running 'litani build' @@ -894,7 +934,7 @@ goto: _result: $(LOGDIR)/result.txt result: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _result @ echo Running 'litani build' @@ -903,7 +943,7 @@ result: _property: $(LOGDIR)/property.xml property: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _property @ echo Running 'litani build' @@ -912,7 +952,7 @@ property: _coverage: $(LOGDIR)/coverage.xml coverage: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _coverage @ echo Running 'litani build' @@ -921,7 +961,7 @@ coverage: _report: $(PROOFDIR)/report report: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _report @ echo Running 'litani build' From 08adf1de29167053aa481cef1c79043ca34aa6bb Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 13 Aug 2024 14:31:59 +0100 Subject: [PATCH 2/7] Add CONTRACT_DECREASES macro for unbounded loop proofs. Signed-off-by: Rod Chapman --- utils/s2n_ensure.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/utils/s2n_ensure.h b/utils/s2n_ensure.h index 866db937db0..5404f6ed520 100644 --- a/utils/s2n_ensure.h +++ b/utils/s2n_ensure.h @@ -139,6 +139,7 @@ void *s2n_ensure_memmove_trace(void *to, const void *from, size_t size); #define CONTRACT_ASSIGNS(...) __CPROVER_assigns(__VA_ARGS__) #define CONTRACT_ASSIGNS_ERR(...) CONTRACT_ASSIGNS(__VA_ARGS__, _s2n_debug_info, s2n_errno) #define CONTRACT_ASSUME(...) __CPROVER_assume(__VA_ARGS__) + #define CONTRACT_DECREASES(...) __CPROVER_decreases(__VA_ARGS__) #define CONTRACT_REQUIRES(...) __CPROVER_requires(__VA_ARGS__) #define CONTRACT_ENSURES(...) __CPROVER_ensures(__VA_ARGS__) #define CONTRACT_INVARIANT(...) __CPROVER_loop_invariant(__VA_ARGS__) @@ -148,6 +149,7 @@ void *s2n_ensure_memmove_trace(void *to, const void *from, size_t size); #define CONTRACT_ASSIGNS(...) #define CONTRACT_ASSIGNS_ERR(...) #define CONTRACT_ASSUME(...) + #define CONTRACT_DECREASES(...) #define CONTRACT_REQUIRES(...) #define CONTRACT_ENSURES(...) #define CONTRACT_INVARIANT(...) From e45bc830e0ddbcfa7ffb2b4d22fc0e0dda37f515 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 13 Aug 2024 14:35:45 +0100 Subject: [PATCH 3/7] Add new partial and total versions of s2n_constant_time_equals and their proofs. Signed-off-by: Rod Chapman --- .../s2n_constant_time_equals_partial/Makefile | 42 +++++++++++++++++++ .../cbmc-proof.txt | 1 + ...s2n_constant_time_equals_partial_harness.c | 29 +++++++++++++ .../s2n_constant_time_equals_total/Makefile | 42 +++++++++++++++++++ .../cbmc-proof.txt | 1 + .../s2n_constant_time_equals_total_harness.c | 29 +++++++++++++ utils/s2n_safety.c | 39 +++++++++++++++++ utils/s2n_safety.h | 28 +++++++++++++ 8 files changed, 211 insertions(+) create mode 100644 tests/cbmc/proofs/s2n_constant_time_equals_partial/Makefile create mode 100644 tests/cbmc/proofs/s2n_constant_time_equals_partial/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_constant_time_equals_partial/s2n_constant_time_equals_partial_harness.c create mode 100644 tests/cbmc/proofs/s2n_constant_time_equals_total/Makefile create mode 100644 tests/cbmc/proofs/s2n_constant_time_equals_total/cbmc-proof.txt create mode 100644 tests/cbmc/proofs/s2n_constant_time_equals_total/s2n_constant_time_equals_total_harness.c diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_partial/Makefile b/tests/cbmc/proofs/s2n_constant_time_equals_partial/Makefile new file mode 100644 index 00000000000..70b5b7cbafc --- /dev/null +++ b/tests/cbmc/proofs/s2n_constant_time_equals_partial/Makefile @@ -0,0 +1,42 @@ +# +# +# 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. + + +# Use the default set of CBMC flags +CHECKFLAGS += + +PROOF_UID = s2n_constant_time_equals_partial +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(HARNESS_ENTRY).c + +# Uncomment and complete this if this function calls other functions that have pre- and post-conditions +#USE_FUNCTION_CONTRACTS = + +CHECK_FUNCTION_CONTRACTS=$(PROOF_UID) +FUNCTION_NAME = $(PROOF_UID) +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Use SMT back-end and disable default SAT backend +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) + +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c + +# Set Verbose=on to see what litani is actually running +VERBOSE=on + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_partial/cbmc-proof.txt b/tests/cbmc/proofs/s2n_constant_time_equals_partial/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_constant_time_equals_partial/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_partial/s2n_constant_time_equals_partial_harness.c b/tests/cbmc/proofs/s2n_constant_time_equals_partial/s2n_constant_time_equals_partial_harness.c new file mode 100644 index 00000000000..f53d7701d94 --- /dev/null +++ b/tests/cbmc/proofs/s2n_constant_time_equals_partial/s2n_constant_time_equals_partial_harness.c @@ -0,0 +1,29 @@ +/* + * 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 "utils/s2n_safety.h" + +void s2n_constant_time_equals_partial_harness() +{ + /* Non-deterministic inputs. */ + uint32_t len; + uint8_t *a; + uint8_t *b; + bool result; + + result = s2n_constant_time_equals_partial(a, b, len); +} diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_total/Makefile b/tests/cbmc/proofs/s2n_constant_time_equals_total/Makefile new file mode 100644 index 00000000000..d706866768a --- /dev/null +++ b/tests/cbmc/proofs/s2n_constant_time_equals_total/Makefile @@ -0,0 +1,42 @@ +# +# +# 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. + + +# Use the default set of CBMC flags +CHECKFLAGS += + +PROOF_UID = s2n_constant_time_equals_total +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(HARNESS_ENTRY).c + +# Uncomment and complete this if this function calls other functions that have pre- and post-conditions +USE_FUNCTION_CONTRACTS = s2n_constant_time_equals_partial + +CHECK_FUNCTION_CONTRACTS=$(PROOF_UID) +FUNCTION_NAME = $(PROOF_UID) +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Use SMT back-end and disable default SAT backend +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) + +PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c + +# Set Verbose=on to see what litani is actually running +VERBOSE=on + +include ../Makefile.common diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_total/cbmc-proof.txt b/tests/cbmc/proofs/s2n_constant_time_equals_total/cbmc-proof.txt new file mode 100644 index 00000000000..6ed46f1258c --- /dev/null +++ b/tests/cbmc/proofs/s2n_constant_time_equals_total/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_total/s2n_constant_time_equals_total_harness.c b/tests/cbmc/proofs/s2n_constant_time_equals_total/s2n_constant_time_equals_total_harness.c new file mode 100644 index 00000000000..59c022e2cd5 --- /dev/null +++ b/tests/cbmc/proofs/s2n_constant_time_equals_total/s2n_constant_time_equals_total_harness.c @@ -0,0 +1,29 @@ +/* + * 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 "utils/s2n_safety.h" + +void s2n_constant_time_equals_total_harness() +{ + /* Non-deterministic inputs. */ + uint32_t len; + uint8_t *a; + uint8_t *b; + bool result; + + result = s2n_constant_time_equals_total(a, b, len); +} diff --git a/utils/s2n_safety.c b/utils/s2n_safety.c index 6b2457b00bf..fe5b87d98c1 100644 --- a/utils/s2n_safety.c +++ b/utils/s2n_safety.c @@ -78,6 +78,45 @@ bool s2n_constant_time_equals(const uint8_t *a, const uint8_t *b, const uint32_t return (xor == 0); } +/* See specification of this function in s2n_safety.h */ +bool s2n_constant_time_equals_partial(const uint8_t *const a, + const uint8_t *const b, + const uint32_t len) +{ + bool arrays_equal = true; + /* iterate over each byte in the slices */ + for (uint32_t i = 0; i < len; i++) + CONTRACT_ASSIGNS(i, arrays_equal) + CONTRACT_INVARIANT(i <= len) + CONTRACT_INVARIANT(arrays_equal == + __CPROVER_forall { unsigned j; (j >= 0 && j < i) ==> (a[j] == b[j]) }) + CONTRACT_DECREASES(len - i) + { + arrays_equal = arrays_equal && (a[i] == b[i]); + } + + /* Substiture i = len into the loop invariant to get... */ + CONTRACT_ASSERT(arrays_equal == + __CPROVER_forall { unsigned j; (j >= 0 && j < len) ==> (a[j] == b[j]) }, + "Post-loop assertion"); + return arrays_equal; +} + + +/* See specification of this function in s2n_safety.h */ +bool s2n_constant_time_equals_total(const uint8_t *const a, + const uint8_t *const b, + const uint32_t len) +{ + if (a != NULL && b != NULL) { + return s2n_constant_time_equals_partial(a, b, len); + } else { + return false; + } +} + + + /** * Given arrays "dest" and "src" of length "len", conditionally copy "src" to "dest" * The execution time of this function is independent of the values diff --git a/utils/s2n_safety.h b/utils/s2n_safety.h index d0ac5f2fc1a..c1eb79acd7d 100644 --- a/utils/s2n_safety.h +++ b/utils/s2n_safety.h @@ -47,6 +47,34 @@ bool s2n_in_test(); /* Returns true if a and b are equal, in constant time */ bool s2n_constant_time_equals(const uint8_t* a, const uint8_t* b, const uint32_t len); +/* Returns true if a and b are equal. Execution time may depend on len */ +/* but not on the value of the data denoted by a or b */ +/* Note that if len == 0, then returns true */ +bool s2n_constant_time_equals_partial(const uint8_t* const a, + const uint8_t* const b, + const uint32_t len) +CONTRACT_REQUIRES(a != NULL && __CPROVER_is_fresh(a, len)) +CONTRACT_REQUIRES(b != NULL && __CPROVER_is_fresh(b, len)) +CONTRACT_ENSURES(CONTRACT_RETURN_VALUE == __CPROVER_forall { unsigned k; (k >= 0 && k < len) ==> (a[k] == b[k]) }); + + +/* If BOTH a and n are non-NULL then */ +/* Returns true if a and b are equal. Execution time may depend on len */ +/* but not on the value of the data denoted by a or b. If len == 0, */ +/* then returns true */ +/* */ +/* If either of a or b is NULL, then returns false */ +bool s2n_constant_time_equals_total(const uint8_t* const a, + const uint8_t* const b, + const uint32_t len) +CONTRACT_REQUIRES(__CPROVER_is_fresh(a, len)) +CONTRACT_REQUIRES(__CPROVER_is_fresh(b, len)) +CONTRACT_ENSURES(((a != NULL && b != NULL) && CONTRACT_RETURN_VALUE == s2n_constant_time_equals_partial(a, b, len) ) + || + ((a == NULL || b == NULL) && CONTRACT_RETURN_VALUE == false) + ); + + /* Copy src to dst, or don't copy it, in constant time */ int s2n_constant_time_copy_or_dont(uint8_t* dst, const uint8_t* src, uint32_t len, uint8_t dont); From 1633e5dbda2fda957108cd8a1ddae7401cf615f8 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Tue, 13 Aug 2024 14:57:29 +0100 Subject: [PATCH 4/7] Correct specification, contracts and code for case when len == 0 Signed-off-by: Rod Chapman --- utils/s2n_safety.c | 4 ++++ utils/s2n_safety.h | 20 ++++++++++++-------- 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/utils/s2n_safety.c b/utils/s2n_safety.c index fe5b87d98c1..e63bd524dd8 100644 --- a/utils/s2n_safety.c +++ b/utils/s2n_safety.c @@ -108,6 +108,10 @@ bool s2n_constant_time_equals_total(const uint8_t *const a, const uint8_t *const b, const uint32_t len) { + if (len == 0) { + return true; + } + if (a != NULL && b != NULL) { return s2n_constant_time_equals_partial(a, b, len); } else { diff --git a/utils/s2n_safety.h b/utils/s2n_safety.h index c1eb79acd7d..13980d12f07 100644 --- a/utils/s2n_safety.h +++ b/utils/s2n_safety.h @@ -58,20 +58,24 @@ CONTRACT_REQUIRES(b != NULL && __CPROVER_is_fresh(b, len)) CONTRACT_ENSURES(CONTRACT_RETURN_VALUE == __CPROVER_forall { unsigned k; (k >= 0 && k < len) ==> (a[k] == b[k]) }); -/* If BOTH a and n are non-NULL then */ -/* Returns true if a and b are equal. Execution time may depend on len */ -/* but not on the value of the data denoted by a or b. If len == 0, */ -/* then returns true */ -/* */ -/* If either of a or b is NULL, then returns false */ +/* If len == 0, then returns true, regardless of the values of a and b */ +/* */ +/* If len != 0 then */ +/* If BOTH a and n are non-NULL then */ +/* Returns true if a and b are equal. Execution time may depend on len */ +/* but not on the value of the data denoted by a or b. */ +/* */ +/* If either of a or b is NULL, then returns false */ bool s2n_constant_time_equals_total(const uint8_t* const a, const uint8_t* const b, const uint32_t len) CONTRACT_REQUIRES(__CPROVER_is_fresh(a, len)) CONTRACT_REQUIRES(__CPROVER_is_fresh(b, len)) -CONTRACT_ENSURES(((a != NULL && b != NULL) && CONTRACT_RETURN_VALUE == s2n_constant_time_equals_partial(a, b, len) ) +CONTRACT_ENSURES(((len == 0) && CONTRACT_RETURN_VALUE == true) || - ((a == NULL || b == NULL) && CONTRACT_RETURN_VALUE == false) + ((len != 0 && a != NULL && b != NULL) && CONTRACT_RETURN_VALUE == s2n_constant_time_equals_partial(a, b, len) ) + || + ((len != 0) && (a == NULL || b == NULL) && CONTRACT_RETURN_VALUE == false) ); From 976761d83bfcc13672994420ed28afe61f86a266 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Wed, 14 Aug 2024 10:12:44 +0100 Subject: [PATCH 5/7] Address review comments from colmmac: 1. Test and return early from s2n_constant_time_equals_total() when either a or b is NULL 2. Remove declaration of s2n_constant_time_equals_partial() from s2n_safety.h and make it "static" in the body of this translation unit. Update contracts accordingly. Signed-off-by: Rod Chapman --- .../s2n_constant_time_equals_partial/Makefile | 9 ++++--- ...s2n_constant_time_equals_partial_harness.c | 4 +++ utils/s2n_safety.c | 25 +++++++++++-------- utils/s2n_safety.h | 14 ++--------- 4 files changed, 27 insertions(+), 25 deletions(-) diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_partial/Makefile b/tests/cbmc/proofs/s2n_constant_time_equals_partial/Makefile index 70b5b7cbafc..923076301c7 100644 --- a/tests/cbmc/proofs/s2n_constant_time_equals_partial/Makefile +++ b/tests/cbmc/proofs/s2n_constant_time_equals_partial/Makefile @@ -31,12 +31,15 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla - PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) -PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c - # Set Verbose=on to see what litani is actually running VERBOSE=on + +#PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c +REWRITTEN_SOURCES = $(PROOFDIR)/s2n_safety.i include ../Makefile.common +$(PROOFDIR)/s2n_safety.i_SOURCE = $(SRCDIR)/utils/s2n_safety.c +$(PROOFDIR)/s2n_safety.i_FUNCTIONS = s2n_constant_time_equals_partial +$(PROOFDIR)/s2n_safety.i_OBJECTS = diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_partial/s2n_constant_time_equals_partial_harness.c b/tests/cbmc/proofs/s2n_constant_time_equals_partial/s2n_constant_time_equals_partial_harness.c index f53d7701d94..1cc44ce2466 100644 --- a/tests/cbmc/proofs/s2n_constant_time_equals_partial/s2n_constant_time_equals_partial_harness.c +++ b/tests/cbmc/proofs/s2n_constant_time_equals_partial/s2n_constant_time_equals_partial_harness.c @@ -17,6 +17,10 @@ #include "utils/s2n_safety.h" +bool s2n_constant_time_equals_partial(const uint8_t* const a, + const uint8_t* const b, + const uint32_t len); + void s2n_constant_time_equals_partial_harness() { /* Non-deterministic inputs. */ diff --git a/utils/s2n_safety.c b/utils/s2n_safety.c index e63bd524dd8..87abdd2f23c 100644 --- a/utils/s2n_safety.c +++ b/utils/s2n_safety.c @@ -78,10 +78,15 @@ bool s2n_constant_time_equals(const uint8_t *a, const uint8_t *b, const uint32_t return (xor == 0); } -/* See specification of this function in s2n_safety.h */ -bool s2n_constant_time_equals_partial(const uint8_t *const a, - const uint8_t *const b, - const uint32_t len) +/* Returns true if a and b are equal. Execution time may depend on len */ +/* but not on the value of the data denoted by a or b */ +/* Note that if len == 0, then returns true */ +static bool s2n_constant_time_equals_partial(const uint8_t* const a, + const uint8_t* const b, + const uint32_t len) +CONTRACT_REQUIRES(a != NULL && __CPROVER_is_fresh(a, len)) +CONTRACT_REQUIRES(b != NULL && __CPROVER_is_fresh(b, len)) +CONTRACT_ENSURES(CONTRACT_RETURN_VALUE == __CPROVER_forall { unsigned k; (k >= 0 && k < len) ==> (a[k] == b[k]) }) { bool arrays_equal = true; /* iterate over each byte in the slices */ @@ -89,7 +94,7 @@ bool s2n_constant_time_equals_partial(const uint8_t *const a, CONTRACT_ASSIGNS(i, arrays_equal) CONTRACT_INVARIANT(i <= len) CONTRACT_INVARIANT(arrays_equal == - __CPROVER_forall { unsigned j; (j >= 0 && j < i) ==> (a[j] == b[j]) }) + __CPROVER_forall { uint32_t j; (j >= 0 && j < i) ==> (a[j] == b[j]) }) CONTRACT_DECREASES(len - i) { arrays_equal = arrays_equal && (a[i] == b[i]); @@ -97,8 +102,8 @@ bool s2n_constant_time_equals_partial(const uint8_t *const a, /* Substiture i = len into the loop invariant to get... */ CONTRACT_ASSERT(arrays_equal == - __CPROVER_forall { unsigned j; (j >= 0 && j < len) ==> (a[j] == b[j]) }, - "Post-loop assertion"); + __CPROVER_forall { uint32_t j; (j >= 0 && j < len) ==> (a[j] == b[j]) }, + "Post-loop assertion"); return arrays_equal; } @@ -112,11 +117,11 @@ bool s2n_constant_time_equals_total(const uint8_t *const a, return true; } - if (a != NULL && b != NULL) { - return s2n_constant_time_equals_partial(a, b, len); - } else { + if (a == NULL || b == NULL) { return false; } + + return s2n_constant_time_equals_partial(a, b, len); } diff --git a/utils/s2n_safety.h b/utils/s2n_safety.h index 13980d12f07..d22c77b56c9 100644 --- a/utils/s2n_safety.h +++ b/utils/s2n_safety.h @@ -47,17 +47,6 @@ bool s2n_in_test(); /* Returns true if a and b are equal, in constant time */ bool s2n_constant_time_equals(const uint8_t* a, const uint8_t* b, const uint32_t len); -/* Returns true if a and b are equal. Execution time may depend on len */ -/* but not on the value of the data denoted by a or b */ -/* Note that if len == 0, then returns true */ -bool s2n_constant_time_equals_partial(const uint8_t* const a, - const uint8_t* const b, - const uint32_t len) -CONTRACT_REQUIRES(a != NULL && __CPROVER_is_fresh(a, len)) -CONTRACT_REQUIRES(b != NULL && __CPROVER_is_fresh(b, len)) -CONTRACT_ENSURES(CONTRACT_RETURN_VALUE == __CPROVER_forall { unsigned k; (k >= 0 && k < len) ==> (a[k] == b[k]) }); - - /* If len == 0, then returns true, regardless of the values of a and b */ /* */ /* If len != 0 then */ @@ -73,7 +62,8 @@ CONTRACT_REQUIRES(__CPROVER_is_fresh(a, len)) CONTRACT_REQUIRES(__CPROVER_is_fresh(b, len)) CONTRACT_ENSURES(((len == 0) && CONTRACT_RETURN_VALUE == true) || - ((len != 0 && a != NULL && b != NULL) && CONTRACT_RETURN_VALUE == s2n_constant_time_equals_partial(a, b, len) ) + ((len != 0 && a != NULL && b != NULL) && + CONTRACT_RETURN_VALUE == __CPROVER_forall { unsigned k; (k >= 0 && k < len) ==> (a[k] == b[k]) }) || ((len != 0) && (a == NULL || b == NULL) && CONTRACT_RETURN_VALUE == false) ); From 1b2dddc36e3e66091e04f076bf81a688ca1a5ae3 Mon Sep 17 00:00:00 2001 From: Rod Chapman Date: Wed, 14 Aug 2024 12:34:11 +0100 Subject: [PATCH 6/7] Tell goto-cc not to export file-local symbols to complete this proof Signed-off-by: Rod Chapman --- tests/cbmc/proofs/s2n_constant_time_equals_total/Makefile | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_total/Makefile b/tests/cbmc/proofs/s2n_constant_time_equals_total/Makefile index d706866768a..ef7006c952b 100644 --- a/tests/cbmc/proofs/s2n_constant_time_equals_total/Makefile +++ b/tests/cbmc/proofs/s2n_constant_time_equals_total/Makefile @@ -31,6 +31,8 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla +# Tell CBMC not to name-mangle and export file-local symbols +EXPORT_FILE_LOCAL_SYMBOLS= PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) From 0ed160a5e3847c73209a06cb18e44e0f5dca6c75 Mon Sep 17 00:00:00 2001 From: Roderick Chapman Date: Tue, 10 Sep 2024 12:15:41 +0100 Subject: [PATCH 7/7] Update utils/s2n_safety.c Correct typo in comment only. Co-authored-by: Sam Clark <3758302+goatgoose@users.noreply.github.com> --- utils/s2n_safety.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/utils/s2n_safety.c b/utils/s2n_safety.c index 87abdd2f23c..e07a4cf352c 100644 --- a/utils/s2n_safety.c +++ b/utils/s2n_safety.c @@ -100,7 +100,7 @@ CONTRACT_ENSURES(CONTRACT_RETURN_VALUE == __CPROVER_forall { unsigned k; (k >= 0 arrays_equal = arrays_equal && (a[i] == b[i]); } - /* Substiture i = len into the loop invariant to get... */ + /* Substitute i = len into the loop invariant to get... */ CONTRACT_ASSERT(arrays_equal == __CPROVER_forall { uint32_t j; (j >= 0 && j < len) ==> (a[j] == b[j]) }, "Post-loop assertion");