Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Unbounded proof and contracts for s2n_constant_time_equals #4704

Open
wants to merge 8 commits into
base: main
Choose a base branch
from
Open

Unbounded proof and contracts for s2n_constant_time_equals #4704

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
d924397
Update Makefile.common from PR#4703 to work with unbounded proofs
rod-chapman Aug 13, 2024
08adf1d
Add CONTRACT_DECREASES macro for unbounded loop proofs.
rod-chapman Aug 13, 2024
e45bc83
Add new partial and total versions of s2n_constant_time_equals and th…
rod-chapman Aug 13, 2024
1633e5d
Correct specification, contracts and code for case when len == 0
rod-chapman Aug 13, 2024
57910fa
Merge branch 'aws:main' into unbound_ct_equals
rod-chapman Aug 14, 2024
976761d
Address review comments from colmmac:
rod-chapman Aug 14, 2024
1b2dddc
Tell goto-cc not to export file-local symbols to complete this proof
rod-chapman Aug 14, 2024
0ed160a
Update utils/s2n_safety.c
rod-chapman Sep 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
112 changes: 76 additions & 36 deletions tests/cbmc/proofs/Makefile.common
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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>-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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 $@' \
Expand All @@ -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 $@' \
Expand All @@ -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) $^ $@' \
Expand All @@ -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 $^ \
Expand All @@ -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 $^ $@' \
Expand All @@ -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 $^ $@' \
Expand All @@ -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 \
Expand All @@ -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 \
Expand All @@ -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) $^ $@' \
Expand All @@ -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 $^ $@' \
Expand All @@ -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 $^ $@' \
Expand All @@ -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 $^ \
Expand All @@ -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

Expand All @@ -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 \
Expand Down Expand Up @@ -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'
Expand All @@ -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'
Expand All @@ -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'
Expand All @@ -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'
Expand All @@ -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'
Expand Down
42 changes: 42 additions & 0 deletions tests/cbmc/proofs/s2n_constant_time_equals_partial/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions tests/cbmc/proofs/s2n_constant_time_equals_partial/cbmc-proof.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
# This file marks this directory as containing a CBMC proof.
29 changes: 29 additions & 0 deletions ...s/cbmc/proofs/s2n_constant_time_equals_partial/s2n_constant_time_equals_partial_harness.c
View file
Open in desktop
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The CBMC results uploaded to the Github action summary indicates that this harness has 0% code coverage:
Screenshot 2024-09-09 at 14 59 34

Is there potentially an issue with this harness? The s2n_constant_time_equals_total harness looks okay. Is there maybe an issue with forward declaring s2n_constant_time_equals_partial() since it's static?

Original file line number Diff line number Diff line change
@@ -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 <assert.h>

#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);
}
Loading
Loading