diff --git a/cbmc/.gitignore b/cbmc/.gitignore new file mode 100644 index 000000000..5def9fe98 --- /dev/null +++ b/cbmc/.gitignore @@ -0,0 +1,19 @@ +# Emitted when running CBMC proofs +proofs/**/logs +proofs/**/gotos +proofs/**/report +proofs/**/html +proofs/output + +# Emitted by CBMC Viewer +TAGS-* + +# Emitted by litani +.ninja_deps +.ninja_log +.litani_cache_dir + +# These files should be overwritten whenever prepare.py runs +cbmc-batch.yaml + +__pycache__/ diff --git a/cbmc/include/README.md b/cbmc/include/README.md new file mode 100644 index 000000000..36bdd94e6 --- /dev/null +++ b/cbmc/include/README.md @@ -0,0 +1,6 @@ +CBMC proof include files +======================== + +This directory contains include files written for CBMC proof. It is +common to write some code to model aspects of the system under test, +and the header files for this code go here. diff --git a/cbmc/proofs/Makefile-project-defines b/cbmc/proofs/Makefile-project-defines new file mode 100644 index 000000000..a772c3898 --- /dev/null +++ b/cbmc/proofs/Makefile-project-defines @@ -0,0 +1,33 @@ +# -*- mode: makefile -*- +# The first line sets the emacs major mode to Makefile + +################################################################ +# Use this file to give project-specific definitions of the command +# line arguments to pass to CBMC tools like goto-cc to build the goto +# binaries and cbmc to do the property and coverage checking. +# +# Use this file to override most default definitions of variables in +# Makefile.common. +################################################################ + +# Flags to pass to goto-cc for compilation (typically those passed to gcc -c) +# COMPILE_FLAGS = + +# Flags to pass to goto-cc for linking (typically those passed to gcc) +# LINK_FLAGS = + +# Flag to pass to goto-cc to make all static symbols globally visible. Leave it +# unset or set it to --export-file-local-symbols to enable this behavior. Else, +# selectively enable access to such symbols via each proof's Makefile. +EXPORT_FILE_LOCAL_SYMBOLS = + +# Preprocessor include paths -I... +# Consider adding +# INCLUDES += -I$(CBMC_ROOT)/include +# You will want to decide what order that comes in relative to the other +# include directories in your project. +# +# INCLUDES = + +# Preprocessor definitions -D... +# DEFINES = diff --git a/cbmc/proofs/Makefile-project-targets b/cbmc/proofs/Makefile-project-targets new file mode 100644 index 000000000..bf681eed1 --- /dev/null +++ b/cbmc/proofs/Makefile-project-targets @@ -0,0 +1,7 @@ +# -*- mode: makefile -*- +# The first line sets the emacs major mode to Makefile + +################################################################ +# Use this file to give project-specific targets, including targets +# that may depend on targets defined in Makefile.common. +################################################################ diff --git a/cbmc/proofs/Makefile-project-testing b/cbmc/proofs/Makefile-project-testing new file mode 100644 index 000000000..03b9a0526 --- /dev/null +++ b/cbmc/proofs/Makefile-project-testing @@ -0,0 +1,8 @@ +# -*- mode: makefile -*- +# The first line sets the emacs major mode to Makefile + +################################################################ +# Use this file to define project-specific targets and definitions for +# unit testing or continuous integration that may depend on targets +# defined in Makefile.common +################################################################ diff --git a/cbmc/proofs/Makefile-template-defines b/cbmc/proofs/Makefile-template-defines new file mode 100644 index 000000000..73e8427a4 --- /dev/null +++ b/cbmc/proofs/Makefile-template-defines @@ -0,0 +1,20 @@ + +# Absolute path to the root of the source tree. +# +SRCDIR ?= $(abspath $(PROOF_ROOT)/../..) + + +# How to invoke litani. +# Use "litani" when litani is present in PATH. +# +LITANI ?= litani + + +# Name of this proof project, displayed in proof reports. For example, +# "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots, +# this may be overridden on the command-line to Make, for example +# +# make PROJECT_NAME="FreeRTOS MQTT" report +# +PROJECT_NAME = "mlkem-c-aarch64" + diff --git a/cbmc/proofs/Makefile.common b/cbmc/proofs/Makefile.common new file mode 100644 index 000000000..455b65139 --- /dev/null +++ b/cbmc/proofs/Makefile.common @@ -0,0 +1,1010 @@ +# -*- mode: makefile -*- +# The first line sets the emacs major mode to Makefile + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.10 + +################################################################ +# The CBMC Starter Kit depends on the files Makefile.common and +# run-cbmc-proofs.py. They are installed by the setup script +# cbmc-starter-kit-setup and updated to the latest version by the +# update script cbmc-starter-kit-update. For more information about +# the starter kit and these files and these scripts, see +# https://model-checking.github.io/cbmc-starter-kit +# +# Makefile.common implements what we consider to be some best +# practices for using cbmc for software verification. +# +# Section I gives default values for a large number of Makefile +# variables that control +# * how your code is built (include paths, etc), +# * what program transformations are applied to your code (loop +# unwinding, etc), and +# * what properties cbmc checks for in your code (memory safety, etc). +# +# These variables are defined below with definitions of the form +# VARIABLE ?= DEFAULT_VALUE +# meaning VARIABLE is set to DEFAULT_VALUE if VARIABLE has not already +# been given a value. +# +# For your project, you can override these default values with +# project-specific definitions in Makefile-project-defines. +# +# For any individual proof, you can override these default values and +# project-specific values with proof-specific definitions in the +# Makefile for your proof. +# +# The definitions in the proof Makefile override definitions in the +# project Makefile-project-defines which override definitions in this +# Makefile.common. +# +# Section II uses the values defined in Section I to build your code, run +# your proof, and build a report of your results. You should not need +# to modify or override anything in Section II, but you may want to +# read it to understand how the values defined in Section I control +# things. +# +# To use Makefile.common, set variables as described above as needed, +# and then for each proof, +# +# * Create a subdirectory . +# * Write a proof harness (a function) with the name +# in a file with the name /.c +# * Write a makefile with the name /Makefile that looks +# something like +# +# HARNESS_FILE= +# HARNESS_ENTRY= +# PROOF_UID= +# +# PROJECT_SOURCES += $(SRCDIR)/libraries/api_1.c +# PROJECT_SOURCES += $(SRCDIR)/libraries/api_2.c +# +# PROOF_SOURCES += $(PROOFDIR)/harness.c +# PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_a.c +# PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_b.c +# +# UNWINDSET += foo.0:3 +# UNWINDSET += bar.1:6 +# +# REMOVE_FUNCTION_BODY += api_stub_a +# REMOVE_FUNCTION_BODY += api_stub_b +# +# DEFINES = -DDEBUG=0 +# +# include ../Makefile.common +# +# * Change directory to and run make +# +# The proof setup script cbmc-starter-kit-setup-proof from the CBMC +# Starter Kit will do most of this for, creating a directory and +# writing a basic Makefile and proof harness into it that you can edit +# as described above. +# +# Warning: If you get results that are hard to explain, consider +# running "make clean" or "make veryclean" before "make" if you get +# results that are hard to explain. Dependency handling in this +# Makefile.common may not be perfect. + +SHELL=/bin/bash + +default: report + +################################################################ +################################################################ +## Section I: This section gives common variable definitions. +## +## Override these definitions in Makefile-project-defines or +## your proof Makefile. +## +## Remember that Makefile.common and Makefile-project-defines are +## included into the proof Makefile in your proof directory, so all +## relative pathnames defined there should be relative to your proof +## directory. + +################################################################ +# Define the layout of the source tree and the proof subtree +# +# Generally speaking, +# +# SRCDIR = the root of the repository +# CBMC_ROOT = /srcdir/cbmc +# PROOF_ROOT = /srcdir/cbmc/proofs +# PROOF_SOURCE = /srcdir/cbmc/sources +# PROOF_INCLUDE = /srcdir/cbmc/include +# PROOF_STUB = /srcdir/cbmc/stubs +# PROOFDIR = the directory containing the Makefile for your proof +# +# The path /srcdir/cbmc used in the example above is determined by the +# setup script cbmc-starter-kit-setup. Projects usually create a cbmc +# directory somewhere in the source tree, and run the setup script in +# that directory. The value of CBMC_ROOT becomes the absolute path to +# that directory. +# +# The location of that cbmc directory in the source tree affects the +# definition of SRCDIR, which is defined in terms of the relative path +# from a proof directory to the repository root. The definition is +# usually determined by the setup script cbmc-starter-kit-setup and +# written to Makefile-template-defines, but you can override it for a +# project in Makefile-project-defines and for a specific proof in the +# Makefile for the proof. + +# Absolute path to the directory containing this Makefile.common +# See https://ftp.gnu.org/old-gnu/Manuals/make-3.80/html_node/make_17.html +# +# Note: We compute the absolute paths to the makefiles in MAKEFILE_LIST +# before we filter the list of makefiles for %/Makefile.common. +# Otherwise an invocation of the form "make -f Makefile.common" will set +# MAKEFILE_LIST to "Makefile.common" which will fail to match the +# pattern %/Makefile.common. +# +MAKEFILE_PATHS = $(foreach makefile,$(MAKEFILE_LIST),$(abspath $(makefile))) +PROOF_ROOT = $(dir $(filter %/Makefile.common,$(MAKEFILE_PATHS))) + +CBMC_ROOT = $(shell dirname $(PROOF_ROOT)) +PROOF_SOURCE = $(CBMC_ROOT)/sources +PROOF_INCLUDE = $(CBMC_ROOT)/include +PROOF_STUB = $(CBMC_ROOT)/stubs + +# Project-specific definitions to override default definitions below +# * Makefile-project-defines will never be overwritten +# * Makefile-template-defines may be overwritten when the starter +# kit is updated +sinclude $(PROOF_ROOT)/Makefile-project-defines +sinclude $(PROOF_ROOT)/Makefile-template-defines + +# SRCDIR is the path to the root of the source tree +# This is a default definition that is frequently overridden in +# another Makefile, see the discussion of SRCDIR above. +SRCDIR ?= $(abspath ../..) + +# PROOFDIR is the path to the directory containing the proof harness +PROOFDIR ?= $(abspath .) + +################################################################ +# Define how to run CBMC + +# Do property checking with the external SAT solver given by +# EXTERNAL_SAT_SOLVER. Do coverage checking with the default solver, +# since coverage checking requires the use of an incremental solver. +# The EXTERNAL_SAT_SOLVER variable is typically set (if it is at all) +# as an environment variable or as a makefile variable in +# Makefile-project-defines. +# +# For a particular proof, if the default solver is faster, do property +# checking with the default solver by including this definition in the +# proof Makefile: +# USE_EXTERNAL_SAT_SOLVER = +# +ifneq ($(strip $(EXTERNAL_SAT_SOLVER)),) + USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver $(EXTERNAL_SAT_SOLVER) +endif +CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER) + +# Job pools +# For version of Litani that are new enough (where `litani print-capabilities` +# prints "pools"), proofs for which `EXPENSIVE = true` is set can be added to a +# "job pool" that restricts how many expensive proofs are run at a time. All +# other proofs will be built in parallel as usual. +# +# In more detail: all compilation, instrumentation, and report jobs are run with +# full parallelism as usual, even for expensive proofs. The CBMC jobs for +# non-expensive proofs are also run in parallel. The only difference is that the +# CBMC safety checks and coverage checks for expensive proofs are run with a +# restricted parallelism level. At any one time, only N of these jobs are run at +# once, amongst all the proofs. +# +# To configure N, Litani needs to be initialized with a pool called "expensive". +# For example, to only run two CBMC safety/coverage jobs at a time from amongst +# all the proofs, you would initialize litani like +# litani init --pools expensive:2 +# The run-cbmc-proofs.py script takes care of this initialization through the +# --expensive-jobs-parallelism flag. +# +# To enable this feature, set +# the ENABLE_POOLS variable when running Make, like +# `make ENABLE_POOLS=true report` +# The run-cbmc-proofs.py script takes care of this through the +# --restrict-expensive-jobs flag. + +ifeq ($(strip $(ENABLE_POOLS)),) + POOL = +else ifeq ($(strip $(EXPENSIVE)),) + POOL = +else + POOL = --pool expensive +endif + +# Similar to the pool feature above. If Litani is new enough, enable +# profiling CBMC's memory use. +ifeq ($(strip $(ENABLE_MEMORY_PROFILING)),) + MEMORY_PROFILING = +else + MEMORY_PROFILING = --profile-memory +endif + +# Property checking flags +# +# 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: +# +# CHECK_FLAG_POINTER_CHECK = +# +# would disable the --pointer-check 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_CONVERSION_CHECK ?= --conversion-check +CBMC_FLAG_DIV_BY_ZERO_CHECK ?= --div-by-zero-check +CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= --float-overflow-check +CBMC_FLAG_NAN_CHECK ?= --nan-check +CBMC_FLAG_POINTER_CHECK ?= --pointer-check +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_UNSIGNED_OVERFLOW_CHECK ?= --unsigned-overflow-check +CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions +CBMC_DEFAULT_UNWIND ?= --unwind 1 +CBMC_FLAG_FLUSH ?= --flush + +# CBMC flags used for property checking and coverage checking + +CBMCFLAGS += $(CBMC_FLAG_FLUSH) + +# CBMC flags used for property checking + +CHECKFLAGS += $(CBMC_FLAG_BOUNDS_CHECK) +CHECKFLAGS += $(CBMC_FLAG_CONVERSION_CHECK) +CHECKFLAGS += $(CBMC_FLAG_DIV_BY_ZERO_CHECK) +CHECKFLAGS += $(CBMC_FLAG_FLOAT_OVERFLOW_CHECK) +CHECKFLAGS += $(CBMC_FLAG_NAN_CHECK) +CHECKFLAGS += $(CBMC_FLAG_POINTER_CHECK) +CHECKFLAGS += $(CBMC_FLAG_POINTER_OVERFLOW_CHECK) +CHECKFLAGS += $(CBMC_FLAG_POINTER_PRIMITIVE_CHECK) +CHECKFLAGS += $(CBMC_FLAG_SIGNED_OVERFLOW_CHECK) +CHECKFLAGS += $(CBMC_FLAG_UNDEFINED_SHIFT_CHECK) +CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK) + +# Additional CBMC flag to CBMC control verbosity. +# +# Meaningful values are +# 0 none +# 1 only errors +# 2 + warnings +# 4 + results +# 6 + status/phase information +# 8 + statistical information +# 9 + progress information +# 10 + debug info +# +# Uncomment the following line or set in Makefile-project-defines +# CBMC_VERBOSITY ?= --verbosity 4 + +# Additional CBMC flag to control how CBMC treats static variables. +# +# NONDET_STATIC is a list of flags of the form --nondet-static +# and --nondet-static-exclude VAR. The --nondet-static flag causes +# CBMC to initialize static variables with unconstrained value +# (ignoring initializers and default zero-initialization). The +# --nondet-static-exclude VAR excludes VAR for the variables +# initialized with unconstrained values. +NONDET_STATIC ?= + +# Flags to pass to goto-cc for compilation and linking +COMPILE_FLAGS ?= -Wall +LINK_FLAGS ?= -Wall +EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols + +# During instrumentation, it adds models of C library functions +ADD_LIBRARY_FLAG := --add-library + +# Preprocessor include paths -I... +INCLUDES ?= +INCLUDES += -I$(PROOFDIR) +INCLUDES += -I$(SRCDIR)/mlkem +INCLUDES += -I$(SRCDIR)/fips202 + +# Preprocessor definitions -D... +DEFINES ?= + +# CBMC object model +# +# CBMC_OBJECT_BITS is the number of bits in a pointer CBMC uses for +# the id of the object to which a pointer is pointing. CBMC uses 8 +# bits for the object id by default. The remaining bits in the pointer +# are used for offset into the object. This limits the size of the +# objects that CBMC can model. This Makefile defines this bound on +# object size to be CBMC_MAX_OBJECT_SIZE. You are likely to get +# unexpected results if you try to malloc an object larger than this +# bound. +CBMC_OBJECT_BITS ?= 8 + +# CBMC loop unwinding (Normally set in the proof Makefile) +# +# UNWINDSET is a list of pairs of the form foo.1:4 meaning that +# CBMC should unwind loop 1 in function foo no more than 4 times. +# For historical reasons, the number 4 is one more than the number +# of times CBMC actually unwinds the loop. +UNWINDSET ?= + +# CBMC early loop unwinding (Normally set in the proof Makefile) +# +# Most users can ignore this variable. +# +# This variable exists to support the use of loop and function +# contracts, two features under development for CBMC. Checking the +# assigns clause for function contracts and loop invariants currently +# assumes loop-free bodies for loops and functions with contracts +# (possibly after replacing nested loops with their own loop +# contracts). To satisfy this requirement, it may be necessary to +# unwind some loops before the function contract and loop invariant +# transformations are applied to the goto program. This variable +# CPROVER_LIBRARY_UNWINDSET is identical to UNWINDSET, and we assume that the +# loops mentioned in CPROVER_LIBRARY_UNWINDSET and UNWINDSET are disjoint. +CPROVER_LIBRARY_UNWINDSET ?= + +# CBMC function removal (Normally set set in the proof Makefile) +# +# REMOVE_FUNCTION_BODY is a list of function names. CBMC will "undefine" +# the function, and CBMC will treat the function as having no side effects +# and returning an unconstrained value of the appropriate return type. +# The list should include the names of functions being stubbed out. +REMOVE_FUNCTION_BODY ?= + +# CBMC function pointer restriction (Normally set in the proof Makefile) +# +# RESTRICT_FUNCTION_POINTER is a list of function pointer restriction +# instructions of the form: +# +# .function_pointer_call./[,]* +# +# The function pointer call number in the specified function gets +# rewritten to a case switch over a finite list of functions. +# If some possible target functions are omitted from the list a counter +# example trace will be found by CBMC, i.e. the transformation is sound. +# If the target functions are file-local symbols, then mangled names must +# be used. +RESTRICT_FUNCTION_POINTER ?= + +# The project source files (Normally set set in the proof Makefile) +# +# PROJECT_SOURCES is the list of project source files to compile, +# including the source file defining the function under test. +PROJECT_SOURCES ?= + +# The proof source files (Normally set in the proof Makefile) +# +# PROOF_SOURCES is the list of proof source files to compile, including +# the proof harness, and including any function stubs being used. +PROOF_SOURCES ?= + +# The number of seconds that CBMC should be allowed to run for before +# being forcefully terminated. Currently, this is set to be less than +# the time limit for a CodeBuild job, which is eight hours. If a proof +# run takes longer than the time limit of the CI environment, the +# environment will halt the proof run without updating the Litani +# report, making the proof run appear to "hang". +CBMC_TIMEOUT ?= 21600 + +# CBMC string abstraction +# +# Replace all uses of char * by a struct that carries that string, +# and also the underlying allocation and the C string length. +STRING_ABSTRACTION ?= +ifdef STRING_ABSTRACTION + ifneq ($(strip $(STRING_ABSTRACTION)),) + CBMC_STRING_ABSTRACTION := --string-abstraction + endif +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) + +# Proof writers could add function contracts in their source code. +# These contracts are ignored by default, but may be enabled in two distinct +# contexts using the following two variables: +# 1. To check whether one or more function contracts are sound with respect to +# the function implementation, CHECK_FUNCTION_CONTRACTS should be a list of +# function names. Use CHECK_FUNCTION_CONTRACTS_REC to check contracts on +# recursive functions. +# 2. To replace calls to certain functions with their correspondent function +# contracts, USE_FUNCTION_CONTRACTS should be a list of function names. +# One must check separately whether a function contract is sound before +# replacing it in calling contexts. +CHECK_FUNCTION_CONTRACTS ?= +CBMC_CHECK_FUNCTION_CONTRACTS := $(patsubst %,--enforce-contract %, $(CHECK_FUNCTION_CONTRACTS)) + +CHECK_FUNCTION_CONTRACTS_REC ?= +CBMC_CHECK_FUNCTION_CONTRACTS_REC := $(patsubst %,--enforce-contract-rec %, $(CHECK_FUNCTION_CONTRACTS_REC)) + +USE_FUNCTION_CONTRACTS ?= +CBMC_USE_FUNCTION_CONTRACTS := $(patsubst %,--replace-call-with-contract %, $(USE_FUNCTION_CONTRACTS)) + +CODE_CONTRACTS := $(CHECK_FUNCTION_CONTRACTS)$(USE_FUNCTION_CONTRACTS)$(APPLY_LOOP_CONTRACTS) + +# Proof writers may also apply function contracts using the Dynamic Frame +# Condition Checking (DFCC) mode. For more information on DFCC, +# please see https://diffblue.github.io/cbmc/contracts-dev-spec-dfcc.html. +USE_DYNAMIC_FRAMES ?= +ifdef USE_DYNAMIC_FRAMES + ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) + CBMC_USE_DYNAMIC_FRAMES := $(CBMC_OPT_CONFIG_LIBRARY) --dfcc $(HARNESS_ENTRY) $(CBMC_CHECK_FUNCTION_CONTRACTS_REC) + endif +endif + +# Similarly, proof writers could also add loop contracts in their source code +# to obtain unbounded correctness proofs. Unlike function contracts, loop +# contracts are not reusable and thus are checked and used simultaneously. +# These contracts are also ignored by default, but may be enabled by setting +# the APPLY_LOOP_CONTRACTS variable. +APPLY_LOOP_CONTRACTS ?= +ifdef APPLY_LOOP_CONTRACTS + ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),) + CBMC_APPLY_LOOP_CONTRACTS := --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 +endif + +################################################################ +################################################################ +## Section II: This section defines the process of running a proof +## +## There should be no reason to edit anything below this line. + +################################################################ +# Paths + +CBMC ?= cbmc +GOTO_ANALYZER ?= goto-analyzer +GOTO_CC ?= goto-cc +GOTO_INSTRUMENT ?= goto-instrument +CRANGLER ?= crangler +VIEWER ?= cbmc-viewer +VIEWER2 ?= cbmc-viewer +CMAKE ?= cmake + +GOTODIR ?= $(PROOFDIR)/gotos +LOGDIR ?= $(PROOFDIR)/logs + +PROJECT ?= project +PROOF ?= proof + +HARNESS_GOTO ?= $(GOTODIR)/$(HARNESS_FILE) +PROJECT_GOTO ?= $(GOTODIR)/$(PROJECT) +PROOF_GOTO ?= $(GOTODIR)/$(PROOF) + +################################################################ +# Useful macros for values that are hard to reference +SPACE :=$() $() +COMMA :=, + +################################################################ +# Set C compiler defines + +CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS) +COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS) + +DEFINES += -DCBMC=1 +DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS) +DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))" + +ifndef KYBER_K + $(error KYBER_K not set) +endif + +DEFINES += -DKYBER_K=$(KYBER_K) + +# CI currently assumes cbmc invocation has at most one --unwindset + +# UNWINDSET is designed for user code (i.e., proof and project code) +ifdef UNWINDSET + ifneq ($(strip $(UNWINDSET)),) + CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET))) + endif +endif + +# CPROVER_LIBRARY_UNWINDSET is designed for CPROVER library functions +ifdef CPROVER_LIBRARY_UNWINDSET + ifneq ($(strip $(CPROVER_LIBRARY_UNWINDSET)),) + CBMC_CPROVER_LIBRARY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(CPROVER_LIBRARY_UNWINDSET))) + endif +endif + +CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY)) + +ifdef RESTRICT_FUNCTION_POINTER + ifneq ($(strip $(RESTRICT_FUNCTION_POINTER)),) + CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER)) + endif +endif + +################################################################ +# Targets for rewriting source files with crangler + +# Construct crangler configuration files +# +# REWRITTEN_SOURCES is a list of crangler output files source.i. +# This target assumes that for each source.i +# * source.i_SOURCE is the path to a source file, +# * source.i_FUNCTIONS is a list of functions (may be empty) +# * source.i_OBJECTS is a list of variables (may be empty) +# This target constructs the crangler configuration file source.i.json +# of the form +# { +# "sources": [ "/proj/code.c" ], +# "includes": [ "/proj/include" ], +# "defines": [ "VAR=1" ], +# "functions": [ {"function_name": ["remove static"]} ], +# "objects": [ {"variable_name": ["remove static"]} ], +# "output": "source.i" +# } +# to remove the static attribute from function_name and variable_name +# in the source file source.c and write the result to source.i. +# +# This target assumes that filenames include no spaces and that +# the INCLUDES and DEFINES variables include no spaces after -I +# and -D. For example, use "-DVAR=1" and not "-D VAR=1". +# +# Define *_SOURCE, *_FUNCTIONS, and *_OBJECTS in the proof Makefile. +# The string source.i is usually an absolute path $(PROOFDIR)/code.i +# to a file in the proof directory that contains the proof Makefile. +# The proof Makefile usually includes the definitions +# $(PROOFDIR)/code.i_SOURCE = /proj/code.c +# $(PROOFDIR)/code.i_FUNCTIONS = function_name +# $(PROOFDIR)/code.i_OBJECTS = variable_name +# Because these definitions refer to PROOFDIR that is defined in this +# Makefile.common, these definitions must appear after the inclusion +# of Makefile.common in the proof Makefile. +# +$(foreach rs,$(REWRITTEN_SOURCES),$(eval $(rs).json: $($(rs)_SOURCE))) +$(foreach rs,$(REWRITTEN_SOURCES),$(rs).json): + echo '{'\ + '"sources": ['\ + '"$($(@:.json=)_SOURCE)"'\ + '],'\ + '"includes": ['\ + '$(subst $(SPACE),$(COMMA),$(patsubst -I%,"%",$(strip $(INCLUDES))))' \ + '],'\ + '"defines": ['\ + '$(subst $(SPACE),$(COMMA),$(patsubst -D%,"%",$(subst ",\",$(strip $(DEFINES)))))' \ + '],'\ + '"functions": ['\ + '{'\ + '$(subst ~, ,$(subst $(SPACE),$(COMMA),$(patsubst %,"%":["remove~static"],$($(@:.json=)_FUNCTIONS))))' \ + '}'\ + '],'\ + '"objects": ['\ + '{'\ + '$(subst ~, ,$(subst $(SPACE),$(COMMA),$(patsubst %,"%":["remove~static"],$($(@:.json=)_OBJECTS))))' \ + '}'\ + '],'\ + '"output": "$(@:.json=)"'\ + '}' > $@ + +# Rewrite source files with crangler +# +$(foreach rs,$(REWRITTEN_SOURCES),$(eval $(rs): $(rs).json)) +$(REWRITTEN_SOURCES): + $(LITANI) add-job \ + --command \ + '$(CRANGLER) $@.json' \ + --inputs $($@_SOURCE) \ + --outputs $@ \ + --stdout-file $(LOGDIR)/crangler-$(subst /,_,$(subst .,_,$@))-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): removing static" + +################################################################ +# Build targets that make the relevant .goto files + +# Compile project 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 $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/project_sources-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): building project binary" + +# Compile 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 $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/proof_sources-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): building proof binary" + +# Remove function bodies from project sources +$(PROJECT_GOTO)0200.goto: $(PROJECT_GOTO)0100.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/remove_function_body-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): removing function bodies from project sources" + +# Link project and proof sources into the proof harness +$(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 $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/link_proof_project-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): linking project to proof" + +# Restrict function pointers +$(HARNESS_GOTO)0200.goto: $(HARNESS_GOTO)0100.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/restrict_function_pointer-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): restricting function pointers in project sources" + +# Fill static variable with unconstrained values +$(HARNESS_GOTO)0300.goto: $(HARNESS_GOTO)0200.goto +ifneq ($(strip $(CODE_CONTRACTS)),) + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/nondet_static-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not setting static variables to nondet (will do during contract instrumentation)" +else + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/nondet_static-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): setting static variables to nondet" +endif + +# Link CPROVER library if DFCC mode is on +$(HARNESS_GOTO)0400.goto: $(HARNESS_GOTO)0300.goto +ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(ADD_LIBRARY_FLAG) $(CBMC_OPT_CONFIG_LIBRARY) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/linking-library-models-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): linking CPROVER library" +else + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/linking-library-models-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not linking CPROVER library" +endif + +# Early unwind all loops on DFCC mode; otherwise, only unwind loops in proof and project code +$(HARNESS_GOTO)0500.goto: $(HARNESS_GOTO)0400.goto +ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/unwind_loops-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description $(UNWIND_0500_DESC) +else ifneq ($(strip $(CODE_CONTRACTS)),) + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/unwind_loops-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): unwinding loops in proof and project code" +else + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --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)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) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/check_function_contracts-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): checking function contracts" + +# Omit initialization of unused global variables (reduces problem size) +$(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/slice_global_inits-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): slicing global initializations" + +# Omit unused functions (sharpens coverage calculations) +$(HARNESS_GOTO)0800.goto: $(HARNESS_GOTO)0700.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): dropping unused functions" + +# Final name for proof harness +$(HARNESS_GOTO).goto: $(HARNESS_GOTO)0800.goto + $(LITANI) add-job \ + --command 'cp $< $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): copying final goto-binary" + +################################################################ +# Targets to run the analysis commands + +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_OPT_CONFIG_LIBRARY) + endif +endif + +$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto + $(LITANI) add-job \ + $(POOL) \ + --command \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \ + --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 \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --show-properties --xml-ui $<' \ + --inputs $^ \ + --outputs $@ \ + --ci-stage test \ + --stdout-file $@ \ + --ignore-returns 10 \ + --pipeline-name "$(PROOF_UID)" \ + --stderr-file $(LOGDIR)/property-err-log.txt \ + --description "$(PROOF_UID): printing safety properties" + +$(LOGDIR)/coverage.xml: $(HARNESS_GOTO).goto + $(LITANI) add-job \ + $(POOL) \ + --command \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(COVERFLAGS) --cover location --xml-ui $<' \ + --inputs $^ \ + --outputs $@ \ + --ci-stage test \ + --stdout-file $@ \ + $(MEMORY_PROFILING) \ + --ignore-returns 10 \ + --timeout $(CBMC_TIMEOUT) \ + --pipeline-name "$(PROOF_UID)" \ + --tags "stats-group:coverage computation" \ + --stderr-file $(LOGDIR)/coverage-err-log.txt \ + --description "$(PROOF_UID): calculating coverage" + +COVERAGE ?= $(LOGDIR)/coverage.xml +VIEWER_COVERAGE_FLAG ?= --coverage $(COVERAGE) + +$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(COVERAGE) + $(LITANI) add-job \ + --command " $(VIEWER) \ + --result $(LOGDIR)/result.xml \ + $(VIEWER_COVERAGE_FLAG) \ + --property $(LOGDIR)/property.xml \ + --srcdir $(SRCDIR) \ + --goto $(HARNESS_GOTO).goto \ + --reportdir $(PROOFDIR)/report \ + --config $(PROOFDIR)/cbmc-viewer.json" \ + --inputs $^ \ + --outputs $(PROOFDIR)/report \ + --pipeline-name "$(PROOF_UID)" \ + --stdout-file $(LOGDIR)/viewer-log.txt \ + --ci-stage report \ + --description "$(PROOF_UID): generating report" + +litani-path: + @echo $(LITANI) + +# ############################################################## +# Phony Rules +# +# These rules provide a convenient way to run a single proof up to a +# certain stage. Users can browse into a proof directory and run +# "make -Bj 3 report" to generate a report for just that proof, or +# "make goto" to build the goto binary. Under the hood, this runs litani +# for just that proof. + +_goto: $(HARNESS_GOTO).goto +goto: + @ echo Running 'litani init' + $(LITANI) init --project $(PROJECT_NAME) + @ echo Running 'litani add-job' + $(MAKE) -B _goto + @ echo Running 'litani build' + $(LITANI) run-build + +_result: $(LOGDIR)/result.txt +result: + @ echo Running 'litani init' + $(LITANI) init --project $(PROJECT_NAME) + @ echo Running 'litani add-job' + $(MAKE) -B _result + @ echo Running 'litani build' + $(LITANI) run-build + +_property: $(LOGDIR)/property.xml +property: + @ echo Running 'litani init' + $(LITANI) init --project $(PROJECT_NAME) + @ echo Running 'litani add-job' + $(MAKE) -B _property + @ echo Running 'litani build' + $(LITANI) run-build + +_coverage: $(LOGDIR)/coverage.xml +coverage: + @ echo Running 'litani init' + $(LITANI) init --project $(PROJECT_NAME) + @ echo Running 'litani add-job' + $(MAKE) -B _coverage + @ echo Running 'litani build' + $(LITANI) run-build + +_report: $(PROOFDIR)/report +report: + @ echo Running 'litani init' + $(LITANI) init --project $(PROJECT_NAME) + @ echo Running 'litani add-job' + $(MAKE) -B _report + @ echo Running 'litani build' + $(LITANI) run-build + +_report_no_coverage: + $(MAKE) COVERAGE="" VIEWER_COVERAGE_FLAG="" _report +report-no-coverage: + $(MAKE) COVERAGE="" VIEWER_COVERAGE_FLAG=" " report + +################################################################ +# Targets to clean up after ourselves +clean: + -$(RM) $(DEPENDENT_GOTOS) + -$(RM) TAGS* + -$(RM) *~ \#* + -$(RM) $(REWRITTEN_SOURCES) $(foreach rs,$(REWRITTEN_SOURCES),$(rs).json) + +veryclean: clean + -$(RM) -r report + -$(RM) -r $(LOGDIR) $(GOTODIR) + +.PHONY: \ + _coverage \ + _goto \ + _property \ + _report \ + _report_no_coverage \ + clean \ + coverage \ + goto \ + litani-path \ + property \ + report \ + report-no-coverage \ + result \ + setup_dependencies \ + testdeps \ + veryclean \ + # + +################################################################ + +# Run "make echo-proof-uid" to print the proof ID of a proof. This can be +# used by scripts to ensure that every proof has an ID, that there are +# no duplicates, etc. + +.PHONY: echo-proof-uid +echo-proof-uid: + @echo $(PROOF_UID) + +.PHONY: echo-project-name +echo-project-name: + @echo $(PROJECT_NAME) + +################################################################ + +# Project-specific targets requiring values defined above +sinclude $(PROOF_ROOT)/Makefile-project-targets + +# CI-specific targets to drive cbmc in CI +sinclude $(PROOF_ROOT)/Makefile-project-testing + +################################################################ diff --git a/cbmc/proofs/Makefile_params.common b/cbmc/proofs/Makefile_params.common new file mode 100644 index 000000000..40b339603 --- /dev/null +++ b/cbmc/proofs/Makefile_params.common @@ -0,0 +1,17 @@ +# SPDX-License-Identifier: Apache-2.0 + +ifndef KYBER_K + $(warning KYBER_K not set -- defaulting to KYBER_K=3) +endif + +KYBER_K ?= 3 + +ifeq ($(KYBER_K),2) + KYBER_NAMESPACE = pqcrystals_kyber512_ref_ +else ifeq ($(KYBER_K),3) + KYBER_NAMESPACE=pqcrystals_kyber768_ref_ +else ifeq ($(KYBER_K),4) + KYBER_NAMESPACE=pqcrystals_kyber1024_ref_ +else + $(error Invalid value of KYBER_K) +endif \ No newline at end of file diff --git a/cbmc/proofs/README.md b/cbmc/proofs/README.md new file mode 100644 index 000000000..de18841a9 --- /dev/null +++ b/cbmc/proofs/README.md @@ -0,0 +1,29 @@ +CBMC proofs +=========== + +# Overview + +This directory contains [CBMC](https://github.com/diffblue/cbmc) proofs for the absence +of certain classes of undefined behaviour for parts of the C-code in MLKEM-C-AArch64. + +Proofs are organized by functions, with the harnesses and proofs for each function +in a separate directory. + +TODO: Provide more information about CBMC and the properties it proves + +# Usage + +To run all proofs, print a summary at the end and reflect overall +success/failure in the error code, use + +``` +KYBER_K={2,3,4} run-cbmc-proofs.py --summarize +``` + +If `GITHUB_STEP_SUMMARY` is set, the proof summary will be appended to it. + +# Covered functions + +The following functions are currently covered: + +- `poly.c`: `poly_compress` diff --git a/cbmc/proofs/lib/__init__.py b/cbmc/proofs/lib/__init__.py new file mode 100644 index 000000000..e69de29bb diff --git a/cbmc/proofs/lib/print_tool_versions.py b/cbmc/proofs/lib/print_tool_versions.py new file mode 100755 index 000000000..bdeb429e3 --- /dev/null +++ b/cbmc/proofs/lib/print_tool_versions.py @@ -0,0 +1,74 @@ +#!/usr/bin/env python3 +# +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: MIT-0 + + +import logging +import pathlib +import shutil +import subprocess + + +_TOOLS = [ + "cadical", + "cbmc", + "cbmc-viewer", + "cbmc-starter-kit-update", + "kissat", + "litani", +] + + +def _format_versions(table): + lines = [ + "", + '', + ] + for tool, version in table.items(): + if version: + v_str = f'
{version}
' + else: + v_str = 'not found' + lines.append( + f'' + f'') + lines.append("
Tool Versions
{tool}:{v_str}
") + return "\n".join(lines) + + +def _get_tool_versions(): + ret = {} + for tool in _TOOLS: + err = f"Could not determine version of {tool}: " + ret[tool] = None + if not shutil.which(tool): + logging.error("%s'%s' not found on $PATH", err, tool) + continue + cmd = [tool, "--version"] + proc = subprocess.Popen(cmd, text=True, stdout=subprocess.PIPE) + try: + out, _ = proc.communicate(timeout=10) + except subprocess.TimeoutExpired: + logging.error("%s'%s --version' timed out", err, tool) + continue + if proc.returncode: + logging.error( + "%s'%s --version' returned %s", err, tool, str(proc.returncode)) + continue + ret[tool] = out.strip() + return ret + + +def main(): + exe_name = pathlib.Path(__file__).name + logging.basicConfig(format=f"{exe_name}: %(message)s") + + table = _get_tool_versions() + out = _format_versions(table) + print(out) + + +if __name__ == "__main__": + main() diff --git a/cbmc/proofs/lib/summarize.py b/cbmc/proofs/lib/summarize.py new file mode 100644 index 000000000..50dbcc33c --- /dev/null +++ b/cbmc/proofs/lib/summarize.py @@ -0,0 +1,143 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: MIT-0 + +import argparse +import json +import logging +import os +import sys + + +DESCRIPTION = """Print 2 tables in GitHub-flavored Markdown that summarize +an execution of CBMC proofs.""" + + +def get_args(): + """Parse arguments for summarize script.""" + parser = argparse.ArgumentParser(description=DESCRIPTION) + for arg in [{ + "flags": ["--run-file"], + "help": "path to the Litani run.json file", + "required": True, + }]: + flags = arg.pop("flags") + parser.add_argument(*flags, **arg) + return parser.parse_args() + + +def _get_max_length_per_column_list(data): + ret = [len(item) + 1 for item in data[0]] + for row in data[1:]: + for idx, item in enumerate(row): + ret[idx] = max(ret[idx], len(item) + 1) + return ret + + +def _get_table_header_separator(max_length_per_column_list): + line_sep = "" + for max_length_of_word_in_col in max_length_per_column_list: + line_sep += "|" + "-" * (max_length_of_word_in_col + 1) + line_sep += "|\n" + return line_sep + + +def _get_entries(max_length_per_column_list, row_data): + entries = [] + for row in row_data: + entry = "" + for idx, word in enumerate(row): + max_length_of_word_in_col = max_length_per_column_list[idx] + space_formatted_word = (max_length_of_word_in_col - len(word)) * " " + entry += "| " + word + space_formatted_word + entry += "|\n" + entries.append(entry) + return entries + + +def _get_rendered_table(data): + table = [] + max_length_per_column_list = _get_max_length_per_column_list(data) + entries = _get_entries(max_length_per_column_list, data) + for idx, entry in enumerate(entries): + if idx == 1: + line_sep = _get_table_header_separator(max_length_per_column_list) + table.append(line_sep) + table.append(entry) + table.append("\n") + return "".join(table) + + +def _get_status_and_proof_summaries(run_dict): + """Parse a dict representing a Litani run and create lists summarizing the + proof results. + + Parameters + ---------- + run_dict + A dictionary representing a Litani run. + + + Returns + ------- + A list of 2 lists. + The first sub-list maps a status to the number of proofs with that status. + The second sub-list maps each proof to its status. + """ + count_statuses = {} + proofs = [["Proof", "Status"]] + for proof_pipeline in run_dict["pipelines"]: + status_pretty_name = proof_pipeline["status"].title().replace("_", " ") + try: + count_statuses[status_pretty_name] += 1 + except KeyError: + count_statuses[status_pretty_name] = 1 + if proof_pipeline["name"] == "print_tool_versions": + continue + proofs.append([proof_pipeline["name"], status_pretty_name]) + statuses = [["Status", "Count"]] + for status, count in count_statuses.items(): + statuses.append([status, str(count)]) + return [statuses, proofs] + + +def print_proof_results(out_file): + """ + Print 2 strings that summarize the proof results. + When printing, each string will render as a GitHub flavored Markdown table. + """ + output = "## Summary of CBMC proof results\n\n" + with open(out_file, encoding='utf-8') as run_json: + run_dict = json.load(run_json) + status_table, proof_table = _get_status_and_proof_summaries(run_dict) + for summary in (status_table, proof_table): + output += _get_rendered_table(summary) + + print(output) + sys.stdout.flush() + + github_summary_file = os.getenv("GITHUB_STEP_SUMMARY") + if github_summary_file: + with open(github_summary_file, "a") as handle: + print(output, file=handle) + handle.flush() + else: + logging.warning( + "$GITHUB_STEP_SUMMARY not set, not writing summary file") + + msg = ( + "Click the 'Summary' button to view a Markdown table " + "summarizing all proof results") + if run_dict["status"] != "success": + logging.error("Not all proofs passed.") + logging.error(msg) + sys.exit(1) + logging.info(msg) + + +if __name__ == '__main__': + args = get_args() + logging.basicConfig(format="%(levelname)s: %(message)s") + try: + print_proof_results(args.run_file) + except Exception as ex: # pylint: disable=broad-except + logging.critical("Could not print results. Exception: %s", str(ex)) diff --git a/cbmc/proofs/poly_decompress/Makefile b/cbmc/proofs/poly_decompress/Makefile new file mode 100644 index 000000000..72367fdd8 --- /dev/null +++ b/cbmc/proofs/poly_decompress/Makefile @@ -0,0 +1,58 @@ +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_decompress_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_decompress + +DEFINES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c + +# For KYBER_K=2,3 a loop with 128 iterations is used. +# For KYBER_K=4, a nested loop with 32 and 8 iterations is used. +ifneq ($(KYBER_K),4) + UNWINDSET += $(KYBER_NAMESPACE)poly_decompress.0:129 +else + UNWINDSET += $(KYBER_NAMESPACE)poly_decompress.1:33 + UNWINDSET += $(KYBER_NAMESPACE)poly_decompress.0:9 +endif + +FUNCTION_NAME = $(KYBER_NAMESPACE)poly_decompress + +# TODO: I would like to comment this out to have CBMC validate the +# function contract as annotated in the source, rather than being forced +# to replicate it in the harness. But somehow this doesn't work...? + +# USE_FUNCTION_CONTRACTS = $(FUNCTION_NAME) + +# USE_DYNAMIC_FRAMES = 1 +# EXTERNAL_SAT_SOLVER = cadical +# CBMCFLAGS += --smt2 + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/cbmc/proofs/poly_decompress/README.md b/cbmc/proofs/poly_decompress/README.md new file mode 100644 index 000000000..e590d3e3c --- /dev/null +++ b/cbmc/proofs/poly_decompress/README.md @@ -0,0 +1,12 @@ +poly_decompress proof +============== + +This directory contains a memory safety proof for poly_decompress. + +To run the proof. +------------- +* Follow these [tool installation instructions](https://github.com/awslabs/aws-templates-for-cbmc-proofs/wiki/Installation) to install cbmc and cbmc-viewer. +* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer` + to your path. +* Run `make`. +* Open `report/html/index.html` in a web browser. diff --git a/cbmc/proofs/poly_decompress/cbmc-proof.txt b/cbmc/proofs/poly_decompress/cbmc-proof.txt new file mode 100644 index 000000000..6ed46f125 --- /dev/null +++ b/cbmc/proofs/poly_decompress/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/cbmc/proofs/poly_decompress/cbmc-viewer.json b/cbmc/proofs/poly_decompress/cbmc-viewer.json new file mode 100644 index 000000000..b73d0fd50 --- /dev/null +++ b/cbmc/proofs/poly_decompress/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "poly_decompress", + "proof-root": "cbmc/proofs" +} diff --git a/cbmc/proofs/poly_decompress/poly_decompress_harness.c b/cbmc/proofs/poly_decompress/poly_decompress_harness.c new file mode 100644 index 000000000..3fb6c4526 --- /dev/null +++ b/cbmc/proofs/poly_decompress/poly_decompress_harness.c @@ -0,0 +1,37 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +/* + * Insert copyright notice + */ + +/** + * @file poly_decompress_harness.c + * @brief Implements the proof harness for poly_decompress function. + */ + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ +#include "poly.h" + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) +{ + poly r; + uint8_t a[KYBER_POLYCOMPRESSEDBYTES]; + + poly_decompress(&r, a); + + // TODO: We're replicating the post-condition of the function contract of + // poly_decompress here. Ideally, we'd use CBMC's function contract mechanism + // here, but there are still issues. cf. a similar comment in the Makefile. + __CPROVER_assert(__CPROVER_forall { \ + unsigned i; (i < KYBER_N) ==> ( 0 <= r.coeffs[i] && r.coeffs[i] < KYBER_Q ) + }, "failed to prove post-condition for poly_decompress"); +} diff --git a/cbmc/proofs/run-cbmc-proofs.py b/cbmc/proofs/run-cbmc-proofs.py new file mode 100755 index 000000000..b10492cea --- /dev/null +++ b/cbmc/proofs/run-cbmc-proofs.py @@ -0,0 +1,438 @@ +#!/usr/bin/env python3 +# +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: MIT-0 + + +import argparse +import asyncio +import json +import logging +import math +import os +import pathlib +import re +import subprocess +import sys +import tempfile +import uuid + +from lib.summarize import print_proof_results + + +DESCRIPTION = "Configure and run all CBMC proofs in parallel" + +# Keep the epilog hard-wrapped at 70 characters, as it gets printed +# verbatim in the terminal. 70 characters stops here --------------> | +EPILOG = """ +This tool automates the process of running `make report` in each of +the CBMC proof directories. The tool calculates the dependency graph +of all tasks needed to build, run, and report on all the proofs, and +executes these tasks in parallel. + +The tool is roughly equivalent to doing this: + + litani init --project "my-cool-project"; + + find . -name cbmc-proof.txt | while read -r proof; do + pushd $(dirname ${proof}); + + # The `make _report` rule adds a single proof to litani + # without running it + make _report; + + popd; + done + + litani run-build; + +except that it is much faster and provides some convenience options. +The CBMC CI runs this script with no arguments to build and run all +proofs in parallel. The value of "my-cool-project" is taken from the +PROJECT_NAME variable in Makefile-project-defines. + +The --no-standalone argument omits the `litani init` and `litani +run-build`; use it when you want to add additional proof jobs, not +just the CBMC ones. In that case, you would run `litani init` +yourself; then run `run-cbmc-proofs --no-standalone`; add any +additional jobs that you want to execute with `litani add-job`; and +finally run `litani run-build`. + +The litani dashboard will be written under the `output` directory; the +cbmc-viewer reports remain in the `$PROOF_DIR/report` directory. The +HTML dashboard from the latest Litani run will always be symlinked to +`output/latest/html/index.html`, so you can keep that page open in +your browser and reload the page whenever you re-run this script. +""" +# 70 characters stops here ----------------------------------------> | + + +def get_project_name(): + cmd = [ + "make", + "--no-print-directory", + "-f", "Makefile.common", + "echo-project-name", + ] + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE, check=False) + if proc.returncode: + logging.critical("could not run make to determine project name") + sys.exit(1) + if not proc.stdout.strip(): + logging.warning( + "project name has not been set; using generic name instead. " + "Set the PROJECT_NAME value in Makefile-project-defines to " + "remove this warning") + return "" + return proc.stdout.strip() + + +def get_args(): + pars = argparse.ArgumentParser( + description=DESCRIPTION, epilog=EPILOG, + formatter_class=argparse.RawDescriptionHelpFormatter) + for arg in [{ + "flags": ["-j", "--parallel-jobs"], + "type": int, + "metavar": "N", + "help": "run at most N proof jobs in parallel", + }, { + "flags": ["--fail-on-proof-failure"], + "action": "store_true", + "help": "exit with return code `10' if any proof failed" + " (default: exit 0)", + }, { + "flags": ["--no-standalone"], + "action": "store_true", + "help": "only configure proofs: do not initialize nor run", + }, { + "flags": ["-p", "--proofs"], + "nargs": "+", + "metavar": "DIR", + "help": "only run proof in directory DIR (can pass more than one)", + }, { + "flags": ["--project-name"], + "metavar": "NAME", + "default": get_project_name(), + "help": "project name for report. Default: %(default)s", + }, { + "flags": ["--marker-file"], + "metavar": "FILE", + "default": "cbmc-proof.txt", + "help": ( + "name of file that marks proof directories. Default: " + "%(default)s"), + }, { + "flags": ["--no-memory-profile"], + "action": "store_true", + "help": "disable memory profiling, even if Litani supports it" + }, { + "flags": ["--no-expensive-limit"], + "action": "store_true", + "help": "do not limit parallelism of 'EXPENSIVE' jobs", + }, { + "flags": ["--expensive-jobs-parallelism"], + "metavar": "N", + "default": 1, + "type": int, + "help": ( + "how many proof jobs marked 'EXPENSIVE' to run in parallel. " + "Default: %(default)s"), + }, { + "flags": ["--verbose"], + "action": "store_true", + "help": "verbose output", + }, { + "flags": ["--debug"], + "action": "store_true", + "help": "debug output", + }, { + "flags": ["--summarize"], + "action": "store_true", + "help": "summarize proof results with two tables on stdout", + }, { + "flags": ["--version"], + "action": "version", + "version": "CBMC starter kit 2.10", + "help": "display version and exit" + }, { + "flags": ["--no-coverage"], + "action": "store_true", + "help": "do property checking without coverage checking" + }]: + flags = arg.pop("flags") + pars.add_argument(*flags, **arg) + return pars.parse_args() + + +def set_up_logging(verbose): + if verbose: + level = logging.DEBUG + else: + level = logging.WARNING + logging.basicConfig( + format="run-cbmc-proofs: %(message)s", level=level) + + +def task_pool_size(): + ret = os.cpu_count() + if ret is None or ret < 3: + return 1 + return ret - 2 + + +def print_counter(counter): + # pylint: disable=consider-using-f-string + print("\rConfiguring CBMC proofs: " + "{complete:{width}} / {total:{width}}".format(**counter), end="", file=sys.stderr) + + +def get_proof_dirs(proof_root, proof_list, marker_file): + if proof_list is not None: + proofs_remaining = list(proof_list) + else: + proofs_remaining = [] + + for root, _, fyles in os.walk(proof_root): + proof_name = str(pathlib.Path(root).name) + if root != str(proof_root) and ".litani_cache_dir" in fyles: + pathlib.Path(f"{root}/.litani_cache_dir").unlink() + if proof_list and proof_name not in proof_list: + continue + if proof_list and proof_name in proofs_remaining: + proofs_remaining.remove(proof_name) + if marker_file in fyles: + yield root + + if proofs_remaining: + logging.critical( + "The following proofs were not found: %s", + ", ".join(proofs_remaining)) + sys.exit(1) + + +def run_build(litani, jobs, fail_on_proof_failure, summarize): + cmd = [str(litani), "run-build"] + if jobs: + cmd.extend(["-j", str(jobs)]) + if fail_on_proof_failure: + cmd.append("--fail-on-pipeline-failure") + if summarize: + out_file = pathlib.Path(tempfile.gettempdir(), "run.json").resolve() + cmd.extend(["--out-file", str(out_file)]) + + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, check=False) + + if proc.returncode and not fail_on_proof_failure: + logging.critical("Failed to run litani run-build") + sys.exit(1) + + if summarize: + print_proof_results(out_file) + out_file.unlink() + + if proc.returncode: + logging.error("One or more proofs failed") + sys.exit(10) + +def get_litani_path(proof_root): + cmd = [ + "make", + "--no-print-directory", + f"PROOF_ROOT={proof_root}", + "-f", "Makefile.common", + "litani-path", + ] + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE, check=False) + if proc.returncode: + logging.critical("Could not determine path to litani") + sys.exit(1) + return proc.stdout.strip() + + +def get_litani_capabilities(litani_path): + cmd = [litani_path, "print-capabilities"] + proc = subprocess.run( + cmd, text=True, stdout=subprocess.PIPE, stderr=subprocess.DEVNULL, check=False) + if proc.returncode: + return [] + try: + return json.loads(proc.stdout) + except RuntimeError: + logging.warning("Could not load litani capabilities: '%s'", proc.stdout) + return [] + + +def check_uid_uniqueness(proof_dir, proof_uids): + with (pathlib.Path(proof_dir) / "Makefile").open() as handle: + for line in handle: + match = re.match(r"^PROOF_UID\s*=\s*(?P\w+)", line) + if not match: + continue + if match["uid"] not in proof_uids: + proof_uids[match["uid"]] = proof_dir + return + + logging.critical( + "The Makefile in directory '%s' should have a different " + "PROOF_UID than the Makefile in directory '%s'", + proof_dir, proof_uids[match["uid"]]) + sys.exit(1) + + logging.critical( + "The Makefile in directory '%s' should contain a line like", proof_dir) + logging.critical("PROOF_UID = ...") + logging.critical("with a unique identifier for the proof.") + sys.exit(1) + + +def should_enable_memory_profiling(litani_caps, args): + if args.no_memory_profile: + return False + return "memory_profile" in litani_caps + + +def should_enable_pools(litani_caps, args): + if args.no_expensive_limit: + return False + return "pools" in litani_caps + + +async def configure_proof_dirs( # pylint: disable=too-many-arguments + queue, counter, proof_uids, enable_pools, enable_memory_profiling, report_target, debug): + while True: + print_counter(counter) + path = str(await queue.get()) + + check_uid_uniqueness(path, proof_uids) + + pools = ["ENABLE_POOLS=true"] if enable_pools else [] + profiling = [ + "ENABLE_MEMORY_PROFILING=true"] if enable_memory_profiling else [] + + # Allow interactive tasks to preempt proof configuration + proc = await asyncio.create_subprocess_exec( + "nice", "-n", "15", "make", *pools, + *profiling, "-B", report_target, "" if debug else "--quiet", cwd=path, + stdout=asyncio.subprocess.PIPE, stderr=asyncio.subprocess.PIPE) + stdout, stderr = await proc.communicate() + logging.debug("returncode: %s", str(proc.returncode)) + logging.debug("stdout:") + for line in stdout.decode().splitlines(): + logging.debug(line) + logging.debug("stderr:") + for line in stderr.decode().splitlines(): + logging.debug(line) + + counter["fail" if proc.returncode else "pass"].append(path) + counter["complete"] += 1 + + print_counter(counter) + queue.task_done() + + +def add_tool_version_job(): + cmd = [ + "litani", "add-job", + "--command", "./lib/print_tool_versions.py .", + "--description", "printing out tool versions", + "--phony-outputs", str(uuid.uuid4()), + "--pipeline-name", "print_tool_versions", + "--ci-stage", "report", + "--tags", "front-page-text", + ] + proc = subprocess.run(cmd) + if proc.returncode: + logging.critical("Could not add tool version printing job") + sys.exit(1) + + +async def main(): # pylint: disable=too-many-locals + args = get_args() + set_up_logging(args.verbose) + + proof_root = pathlib.Path(os.getcwd()) + litani = get_litani_path(proof_root) + + litani_caps = get_litani_capabilities(litani) + enable_pools = should_enable_pools(litani_caps, args) + init_pools = [ + "--pools", f"expensive:{args.expensive_jobs_parallelism}" + ] if enable_pools else [] + + if not args.no_standalone: + cmd = [ + str(litani), "init", *init_pools, "--project", args.project_name, + "--no-print-out-dir", + ] + + if "output_directory_flags" in litani_caps: + out_prefix = proof_root / "output" + out_symlink = out_prefix / "latest" + out_index = out_symlink / "html" / "index.html" + cmd.extend([ + "--output-prefix", str(out_prefix), + "--output-symlink", str(out_symlink), + ]) + print( + "\nFor your convenience, the output of this run will be symbolically linked to ", + out_index, "\n") + + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, check=False) + if proc.returncode: + logging.critical("Failed to run litani init") + sys.exit(1) + + proof_dirs = list(get_proof_dirs( + proof_root, args.proofs, args.marker_file)) + if not proof_dirs: + logging.critical("No proof directories found") + sys.exit(1) + + proof_queue = asyncio.Queue() + for proof_dir in proof_dirs: + proof_queue.put_nowait(proof_dir) + + counter = { + "pass": [], + "fail": [], + "complete": 0, + "total": len(proof_dirs), + "width": int(math.log10(len(proof_dirs))) + 1 + } + + proof_uids = {} + tasks = [] + + enable_memory_profiling = should_enable_memory_profiling(litani_caps, args) + report_target = "_report_no_coverage" if args.no_coverage else "_report" + + for _ in range(task_pool_size()): + task = asyncio.create_task(configure_proof_dirs( + proof_queue, counter, proof_uids, enable_pools, + enable_memory_profiling, report_target, args.debug)) + tasks.append(task) + + await proof_queue.join() + + add_tool_version_job() + + print_counter(counter) + print("", file=sys.stderr) + + if counter["fail"]: + logging.critical( + "Failed to configure the following proofs:\n%s", "\n".join( + [str(f) for f in counter["fail"]])) + sys.exit(1) + + if not args.no_standalone: + run_build(litani, args.parallel_jobs, args.fail_on_proof_failure, args.summarize) + + +if __name__ == "__main__": + asyncio.run(main()) diff --git a/cbmc/sources/README.md b/cbmc/sources/README.md new file mode 100644 index 000000000..4f706b23d --- /dev/null +++ b/cbmc/sources/README.md @@ -0,0 +1,6 @@ +CBMC proof source code +====================== + +This directory contains source code written for CBMC proofs. It is +common to write some code to model aspects of the system under test, +and this code goes here. diff --git a/cbmc/stubs/README.md b/cbmc/stubs/README.md new file mode 100644 index 000000000..3b7823dd6 --- /dev/null +++ b/cbmc/stubs/README.md @@ -0,0 +1,6 @@ +CBMC proof stubs +====================== + +This directory contains the stubs written for CBMC proofs. It is +common to stub out functionality like network send and receive methods +when writing a CBMC proof, and the code for these stubs goes here. diff --git a/mlkem/poly.c b/mlkem/poly.c index a481397d0..c85a1faca 100644 --- a/mlkem/poly.c +++ b/mlkem/poly.c @@ -78,8 +78,22 @@ void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a) { * Arguments: - poly *r: pointer to output polynomial * - const uint8_t *a: pointer to input byte array * (of length KYBER_POLYCOMPRESSEDBYTES bytes) +* +* Upon return, the coefficients of the output polynomial are unsigned-canonical +* (non-negative and smaller than KYBER_Q). +* **************************************************/ -void poly_decompress(poly *r, const uint8_t a[KYBER_POLYCOMPRESSEDBYTES]) { +void poly_decompress(poly *r, const uint8_t a[KYBER_POLYCOMPRESSEDBYTES]) +/* ------ CBMC contract ------ */ +__CPROVER_requires(__CPROVER_is_fresh(r, sizeof(*r))) +__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(KYBER_POLYCOMPRESSEDBYTES))) +__CPROVER_ensures( \ + /* Output coefficients are unsigned canonical */ \ + __CPROVER_forall { \ + unsigned i; (i < KYBER_N) ==> ( 0 <= r->coeffs[i] && r->coeffs[i] < KYBER_Q ) + }) +/* --- End of CBMC contract --- */ +{ unsigned int i; #if (KYBER_POLYCOMPRESSEDBYTES == 128) @@ -92,18 +106,21 @@ void poly_decompress(poly *r, const uint8_t a[KYBER_POLYCOMPRESSEDBYTES]) { unsigned int j; uint8_t t[8]; for (i = 0; i < KYBER_N / 8; i++) { - t[0] = (a[0] >> 0); - t[1] = (a[0] >> 5) | (a[1] << 3); - t[2] = (a[1] >> 2); - t[3] = (a[1] >> 7) | (a[2] << 1); - t[4] = (a[2] >> 4) | (a[3] << 4); - t[5] = (a[3] >> 1); - t[6] = (a[3] >> 6) | (a[4] << 2); - t[7] = (a[4] >> 3); + // REF-CHANGE: Explicitly truncate to avoid warning about + // implicit truncation in CBMC. + t[0] = 0x1F & (a[0] >> 0); + t[1] = 0x1F & ((a[0] >> 5) | (a[1] << 3)); + t[2] = 0x1F & (a[1] >> 2); + t[3] = 0x1F & ((a[1] >> 7) | (a[2] << 1)); + t[4] = 0x1F & ((a[2] >> 4) | (a[3] << 4)); + t[5] = 0x1F & (a[3] >> 1); + t[6] = 0x1F & ((a[3] >> 6) | (a[4] << 2)); + t[7] = 0x1F & (a[4] >> 3); a += 5; for (j = 0; j < 8; j++) { - r->coeffs[8 * i + j] = ((uint32_t)(t[j] & 31) * KYBER_Q + 16) >> 5; + // REF-CHANGE: Truncation happened before + r->coeffs[8 * i + j] = ((uint32_t) t[j] * KYBER_Q + 16) >> 5; } } #else