diff --git a/regression/contracts/s2n_record_writev/LICENSE b/regression/contracts/s2n_record_writev/LICENSE new file mode 100644 index 00000000000..4583997a69e --- /dev/null +++ b/regression/contracts/s2n_record_writev/LICENSE @@ -0,0 +1,224 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License 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. + + +============================================================================ + S2N SUBCOMPONENTS: + + The s2n Project contains subcomponents with seperate copyright notices + and license terms. Your use of the source code for these subcomponents is + subject to the terms and conditions of the following licenses. + + +======================================================================== +Third party MIT licenses +======================================================================== + +The following components are provided under the MIT License. See project link for details. + + + SIKE + -> s2n/pq-crypto/sike_r1/LICENSE.txt + + + diff --git a/regression/contracts/s2n_record_writev/Makefile b/regression/contracts/s2n_record_writev/Makefile new file mode 100644 index 00000000000..03b869043a7 --- /dev/null +++ b/regression/contracts/s2n_record_writev/Makefile @@ -0,0 +1,23 @@ +PROJECT_NAME = "s2n" + +CHECKFLAGS += --pointer-primitive-check + + +LITANI ?= litani + +PROOFDIR ?= $(abspath .) + + +CBMC_OBJECT_BITS = 9 +PROOF_UID = s2n_record_writev +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(PROOF_UID).c + +CHECK_FUNCTION_CONTRACTS += s2n_record_writev +USE_FUNCTION_CONTRACTS += s2n_hmac_update + +PROJECT_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) + + +include Makefile.common diff --git a/regression/contracts/s2n_record_writev/Makefile.common b/regression/contracts/s2n_record_writev/Makefile.common new file mode 100644 index 00000000000..b6dd5401486 --- /dev/null +++ b/regression/contracts/s2n_record_writev/Makefile.common @@ -0,0 +1,985 @@ +# -*- 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 + +CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.5 + +################################################################ +# 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_FLAG_UNWIND ?= --unwind 1 +CBMC_FLAG_FLUSH ?= --flush + +# CBMC flags used for property checking and coverage checking + +CBMCFLAGS += $(CBMC_FLAG_UNWIND) $(CBMC_UNWINDSET) $(CBMC_FLAG_FLUSH) + +# CBMC flags used for property checking + +CHECKFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL) +CHECKFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL) +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) +CHECKFLAGS += $(CBMC_FLAG_UNWINDING_ASSERTIONS) + +# CBMC flags used for coverage checking + +COVERFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL) +COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL) + +# 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 + +# Preprocessor include paths -I... +INCLUDES ?= + +# 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 +# EARLY_UNWINDSET is identical to UNWINDSET, and we assume that the +# loops mentioned in EARLY_UNWINDSET and UNWINDSET are disjoint. +EARLY_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 + +# 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. +# 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)) + +USE_FUNCTION_CONTRACTS ?= +CBMC_USE_FUNCTION_CONTRACTS := $(patsubst %,--replace-call-with-contract %, $(USE_FUNCTION_CONTRACTS)) + +# 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 to 1. +APPLY_LOOP_CONTRACTS ?= 0 +ifeq ($(APPLY_LOOP_CONTRACTS),1) + CBMC_APPLY_LOOP_CONTRACTS ?= --apply-loop-contracts +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 +MAKE_SOURCE ?= make-source +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))" + +# CI currently assumes cbmc invocation has at most one --unwindset +ifdef UNWINDSET + ifneq ($(strip $(UNWINDSET)),"") + CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET))) + endif +endif +ifdef EARLY_UNWINDSET + ifneq ($(strip $(EARLY_UNWINDSET)),"") + CBMC_EARLY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(EARLY_UNWINDSET))) + endif +endif + +CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY)) +CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER)) + +################################################################ +# 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)1.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)1.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)2.goto: $(PROJECT_GOTO)1.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)1.goto: $(PROOF_GOTO)1.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)2.goto: $(HARNESS_GOTO)1.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) $^ $@' \ + --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)3.goto: $(HARNESS_GOTO)2.goto + $(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" + +# # Omit unused functions (sharpens coverage calculations) +# $(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.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" + +# Omit initialization of unused global variables (reduces problem size) +$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)3.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" + +# Unwind loops for loop and function contracts +$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)5.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_EARLY_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" + +# Apply loop contracts +$(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/apply_loop_contracts-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): applying loop contracts" + +# Check function contracts +$(HARNESS_GOTO)9.goto: $(HARNESS_GOTO)8.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --dfcc $(HARNESS_ENTRY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/check_function_contracts-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): checking function contracts" + +# Final name for proof harness +$(HARNESS_GOTO).goto: $(HARNESS_GOTO)9.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 + +$(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)/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" + +define VIEWER_CMD + $(VIEWER) \ + --result $(LOGDIR)/result.txt \ + --block $(LOGDIR)/coverage.xml \ + --property $(LOGDIR)/property.xml \ + --srcdir $(SRCDIR) \ + --goto $(HARNESS_GOTO).goto \ + --htmldir $(PROOFDIR)/html +endef +export VIEWER_CMD + +$(PROOFDIR)/html: $(LOGDIR)/result.txt $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml + $(LITANI) add-job \ + --command "$$VIEWER_CMD" \ + --inputs $^ \ + --outputs $(PROOFDIR)/html \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage report \ + --stdout-file $(LOGDIR)/viewer-log.txt \ + --description "$(PROOF_UID): generating report" + + +# Caution: run make-source before running property and coverage checking +# The current make-source script removes the goto binary +$(LOGDIR)/source.json: + mkdir -p $(dir $@) + $(RM) -r $(GOTODIR) + $(MAKE_SOURCE) --srcdir $(SRCDIR) --wkdir $(PROOFDIR) > $@ + $(RM) -r $(GOTODIR) + +define VIEWER2_CMD + $(VIEWER2) \ + --result $(LOGDIR)/result.xml \ + --coverage $(LOGDIR)/coverage.xml \ + --property $(LOGDIR)/property.xml \ + --srcdir $(SRCDIR) \ + --goto $(HARNESS_GOTO).goto \ + --reportdir $(PROOFDIR)/report \ + --config $(PROOFDIR)/cbmc-viewer.json +endef +export VIEWER2_CMD + +# Omit logs/source.json from report generation until make-sources +# works correctly with Makefiles that invoke the compiler with +# mutliple source files at once. +$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml + $(LITANI) add-job \ + --command "$$VIEWER2_CMD" \ + --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 + +# Choose the invocation of cbmc-viewer depending on which version of +# cbmc-viewer is installed. The --version flag is not implemented in +# version 1 --- it is an "unrecognized argument" --- but it is +# implemented in version 2. +_report1: $(PROOFDIR)/html +_report2: $(PROOFDIR)/report +_report: + (cbmc-viewer --version 2>&1 | grep "unrecognized argument" > /dev/null) && \ + $(MAKE) -B _report1 || $(MAKE) -B _report2 + +report report1 report2: + @ echo Running 'litani init' + $(LITANI) init --project $(PROJECT_NAME) + @ echo Running 'litani add-job' + $(MAKE) -B _report + @ echo Running 'litani build' + $(LITANI) run-build + +################################################################ +# 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 html report + -$(RM) -r $(LOGDIR) $(GOTODIR) + +.PHONY: \ + _coverage \ + _goto \ + _property \ + _report \ + _report2 \ + _result \ + clean \ + coverage \ + goto \ + litani-path \ + property \ + report \ + report2 \ + result \ + setup_dependencies \ + testdeps \ + veryclean \ + # + +################################################################ + +# Rule for generating cbmc-batch.yaml, used by the CI at +# https://github.com/awslabs/aws-batch-cbmc/ + +JOB_OS ?= ubuntu16 +JOB_MEMORY ?= 32000 + +# Proofs that are expected to fail should set EXPECTED to +# "FAILED" in their Makefile. Values other than SUCCESSFUL +# or FAILED will cause a CI error. +EXPECTED ?= SUCCESSFUL + +define yaml_encode_options + "$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')" +endef + +CI_FLAGS = $(CBMCFLAGS) $(CHECKFLAGS) $(COVERFLAGS) + +cbmc-batch.yaml: + @$(RM) $@ + @echo 'build_memory: $(JOB_MEMORY)' > $@ + @echo 'cbmcflags: $(strip $(call yaml_encode_options,$(CI_FLAGS)))' >> $@ + @echo 'coverage_memory: $(JOB_MEMORY)' >> $@ + @echo 'expected: $(EXPECTED)' >> $@ + @echo 'goto: $(HARNESS_GOTO).goto' >> $@ + @echo 'jobos: $(JOB_OS)' >> $@ + @echo 'property_memory: $(JOB_MEMORY)' >> $@ + @echo 'report_memory: $(JOB_MEMORY)' >> $@ + +.PHONY: cbmc-batch.yaml + +################################################################ + +# 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/regression/contracts/s2n_record_writev/NOTICE b/regression/contracts/s2n_record_writev/NOTICE new file mode 100644 index 00000000000..f8bbcc301b5 --- /dev/null +++ b/regression/contracts/s2n_record_writev/NOTICE @@ -0,0 +1,2 @@ +s2n +Copyright 2014-2015 Amazon.com, Inc. or its affiliates. All Rights Reserved. diff --git a/regression/contracts/s2n_record_writev/README b/regression/contracts/s2n_record_writev/README new file mode 100644 index 00000000000..dec999563e9 --- /dev/null +++ b/regression/contracts/s2n_record_writev/README @@ -0,0 +1,9 @@ +This directory contains an example of a problem encountered when +applying function contracts in the context of AWS s2n-tls. Run the +example by using the command: + +make veryclean && make result + +This creates a large problem during symbolic execution and solving. + +This test is currently not included in the any regression. \ No newline at end of file diff --git a/regression/contracts/s2n_record_writev/minimized/LICENSE b/regression/contracts/s2n_record_writev/minimized/LICENSE new file mode 100644 index 00000000000..4583997a69e --- /dev/null +++ b/regression/contracts/s2n_record_writev/minimized/LICENSE @@ -0,0 +1,224 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License 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. + + +============================================================================ + S2N SUBCOMPONENTS: + + The s2n Project contains subcomponents with seperate copyright notices + and license terms. Your use of the source code for these subcomponents is + subject to the terms and conditions of the following licenses. + + +======================================================================== +Third party MIT licenses +======================================================================== + +The following components are provided under the MIT License. See project link for details. + + + SIKE + -> s2n/pq-crypto/sike_r1/LICENSE.txt + + + diff --git a/regression/contracts/s2n_record_writev/minimized/Makefile b/regression/contracts/s2n_record_writev/minimized/Makefile new file mode 100644 index 00000000000..991ec9a5f05 --- /dev/null +++ b/regression/contracts/s2n_record_writev/minimized/Makefile @@ -0,0 +1,23 @@ +PROJECT_NAME = "s2n" + +CHECKFLAGS += --pointer-primitive-check + + +LITANI ?= litani + +PROOFDIR ?= $(abspath .) + + +CBMC_OBJECT_BITS = 9 +PROOF_UID = s2n_record_writev +HARNESS_ENTRY = $(PROOF_UID)_harness +HARNESS_FILE = $(PROOF_UID).c + +# CHECK_FUNCTION_CONTRACTS += s2n_record_writev +# USE_FUNCTION_CONTRACTS += s2n_hmac_update + +PROJECT_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE) + + +include Makefile.common diff --git a/regression/contracts/s2n_record_writev/minimized/Makefile.common b/regression/contracts/s2n_record_writev/minimized/Makefile.common new file mode 100644 index 00000000000..a6ef6994ce5 --- /dev/null +++ b/regression/contracts/s2n_record_writev/minimized/Makefile.common @@ -0,0 +1,985 @@ +# -*- 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 + +CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.5 + +################################################################ +# 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_FLAG_UNWIND ?= --unwind 1 +CBMC_FLAG_FLUSH ?= --flush + +# CBMC flags used for property checking and coverage checking + +CBMCFLAGS += $(CBMC_FLAG_UNWIND) $(CBMC_UNWINDSET) $(CBMC_FLAG_FLUSH) + +# CBMC flags used for property checking + +CHECKFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL) +CHECKFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL) +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) +CHECKFLAGS += $(CBMC_FLAG_UNWINDING_ASSERTIONS) + +# CBMC flags used for coverage checking + +COVERFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL) +COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL) + +# 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 + +# Preprocessor include paths -I... +INCLUDES ?= + +# 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 +# EARLY_UNWINDSET is identical to UNWINDSET, and we assume that the +# loops mentioned in EARLY_UNWINDSET and UNWINDSET are disjoint. +EARLY_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 + +# 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. +# 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)) + +USE_FUNCTION_CONTRACTS ?= +CBMC_USE_FUNCTION_CONTRACTS := $(patsubst %,--replace-call-with-contract %, $(USE_FUNCTION_CONTRACTS)) + +# 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 to 1. +APPLY_LOOP_CONTRACTS ?= 0 +ifeq ($(APPLY_LOOP_CONTRACTS),1) + CBMC_APPLY_LOOP_CONTRACTS ?= --apply-loop-contracts +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 +MAKE_SOURCE ?= make-source +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))" + +# CI currently assumes cbmc invocation has at most one --unwindset +ifdef UNWINDSET + ifneq ($(strip $(UNWINDSET)),"") + CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET))) + endif +endif +ifdef EARLY_UNWINDSET + ifneq ($(strip $(EARLY_UNWINDSET)),"") + CBMC_EARLY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(EARLY_UNWINDSET))) + endif +endif + +CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY)) +CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER)) + +################################################################ +# 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)1.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)1.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)2.goto: $(PROJECT_GOTO)1.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)1.goto: $(PROOF_GOTO)1.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)2.goto: $(HARNESS_GOTO)1.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) $^ $@' \ + --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)3.goto: $(HARNESS_GOTO)2.goto + $(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" + +# # Omit unused functions (sharpens coverage calculations) +# $(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.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" + +# Omit initialization of unused global variables (reduces problem size) +$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)3.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" + +# Unwind loops for loop and function contracts +$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)5.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_EARLY_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" + +# Apply loop contracts +$(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/apply_loop_contracts-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): applying loop contracts" + +# # Check function contracts +# $(HARNESS_GOTO)9.goto: $(HARNESS_GOTO)8.goto +# $(LITANI) add-job \ +# --command \ +# '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --dfcc $(HARNESS_ENTRY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \ +# --inputs $^ \ +# --outputs $@ \ +# --stdout-file $(LOGDIR)/check_function_contracts-log.txt \ +# --pipeline-name "$(PROOF_UID)" \ +# --ci-stage build \ +# --description "$(PROOF_UID): checking function contracts" + +# Final name for proof harness +$(HARNESS_GOTO).goto: $(HARNESS_GOTO)8.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 + +$(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)/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" + +define VIEWER_CMD + $(VIEWER) \ + --result $(LOGDIR)/result.txt \ + --block $(LOGDIR)/coverage.xml \ + --property $(LOGDIR)/property.xml \ + --srcdir $(SRCDIR) \ + --goto $(HARNESS_GOTO).goto \ + --htmldir $(PROOFDIR)/html +endef +export VIEWER_CMD + +$(PROOFDIR)/html: $(LOGDIR)/result.txt $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml + $(LITANI) add-job \ + --command "$$VIEWER_CMD" \ + --inputs $^ \ + --outputs $(PROOFDIR)/html \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage report \ + --stdout-file $(LOGDIR)/viewer-log.txt \ + --description "$(PROOF_UID): generating report" + + +# Caution: run make-source before running property and coverage checking +# The current make-source script removes the goto binary +$(LOGDIR)/source.json: + mkdir -p $(dir $@) + $(RM) -r $(GOTODIR) + $(MAKE_SOURCE) --srcdir $(SRCDIR) --wkdir $(PROOFDIR) > $@ + $(RM) -r $(GOTODIR) + +define VIEWER2_CMD + $(VIEWER2) \ + --result $(LOGDIR)/result.xml \ + --coverage $(LOGDIR)/coverage.xml \ + --property $(LOGDIR)/property.xml \ + --srcdir $(SRCDIR) \ + --goto $(HARNESS_GOTO).goto \ + --reportdir $(PROOFDIR)/report \ + --config $(PROOFDIR)/cbmc-viewer.json +endef +export VIEWER2_CMD + +# Omit logs/source.json from report generation until make-sources +# works correctly with Makefiles that invoke the compiler with +# mutliple source files at once. +$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml + $(LITANI) add-job \ + --command "$$VIEWER2_CMD" \ + --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 + +# Choose the invocation of cbmc-viewer depending on which version of +# cbmc-viewer is installed. The --version flag is not implemented in +# version 1 --- it is an "unrecognized argument" --- but it is +# implemented in version 2. +_report1: $(PROOFDIR)/html +_report2: $(PROOFDIR)/report +_report: + (cbmc-viewer --version 2>&1 | grep "unrecognized argument" > /dev/null) && \ + $(MAKE) -B _report1 || $(MAKE) -B _report2 + +report report1 report2: + @ echo Running 'litani init' + $(LITANI) init --project $(PROJECT_NAME) + @ echo Running 'litani add-job' + $(MAKE) -B _report + @ echo Running 'litani build' + $(LITANI) run-build + +################################################################ +# 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 html report + -$(RM) -r $(LOGDIR) $(GOTODIR) + +.PHONY: \ + _coverage \ + _goto \ + _property \ + _report \ + _report2 \ + _result \ + clean \ + coverage \ + goto \ + litani-path \ + property \ + report \ + report2 \ + result \ + setup_dependencies \ + testdeps \ + veryclean \ + # + +################################################################ + +# Rule for generating cbmc-batch.yaml, used by the CI at +# https://github.com/awslabs/aws-batch-cbmc/ + +JOB_OS ?= ubuntu16 +JOB_MEMORY ?= 32000 + +# Proofs that are expected to fail should set EXPECTED to +# "FAILED" in their Makefile. Values other than SUCCESSFUL +# or FAILED will cause a CI error. +EXPECTED ?= SUCCESSFUL + +define yaml_encode_options + "$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')" +endef + +CI_FLAGS = $(CBMCFLAGS) $(CHECKFLAGS) $(COVERFLAGS) + +cbmc-batch.yaml: + @$(RM) $@ + @echo 'build_memory: $(JOB_MEMORY)' > $@ + @echo 'cbmcflags: $(strip $(call yaml_encode_options,$(CI_FLAGS)))' >> $@ + @echo 'coverage_memory: $(JOB_MEMORY)' >> $@ + @echo 'expected: $(EXPECTED)' >> $@ + @echo 'goto: $(HARNESS_GOTO).goto' >> $@ + @echo 'jobos: $(JOB_OS)' >> $@ + @echo 'property_memory: $(JOB_MEMORY)' >> $@ + @echo 'report_memory: $(JOB_MEMORY)' >> $@ + +.PHONY: cbmc-batch.yaml + +################################################################ + +# 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/regression/contracts/s2n_record_writev/minimized/NOTICE b/regression/contracts/s2n_record_writev/minimized/NOTICE new file mode 100644 index 00000000000..f8bbcc301b5 --- /dev/null +++ b/regression/contracts/s2n_record_writev/minimized/NOTICE @@ -0,0 +1,2 @@ +s2n +Copyright 2014-2015 Amazon.com, Inc. or its affiliates. All Rights Reserved. diff --git a/regression/contracts/s2n_record_writev/minimized/README b/regression/contracts/s2n_record_writev/minimized/README new file mode 100644 index 00000000000..dec999563e9 --- /dev/null +++ b/regression/contracts/s2n_record_writev/minimized/README @@ -0,0 +1,9 @@ +This directory contains an example of a problem encountered when +applying function contracts in the context of AWS s2n-tls. Run the +example by using the command: + +make veryclean && make result + +This creates a large problem during symbolic execution and solving. + +This test is currently not included in the any regression. \ No newline at end of file diff --git a/regression/contracts/s2n_record_writev/minimized/s2n_record_writev.c b/regression/contracts/s2n_record_writev/minimized/s2n_record_writev.c new file mode 100644 index 00000000000..7c383db4d52 --- /dev/null +++ b/regression/contracts/s2n_record_writev/minimized/s2n_record_writev.c @@ -0,0 +1,722 @@ +/* + * 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 +#include + +// iovec +#include +// sysconf +#include + +// clang-format off + +bool nondet_bool(); +int nondet_int(); +long nondet_long(); + +uint32_t nondet_uint32(); +uint64_t nondet_uint64(); +struct s2n_hash *nondet_s2n_hash(); +char *nondet_char_star(); + +// ============================= SAFETY ============================== + +#define S2N_SUCCESS 0 +#define S2N_FAILURE -1 + +#define __S2N_ENSURE(cond, action) \ + do { \ + if (!(cond)) { \ + action; \ + } \ + } while (0) + +#define POSIX_GUARD(result) \ + __S2N_ENSURE((result) >= S2N_SUCCESS, return S2N_FAILURE) + +#define S2N_IMPLIES(a, b) (!(a) || (b)) + +typedef struct { + int __error_signal; +} s2n_result; + +inline bool s2n_result_is_ok(s2n_result result) { + return result.__error_signal == S2N_SUCCESS; +} + +#define s2n_likely(x) __builtin_expect(!!(x), 1) +#define S2N_RESULT_OK ((s2n_result){S2N_SUCCESS}) +#define S2N_RESULT_ERROR ((s2n_result){S2N_FAILURE}) + +#define __S2N_ENSURE_PRECONDITION(result) \ + (s2n_likely(s2n_result_is_ok(result)) ? S2N_RESULT_OK : S2N_RESULT_ERROR) + +#define POSIX_GUARD_RESULT(result) \ + __S2N_ENSURE(s2n_result_is_ok(result), return S2N_FAILURE) +#define POSIX_PRECONDITION(result) \ + POSIX_GUARD_RESULT(__S2N_ENSURE_PRECONDITION((result))) + +int s2n_calculate_stacktrace() { + return nondet_bool() ? S2N_SUCCESS : S2N_FAILURE; +} + +__thread int s2n_errno; +__thread const char *s2n_debug_str; + +#define TO_STRING(s) #s +#define STRING_(s) TO_STRING(s) +#define STRING__LINE__ STRING_(__LINE__) +#define _S2N_DEBUG_LINE "Error encountered in " __FILE__ ":" STRING__LINE__ + +#define _S2N_ERROR(x) \ + do { \ + s2n_debug_str = _S2N_DEBUG_LINE; \ + s2n_errno = (x); \ + s2n_calculate_stacktrace(); \ + } while (0) + +#define POSIX_BAIL(error) \ + do { \ + _S2N_ERROR((error)); \ + return S2N_FAILURE; \ + } while (0) +#define POSIX_ENSURE(condition, error) \ + __S2N_ENSURE((condition), POSIX_BAIL(error)) + +// =========================== CBMC MACROS =========================== + +#ifdef CBMC +#define CONTRACT_ASSIGNS(...) __CPROVER_assigns(__VA_ARGS__) +#define CONTRACT_ASSIGNS_ERR(...) \ + __CPROVER_assigns(s2n_debug_str, s2n_errno; __VA_ARGS__) +#define CONTRACT_REQUIRES(...) __CPROVER_requires(__VA_ARGS__) +#define CONTRACT_ENSURES(...) __CPROVER_ensures(__VA_ARGS__) +#define CONTRACT_INVARIANT(...) __CPROVER_loop_invariant(__VA_ARGS__) +#define CONTRACT_LOOP_ENTRY(...) __CPROVER_loop_entry(__VA_ARGS__) +#define CONTRACT_RETURN_VALUE (__CPROVER_return_value) +#define CONTRACT_IS_FRESH(...) __CPROVER_is_fresh(__VA_ARGS__) +#define CONTRACT_OLD(...) __CPROVER_old(__VA_ARGS__) +#define CONTRACT_ENSURES_SUCCESS(...) \ + __CPROVER_ensures( \ + S2N_IMPLIES(CONTRACT_RETURN_VALUE >= S2N_SUCCESS, __VA_ARGS__)) +#define CONTRACT_ENSURES_FAILURE(...) \ + __CPROVER_ensures( \ + S2N_IMPLIES(CONTRACT_RETURN_VALUE <= S2N_FAILURE, __VA_ARGS__)) +#define CONTRACT_ENSURES_VALID_RETURN_VALUE \ + __CPROVER_ensures(__CPROVER_return_value == S2N_SUCCESS || \ + __CPROVER_return_value == S2N_FAILURE) +#define RW_OK(ptr) __CPROVER_rw_ok(ptr, sizeof(*(ptr))) +#define RW_OK_SIZE(ptr, size) __CPROVER_rw_ok(ptr, size) +#else +#define CONTRACT_ASSIGNS(...) +#define CONTRACT_ASSIGNS_ERR(...) +#define CONTRACT_REQUIRES(...) +#define CONTRACT_ENSURES(...) +#define CONTRACT_INVARIANT(...) +#define CONTRACT_LOOP_ENTRY(...) +#define CONTRACT_RETURN_VALUE +#define CONTRACT_IS_FRESH(...) +#define CONTRACT_OLD(...) +#define CONTRACT_ENSURES_SUCCESS(...) +#define CONTRACT_ENSURES_FAILURE(...) +#define CONTRACT_ENSURES_VALID_RETURN_VALUE +#define RW_OK(...) +#define RW_OK_SIZE(...) +#endif + +#define CBMC_ENSURE_REF(cond) \ + do { \ + if (!(cond)) { \ + return; \ + } \ + } while (0) + +// ============================ FIPS_MODE ============================ + +static int __CPROVER_s2n_fips_mode = 0; + +void s2n_fips_init(void) { __CPROVER_s2n_fips_mode = nondet_int(); } + +// force fips mode +int s2n_is_in_fips_mode() { return true; } + +// ========================== S2N_MEM_INIT =========================== + +static long page_size = 4096; + +long sysconf(int name) { return nondet_long(); } + +int s2n_mem_init() { + POSIX_GUARD(page_size = sysconf(_SC_PAGESIZE)); + + return 0; +} + +void __s2n_mem_init() { + if (nondet_bool()) { + s2n_mem_init(); + } +} + +// ============================= BIGNUM ============================== + +typedef struct bignum_st BIGNUM; + +/* Abstraction of the BIGNUM struct. */ +struct bignum_st { + bool is_initialized; + unsigned long int *d; /* Pointer to an array of 'BN_BITS2' bit + * chunks. */ + int top; /* Index of last used d +1. */ + /* The next are internal book keeping for bn_expand. */ + int dmax; /* Size of the d array. */ + int neg; /* one if the number is negative */ + int flags; +}; + +// ============================== OSSL =============================== + +#define MD5_LONG unsigned int +#define MD5_CBLOCK 64 +#define MD5_LBLOCK (MD5_CBLOCK / 4) + +typedef struct MD5state_st { + /* Internal buffers used during the computation. */ + MD5_LONG A, B, C, D; + /* The other subfields keep information on the running hash. */ + MD5_LONG Nl, Nh; + MD5_LONG data[MD5_LBLOCK]; + unsigned int num; +} MD5_CTX; + +#define SHA_LONG unsigned int +#define SHA_LBLOCK 16 +#define SHA_CBLOCK \ + (SHA_LBLOCK * 4) /* SHA treats input data as a \ + * contiguous array of 32 bit \ + * wide big-endian values. */ + +typedef struct SHAstate_st { + SHA_LONG h0, h1, h2, h3, h4; + SHA_LONG Nl, Nh; + SHA_LONG data[SHA_LBLOCK]; + unsigned int num; +} SHA_CTX; + +typedef struct SHA256state_st { + SHA_LONG h[8]; + SHA_LONG Nl, Nh; + SHA_LONG data[SHA_LBLOCK]; + unsigned int num, md_len; +} SHA256_CTX; + +#define SHA512_CBLOCK \ + (SHA_LBLOCK * 8) /* SHA-512 treats input data as a \ + * contiguous array of 64 bit \ + * wide big-endian values. */ +#define SHA_LONG64 unsigned long long +#define SHA512_DIGEST_LENGTH 64 + +typedef struct SHA512state_st { + SHA_LONG64 h[8]; + SHA_LONG64 Nl, Nh; + union { + SHA_LONG64 d[SHA_LBLOCK]; + unsigned char p[SHA512_CBLOCK]; + } u; + unsigned int num, md_len; +} SHA512_CTX; + +// =============================== EVP =============================== + +enum evp_sha { + EVP_MD5, + EVP_SHA1, + EVP_SHA224, + EVP_SHA256, + EVP_SHA384, + EVP_SHA512 +}; + +typedef struct evp_md_st EVP_MD; +typedef struct evp_md_ctx_st EVP_MD_CTX; +typedef struct evp_pkey_ctx_st EVP_PKEY_CTX; +typedef struct evp_pkey_st EVP_PKEY; +typedef struct ec_key_st EC_KEY; + +typedef enum { + POINT_CONVERSION_COMPRESSED = 2, + POINT_CONVERSION_UNCOMPRESSED = 4, + POINT_CONVERSION_HYBRID = 6 +} point_conversion_form_t; + +/* Abstraction of the EC_GROUP struct */ +struct ec_group_st { + int curve_name; + point_conversion_form_t asn1_form; + BIGNUM *order; +}; + +typedef struct ec_group_st EC_GROUP; + +/* Abstraction of the EC_KEY struct */ +struct ec_key_st { + int references; + EC_GROUP *group; + point_conversion_form_t conv_form; + BIGNUM *priv_key; + bool pub_key_is_set; // We never have to return a public-key object, so just + // having this flag is enough +}; + +struct evp_pkey_st { + int references; + EC_KEY *ec_key; +}; + +struct evp_pkey_ctx_st { + bool is_initialized_for_signing; + bool is_initialized_for_derivation; + bool is_initialized_for_encryption; + bool is_initialized_for_decryption; + int rsa_pad; + EVP_PKEY *pkey; +}; + +/* Abstraction of the EVP_MD struct. */ +struct evp_md_st { + enum evp_sha from; + + /* nid */ + int type; + + int pkey_type; + int md_size; + unsigned long flags; + int block_size; + /* How big does the ctx->md_data need to be. */ + int ctx_size; +}; + +struct evp_md_ctx_st { + const EVP_MD *digest; + + unsigned long flags; + void *md_data; + /* Public key context for sign/verify. */ + EVP_PKEY_CTX *pctx; +} /* EVP_MD_CTX */; + +struct s2n_evp_digest { + const EVP_MD *md; + EVP_MD_CTX *ctx; +}; + +// ========================= S2N_HASH_STATE ========================== + +typedef enum { + S2N_HASH_NONE = 0, + S2N_HASH_MD5, + S2N_HASH_SHA1, + S2N_HASH_SHA224, + S2N_HASH_SHA256, + S2N_HASH_SHA384, + S2N_HASH_SHA512, + S2N_HASH_MD5_SHA1, + /* Don't add any hash algorithms below S2N_HASH_SENTINEL */ + S2N_HASH_SENTINEL +} s2n_hash_algorithm; + +/* The low_level_digest stores all OpenSSL structs that are alg-specific to be + * used with OpenSSL's low-level hash API's. */ +union s2n_hash_low_level_digest { + MD5_CTX md5; + SHA_CTX sha1; + SHA256_CTX sha224; + SHA256_CTX sha256; + SHA512_CTX sha384; + SHA512_CTX sha512; + struct { + MD5_CTX md5; + SHA_CTX sha1; + } md5_sha1; +}; + +/* The evp_digest stores all OpenSSL structs to be used with OpenSSL's EVP hash + * API's. */ +struct s2n_hash_evp_digest { + struct s2n_evp_digest evp; + /* Always store a secondary evp_digest to allow resetting a hash_state to + * MD5_SHA1 from another alg. */ + struct s2n_evp_digest evp_md5_secondary; +}; + +struct s2n_hash_state { + const struct s2n_hash *hash_impl; + s2n_hash_algorithm alg; + uint8_t is_ready_for_input; + uint64_t currently_in_hash; + union { + union s2n_hash_low_level_digest low_level; + struct s2n_hash_evp_digest high_level; + } digest; +}; + +struct s2n_hash { + int (*alloc)(struct s2n_hash_state *state); + int (*allow_md5_for_fips)(struct s2n_hash_state *state); + int (*init)(struct s2n_hash_state *state, s2n_hash_algorithm alg); + int (*update)(struct s2n_hash_state *state, const void *data, uint32_t size); + int (*digest)(struct s2n_hash_state *state, void *out, uint32_t size); + int (*copy)(struct s2n_hash_state *to, struct s2n_hash_state *from); + int (*reset)(struct s2n_hash_state *state); + int (*free)(struct s2n_hash_state *state); +}; + +// ========================= S2N_HMAC_STATE ========================== + +typedef enum { + S2N_HMAC_NONE, + S2N_HMAC_MD5, + S2N_HMAC_SHA1, + S2N_HMAC_SHA224, + S2N_HMAC_SHA256, + S2N_HMAC_SHA384, + S2N_HMAC_SHA512, + S2N_HMAC_SSLv3_MD5, + S2N_HMAC_SSLv3_SHA1 +} s2n_hmac_algorithm; + +struct s2n_hmac_state { + s2n_hmac_algorithm alg; + + uint16_t hash_block_size; + uint32_t currently_in_hash_block; + uint16_t xor_pad_size; + uint8_t digest_size; + + struct s2n_hash_state inner; + struct s2n_hash_state inner_just_key; + struct s2n_hash_state outer; + struct s2n_hash_state outer_just_key; + + /* key needs to be as large as the biggest block size */ + uint8_t xor_pad[128]; + + /* For storing the inner digest */ + uint8_t digest_pad[SHA512_DIGEST_LENGTH]; +}; + +// ====================== S2N_CRYPTO_PARAMETERS ====================== + +#define S2N_TLS_SEQUENCE_NUM_LEN 8 + +struct s2n_crypto_parameters { + struct s2n_hmac_state client_record_mac; + struct s2n_hmac_state server_record_mac; + uint8_t client_sequence_number[S2N_TLS_SEQUENCE_NUM_LEN]; + uint8_t server_sequence_number[S2N_TLS_SEQUENCE_NUM_LEN]; +}; + +// =========================== S2N_STUFFER =========================== + +struct s2n_blob { + /* The data for the s2n_blob */ + uint8_t *data; + + /* The size of the data */ + uint32_t size; + + /* The amount of memory allocated for this blob (i.e. the amount of memory + * which needs to be freed when the blob is cleaned up). If this blob was + * created with s2n_blob_init(), this value is 0. If s2n_alloc() was called, + * this value will be greater than 0. + */ + uint32_t allocated; + + /* Can this blob be resized */ + unsigned growable : 1; +}; + +struct s2n_stuffer { + /* The data for the s2n_stuffer */ + struct s2n_blob blob; + + /* Cursors to the current read/write position in the s2n_stuffer */ + uint32_t read_cursor; + uint32_t write_cursor; + uint32_t high_water_mark; + + /* Was this stuffer alloc()'d ? */ + unsigned int alloced : 1; + + /* Is this stuffer growable? */ + unsigned int growable : 1; + + /* Can this stuffer be safely resized? + * A growable stuffer can be temporarily tainted by a raw read/write, + * preventing it from resizing. */ + unsigned int tainted : 1; +}; + +// ========================= S2N_CONNECTION ========================== + +typedef enum { S2N_SERVER, S2N_CLIENT } s2n_mode; + +struct s2n_connection { + s2n_mode mode; + + struct s2n_crypto_parameters *initial; + struct s2n_crypto_parameters *secure; + + struct s2n_crypto_parameters *client; + struct s2n_crypto_parameters *server; + + struct s2n_stuffer out; +}; + +// ========================= S2N_HMAC_UPDATE ========================= + +/* int s2n_hmac_update(struct s2n_hmac_state *state, const void *in, uint32_t size) */ +/* { */ +/* // assert(size != 0 && size <= __CPROVER_max_malloc_size); */ +/* // assert(RW_OK(state)); */ +/* // assert(RW_OK_SIZE(in, size)); */ +/* // assert(!s2n_is_in_fips_mode() || RW_OK(state->inner.digest.high_level.evp.ctx)); */ +/* // assert(!s2n_is_in_fips_mode() || RW_OK(state->inner.digest.high_level.evp_md5_secondary.ctx)); */ +/* assert(!s2n_is_in_fips_mode() || RW_OK(state->inner.digest.high_level.evp.ctx->digest)); */ +/* // assert(!s2n_is_in_fips_mode() || RW_OK(state->inner.digest.high_level.evp_md5_secondary.ctx->digest)); */ + +/* // // havoc state */ +/* // // s2n_debug_str = nondet_char_star(); // do create nondet pointers */ +/* state->inner.hash_impl = nondet_s2n_hash(); // do not create nondet pointers */ +/* // s2n_errno = nondet_int(); */ +/* // state->currently_in_hash_block = nondet_uint32(); */ +/* // state->inner.currently_in_hash = nondet_uint64(); */ +/* // if(s2n_is_in_fips_mode()) */ +/* // { */ +/* // __CPROVER_havoc_object(state->inner.digest.high_level.evp.ctx->digest); */ +/* // __CPROVER_havoc_object(state->inner.digest.high_level.evp_md5_secondary.ctx->digest); */ +/* // } */ +/* return nondet_bool() ? S2N_SUCCESS : S2N_FAILURE; */ +/* } */ + +// ======================== S2N_RECORD_WRITEV ======================== + +#define S2N_TLS_SEQUENCE_NUM_LEN 8 +#define S2N_TLS_CONTENT_TYPE_LENGTH 1 +#define S2N_TLS_PROTOCOL_VERSION_LEN 2 +#define S2N_TLS_RECORD_HEADER_LENGTH \ + (S2N_TLS_CONTENT_TYPE_LENGTH + S2N_TLS_PROTOCOL_VERSION_LEN + 2) + +int s2n_record_writev(struct s2n_connection *conn, uint8_t content_type, + const struct iovec *in, size_t in_count, size_t offs, + size_t to_write) +{ + conn->client = conn->initial; + conn->server = conn->initial; + + struct s2n_hmac_state *mac; + + if (conn->mode == S2N_CLIENT) { + mac = &conn->client->client_record_mac; + } else { + mac = &conn->server->server_record_mac; + } + mac->inner.hash_impl = nondet_s2n_hash(); // do not create nondet pointers + assert(!s2n_is_in_fips_mode() || RW_OK(mac->inner.digest.high_level.evp.ctx->digest)); + + return 0; +} + +// ============================ POPULATE ============================= + +void cbmc_populate_BIGNUM(BIGNUM *bignum) { + CBMC_ENSURE_REF(bignum); + bignum->d = malloc(sizeof(*(bignum->d))); +} + +BIGNUM *cbmc_allocate_BIGNUM() { + BIGNUM *bignum = malloc(sizeof(*bignum)); + cbmc_populate_BIGNUM(bignum); + return bignum; +} + +void cbmc_populate_EC_GROUP(EC_GROUP *ec_group) { + CBMC_ENSURE_REF(ec_group); + ec_group->order = cbmc_allocate_BIGNUM(); +} + +EC_GROUP *cbmc_allocate_EC_GROUP() { + EC_GROUP *ec_group = malloc(sizeof(*ec_group)); + cbmc_populate_EC_GROUP(ec_group); + return ec_group; +} + +void cbmc_populate_EC_KEY(EC_KEY *ec_key) { + CBMC_ENSURE_REF(ec_key); + ec_key->group = cbmc_allocate_EC_GROUP(); + ec_key->priv_key = cbmc_allocate_BIGNUM(); +} + +EC_KEY *cbmc_allocate_EC_KEY() { + EC_KEY *ec_key = malloc(sizeof(*ec_key)); + cbmc_populate_EC_KEY(ec_key); + return ec_key; +} + +void cbmc_populate_EVP_PKEY(EVP_PKEY *evp_pkey) { + CBMC_ENSURE_REF(evp_pkey); + evp_pkey->ec_key = cbmc_allocate_EC_KEY(); +} + +EVP_PKEY *cbmc_allocate_EVP_PKEY() { + EVP_PKEY *evp_pkey = malloc(sizeof(*evp_pkey)); + cbmc_populate_EVP_PKEY(evp_pkey); + return evp_pkey; +} + +void cbmc_populate_EVP_PKEY_CTX(EVP_PKEY_CTX *evp_pkey_ctx) { + CBMC_ENSURE_REF(evp_pkey_ctx); + evp_pkey_ctx->pkey = cbmc_allocate_EVP_PKEY(); +} + +EVP_PKEY_CTX *cbmc_allocate_EVP_PKEY_CTX() { + EVP_PKEY_CTX *evp_pkey_ctx = malloc(sizeof(*evp_pkey_ctx)); + cbmc_populate_EVP_PKEY_CTX(evp_pkey_ctx); + return evp_pkey_ctx; +} + +#define EVP_MAX_MD_SIZE 64 /* Longest known is SHA512. */ + +void cbmc_populate_EVP_MD_CTX(EVP_MD_CTX *ctx) { + CBMC_ENSURE_REF(ctx); + ctx->digest = malloc(sizeof(*(ctx->digest))); + ctx->md_data = malloc(EVP_MAX_MD_SIZE); + ctx->pctx = cbmc_allocate_EVP_PKEY_CTX(); +} + +EVP_MD_CTX *cbmc_allocate_EVP_MD_CTX() { + EVP_MD_CTX *ctx = malloc(sizeof(*ctx)); + cbmc_populate_EVP_MD_CTX(ctx); + return ctx; +} + +void cbmc_populate_s2n_evp_digest(struct s2n_evp_digest *evp_digest) { + CBMC_ENSURE_REF(evp_digest); + /* `evp_digest->md` is never allocated. + * It is always initialized based on the hashing algorithm. + * If required, this initialization should be done in the validation function. + */ + evp_digest->ctx = cbmc_allocate_EVP_MD_CTX(); +} + +void cbmc_populate_s2n_hash_state(struct s2n_hash_state *state) { + CBMC_ENSURE_REF(state); + /* `state->hash_impl` is never allocated. + * It is always initialized based on the hashing algorithm. + * If required, this initialization should be done in the validation function. + */ + cbmc_populate_s2n_evp_digest(&state->digest.high_level.evp); + cbmc_populate_s2n_evp_digest(&state->digest.high_level.evp_md5_secondary); +} + +void cbmc_populate_s2n_hmac_state(struct s2n_hmac_state *state) { + CBMC_ENSURE_REF(state); + cbmc_populate_s2n_hash_state(&state->inner); + // commented because these are never accessed during the proof + // cbmc_populate_s2n_hash_state(&state->inner_just_key); + // cbmc_populate_s2n_hash_state(&state->outer); + // cbmc_populate_s2n_hash_state(&state->outer_just_key); +} + +void cbmc_populate_s2n_blob(struct s2n_blob *blob) { + CBMC_ENSURE_REF(blob); + if (blob->growable) { + blob->data = (blob->allocated == 0) ? NULL : malloc(blob->allocated); + } else { + blob->data = (blob->size == 0) ? NULL : malloc(blob->size); + } +} + +void cbmc_populate_s2n_stuffer(struct s2n_stuffer *stuffer) { + CBMC_ENSURE_REF(stuffer); + cbmc_populate_s2n_blob(&stuffer->blob); +} + +struct s2n_stuffer *cbmc_allocate_s2n_stuffer() { + struct s2n_stuffer *stuffer = malloc(sizeof(*stuffer)); + cbmc_populate_s2n_stuffer(stuffer); + return stuffer; +} + +// ============================= HARNESS ============================= + +void s2n_record_writev_harness() { + /* Non-deterministic input allocation. */ + struct s2n_connection *conn = malloc(sizeof(*conn)); + + struct s2n_hmac_state client_record_mac; + cbmc_populate_s2n_hmac_state(&(client_record_mac)); + + struct s2n_hmac_state server_record_mac; + cbmc_populate_s2n_hmac_state(&(server_record_mac)); + + struct s2n_stuffer *conn_out = cbmc_allocate_s2n_stuffer(); + + if (conn) { + conn->out = *conn_out; + /* initial */ + conn->initial = malloc(sizeof(*(conn->initial))); + if (conn->initial) { + conn->initial->client_record_mac = client_record_mac; + conn->initial->server_record_mac = server_record_mac; + } + + /* client */ + conn->client = malloc(sizeof(*(conn->client))); + if (conn->client) { + conn->client->client_record_mac = client_record_mac; + } + + /* server */ + conn->server = malloc(sizeof(*(conn->server))); + if (conn->server) { + conn->server->server_record_mac = server_record_mac; + } + } + uint8_t content_type; + const struct iovec *in = malloc(sizeof(*in)); + size_t in_count; + uint32_t offs; + size_t to_write; + + /* Extra assumptions. */ + __s2n_mem_init(); + + /* Initialize s2n_fips_mode nondetermistically. Check stub for + * details */ + s2n_fips_init(); + + // so the funciton does not get dropped; + s2n_is_in_fips_mode(); + + /* Operation under verification. */ + s2n_record_writev(conn, content_type, in, in_count, offs, to_write); +} + +// clang-format on diff --git a/regression/contracts/s2n_record_writev/s2n_record_writev.c b/regression/contracts/s2n_record_writev/s2n_record_writev.c new file mode 100644 index 00000000000..1ede0e3fdcf --- /dev/null +++ b/regression/contracts/s2n_record_writev/s2n_record_writev.c @@ -0,0 +1,809 @@ +/* + * 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. + */ + +// clang-format off + +#include +#include +#include + +// iovec +#include +// sysconf +#include + + +bool nondet_bool(); +int nondet_int(); +long nondet_long(); + +// ============================= SAFETY ============================== + +#define S2N_SUCCESS 0 +#define S2N_FAILURE -1 + +#define __S2N_ENSURE( cond, action ) do {if ( !(cond) ) { action; }} while (0) + +#define POSIX_GUARD(result) __S2N_ENSURE((result) >= S2N_SUCCESS, return S2N_FAILURE) + +#define S2N_IMPLIES(a, b) (!(a) || (b)) + +typedef struct { + int __error_signal; +} s2n_result; + +inline bool s2n_result_is_ok(s2n_result result) +{ + return result.__error_signal == S2N_SUCCESS; +} + +#define s2n_likely(x) __builtin_expect(!!(x), 1) +#define S2N_RESULT_OK ((s2n_result) { S2N_SUCCESS }) +#define S2N_RESULT_ERROR ((s2n_result) { S2N_FAILURE }) + +#define __S2N_ENSURE_PRECONDITION( result ) (s2n_likely(s2n_result_is_ok(result)) ? S2N_RESULT_OK : S2N_RESULT_ERROR) + +#define POSIX_GUARD_RESULT(result) __S2N_ENSURE(s2n_result_is_ok(result), return S2N_FAILURE) +#define POSIX_PRECONDITION(result) POSIX_GUARD_RESULT(__S2N_ENSURE_PRECONDITION((result))) + +int s2n_calculate_stacktrace() { return nondet_bool() ? S2N_SUCCESS : S2N_FAILURE; } + +__thread int s2n_errno; +__thread const char *s2n_debug_str; + +#define TO_STRING(s) #s +#define STRING_(s) TO_STRING(s) +#define STRING__LINE__ STRING_(__LINE__) +#define _S2N_DEBUG_LINE "Error encountered in " __FILE__ ":" STRING__LINE__ + + +#define _S2N_ERROR( x ) do { s2n_debug_str = _S2N_DEBUG_LINE; s2n_errno = ( x ); s2n_calculate_stacktrace(); } while (0) + +#define POSIX_BAIL(error) do { _S2N_ERROR((error)); return S2N_FAILURE; } while (0) +#define POSIX_ENSURE(condition, error) __S2N_ENSURE((condition), POSIX_BAIL(error)) + + +// =========================== CBMC MACROS =========================== + +#ifdef CBMC +# define CONTRACT_ASSIGNS(...) __CPROVER_assigns(__VA_ARGS__) +# define CONTRACT_ASSIGNS_ERR(...) __CPROVER_assigns(s2n_debug_str, s2n_errno; __VA_ARGS__) +# define CONTRACT_REQUIRES(...) __CPROVER_requires(__VA_ARGS__) +# define CONTRACT_ENSURES(...) __CPROVER_ensures(__VA_ARGS__) +# define CONTRACT_INVARIANT(...) __CPROVER_loop_invariant(__VA_ARGS__) +# define CONTRACT_LOOP_ENTRY(...) __CPROVER_loop_entry(__VA_ARGS__) +# define CONTRACT_RETURN_VALUE (__CPROVER_return_value) +# define CONTRACT_IS_FRESH(...) __CPROVER_is_fresh(__VA_ARGS__) +# define CONTRACT_OLD(...) __CPROVER_old(__VA_ARGS__) +# define CONTRACT_ENSURES_SUCCESS(...) __CPROVER_ensures(S2N_IMPLIES(CONTRACT_RETURN_VALUE >= S2N_SUCCESS, __VA_ARGS__)) +# define CONTRACT_ENSURES_FAILURE(...) __CPROVER_ensures(S2N_IMPLIES(CONTRACT_RETURN_VALUE <= S2N_FAILURE, __VA_ARGS__)) +# define CONTRACT_ENSURES_VALID_RETURN_VALUE __CPROVER_ensures(__CPROVER_return_value == S2N_SUCCESS || __CPROVER_return_value == S2N_FAILURE) +# define RW_OK(ptr) __CPROVER_rw_ok(ptr, sizeof(*(ptr))) +# define RW_OK_SIZE(ptr, size) __CPROVER_rw_ok(ptr, size) +#else +# define CONTRACT_ASSIGNS(...) +# define CONTRACT_ASSIGNS_ERR(...) +# define CONTRACT_REQUIRES(...) +# define CONTRACT_ENSURES(...) +# define CONTRACT_INVARIANT(...) +# define CONTRACT_LOOP_ENTRY(...) +# define CONTRACT_RETURN_VALUE +# define CONTRACT_IS_FRESH(...) +# define CONTRACT_OLD(...) +# define CONTRACT_ENSURES_SUCCESS(...) +# define CONTRACT_ENSURES_FAILURE(...) +# define CONTRACT_ENSURES_VALID_RETURN_VALUE +# define RW_OK(...) +# define RW_OK_SIZE(...) +#endif + +#define CBMC_ENSURE_REF(cond) \ + do { \ + if (!(cond)) { return; } \ + } while (0) + + +// ============================ FIPS_MODE ============================ + +static int __CPROVER_s2n_fips_mode = 0; + +void s2n_fips_init(void) { + __CPROVER_s2n_fips_mode = nondet_int(); +} + +int s2n_is_in_fips_mode() +{ + return __CPROVER_s2n_fips_mode; +} + +// ========================== S2N_MEM_INIT =========================== + +static long page_size = 4096; + +long sysconf(int name) { return nondet_long(); } + + +int s2n_mem_init() +{ + POSIX_GUARD(page_size = sysconf(_SC_PAGESIZE)); + + return 0; +} + +void s2n_mem_init_nondet() { + if (nondet_bool()) { + s2n_mem_init(); + } +} + + +// ============================= BIGNUM ============================== + +typedef struct bignum_st BIGNUM; + +/* Abstraction of the BIGNUM struct. */ +struct bignum_st { + bool is_initialized; + unsigned long int *d; /* Pointer to an array of 'BN_BITS2' bit + * chunks. */ + int top; /* Index of last used d +1. */ + /* The next are internal book keeping for bn_expand. */ + int dmax; /* Size of the d array. */ + int neg; /* one if the number is negative */ + int flags; +}; + + +// ============================== OSSL =============================== + +#define MD5_LONG unsigned int +#define MD5_CBLOCK 64 +#define MD5_LBLOCK (MD5_CBLOCK / 4) + +typedef struct MD5state_st { + /* Internal buffers used during the computation. */ + MD5_LONG A, B, C, D; + /* The other subfields keep information on the running hash. */ + MD5_LONG Nl, Nh; + MD5_LONG data[MD5_LBLOCK]; + unsigned int num; +} MD5_CTX; + + +#define SHA_LONG unsigned int +#define SHA_LBLOCK 16 +#define SHA_CBLOCK \ + (SHA_LBLOCK * 4) /* SHA treats input data as a \ + * contiguous array of 32 bit \ + * wide big-endian values. */ + +typedef struct SHAstate_st { + SHA_LONG h0, h1, h2, h3, h4; + SHA_LONG Nl, Nh; + SHA_LONG data[SHA_LBLOCK]; + unsigned int num; +} SHA_CTX; + +typedef struct SHA256state_st { + SHA_LONG h[8]; + SHA_LONG Nl, Nh; + SHA_LONG data[SHA_LBLOCK]; + unsigned int num, md_len; +} SHA256_CTX; + +#define SHA512_CBLOCK \ + (SHA_LBLOCK * 8) /* SHA-512 treats input data as a \ + * contiguous array of 64 bit \ + * wide big-endian values. */ +#define SHA_LONG64 unsigned long long +#define SHA512_DIGEST_LENGTH 64 + +typedef struct SHA512state_st { + SHA_LONG64 h[8]; + SHA_LONG64 Nl, Nh; + union { + SHA_LONG64 d[SHA_LBLOCK]; + unsigned char p[SHA512_CBLOCK]; + } u; + unsigned int num, md_len; +} SHA512_CTX; + + +// =============================== EVP =============================== + +enum evp_sha { EVP_MD5, EVP_SHA1, EVP_SHA224, EVP_SHA256, EVP_SHA384, EVP_SHA512 }; + +typedef struct evp_md_st EVP_MD; +typedef struct evp_md_ctx_st EVP_MD_CTX; +typedef struct evp_pkey_ctx_st EVP_PKEY_CTX; +typedef struct evp_pkey_st EVP_PKEY; +typedef struct ec_key_st EC_KEY; + +typedef enum { + POINT_CONVERSION_COMPRESSED = 2, + POINT_CONVERSION_UNCOMPRESSED = 4, + POINT_CONVERSION_HYBRID = 6 +} point_conversion_form_t; + +/* Abstraction of the EC_GROUP struct */ +struct ec_group_st { + int curve_name; + point_conversion_form_t asn1_form; + BIGNUM *order; +}; + +typedef struct ec_group_st EC_GROUP; + +/* Abstraction of the EC_KEY struct */ +struct ec_key_st { + int references; + EC_GROUP *group; + point_conversion_form_t conv_form; + BIGNUM *priv_key; + bool pub_key_is_set; // We never have to return a public-key object, so just having this flag is enough +}; + +struct evp_pkey_st { + int references; + EC_KEY *ec_key; +}; + +struct evp_pkey_ctx_st { + bool is_initialized_for_signing; + bool is_initialized_for_derivation; + bool is_initialized_for_encryption; + bool is_initialized_for_decryption; + int rsa_pad; + EVP_PKEY *pkey; +}; + +/* Abstraction of the EVP_MD struct. */ +struct evp_md_st { + enum evp_sha from; + + /* nid */ + int type; + + int pkey_type; + int md_size; + unsigned long flags; + int block_size; + /* How big does the ctx->md_data need to be. */ + int ctx_size; +}; + + +struct evp_md_ctx_st { + const EVP_MD *digest; + + unsigned long flags; + void *md_data; + /* Public key context for sign/verify. */ + EVP_PKEY_CTX *pctx; +} /* EVP_MD_CTX */; + + +struct s2n_evp_digest { + const EVP_MD *md; + EVP_MD_CTX *ctx; +}; + + + +// ========================= S2N_HASH_STATE ========================== + +typedef enum { + S2N_HASH_NONE=0, + S2N_HASH_MD5, + S2N_HASH_SHA1, + S2N_HASH_SHA224, + S2N_HASH_SHA256, + S2N_HASH_SHA384, + S2N_HASH_SHA512, + S2N_HASH_MD5_SHA1, + /* Don't add any hash algorithms below S2N_HASH_SENTINEL */ + S2N_HASH_SENTINEL +} s2n_hash_algorithm; + + + + +/* The low_level_digest stores all OpenSSL structs that are alg-specific to be used with OpenSSL's low-level hash API's. */ +union s2n_hash_low_level_digest { + MD5_CTX md5; + SHA_CTX sha1; + SHA256_CTX sha224; + SHA256_CTX sha256; + SHA512_CTX sha384; + SHA512_CTX sha512; + struct { + MD5_CTX md5; + SHA_CTX sha1; + } md5_sha1; +}; + +/* The evp_digest stores all OpenSSL structs to be used with OpenSSL's EVP hash API's. */ +struct s2n_hash_evp_digest { + struct s2n_evp_digest evp; + /* Always store a secondary evp_digest to allow resetting a hash_state to MD5_SHA1 from another alg. */ + struct s2n_evp_digest evp_md5_secondary; +}; + + +struct s2n_hash_state { + const struct s2n_hash *hash_impl; + s2n_hash_algorithm alg; + uint8_t is_ready_for_input; + uint64_t currently_in_hash; + union { + union s2n_hash_low_level_digest low_level; + struct s2n_hash_evp_digest high_level; + } digest; +}; + +struct s2n_hash { + int (*alloc) (struct s2n_hash_state *state); + int (*allow_md5_for_fips) (struct s2n_hash_state *state); + int (*init) (struct s2n_hash_state *state, s2n_hash_algorithm alg); + int (*update) (struct s2n_hash_state *state, const void *data, uint32_t size); + int (*digest) (struct s2n_hash_state *state, void *out, uint32_t size); + int (*copy) (struct s2n_hash_state *to, struct s2n_hash_state *from); + int (*reset) (struct s2n_hash_state *state); + int (*free) (struct s2n_hash_state *state); +}; + + +// ========================= S2N_HMAC_STATE ========================== + +typedef enum { + S2N_HMAC_NONE, + S2N_HMAC_MD5, + S2N_HMAC_SHA1, + S2N_HMAC_SHA224, + S2N_HMAC_SHA256, + S2N_HMAC_SHA384, + S2N_HMAC_SHA512, + S2N_HMAC_SSLv3_MD5, + S2N_HMAC_SSLv3_SHA1 +} s2n_hmac_algorithm; + + +struct s2n_hmac_state { + s2n_hmac_algorithm alg; + + uint16_t hash_block_size; + uint32_t currently_in_hash_block; + uint16_t xor_pad_size; + uint8_t digest_size; + + struct s2n_hash_state inner; + struct s2n_hash_state inner_just_key; + struct s2n_hash_state outer; + struct s2n_hash_state outer_just_key; + + /* key needs to be as large as the biggest block size */ + uint8_t xor_pad[128]; + + /* For storing the inner digest */ + uint8_t digest_pad[SHA512_DIGEST_LENGTH]; +}; + + +// ====================== S2N_CRYPTO_PARAMETERS ====================== + +#define S2N_TLS_SEQUENCE_NUM_LEN 8 + +struct s2n_crypto_parameters { + struct s2n_hmac_state client_record_mac; + struct s2n_hmac_state server_record_mac; + uint8_t client_sequence_number[S2N_TLS_SEQUENCE_NUM_LEN]; + uint8_t server_sequence_number[S2N_TLS_SEQUENCE_NUM_LEN]; +}; + + + +// =========================== S2N_STUFFER =========================== + +struct s2n_blob { + /* The data for the s2n_blob */ + uint8_t *data; + + /* The size of the data */ + uint32_t size; + + /* The amount of memory allocated for this blob (i.e. the amount of memory + * which needs to be freed when the blob is cleaned up). If this blob was + * created with s2n_blob_init(), this value is 0. If s2n_alloc() was called, + * this value will be greater than 0. + */ + uint32_t allocated; + + /* Can this blob be resized */ + unsigned growable :1; +}; + +struct s2n_stuffer { + /* The data for the s2n_stuffer */ + struct s2n_blob blob; + + /* Cursors to the current read/write position in the s2n_stuffer */ + uint32_t read_cursor; + uint32_t write_cursor; + uint32_t high_water_mark; + + /* Was this stuffer alloc()'d ? */ + unsigned int alloced:1; + + /* Is this stuffer growable? */ + unsigned int growable:1; + + /* Can this stuffer be safely resized? + * A growable stuffer can be temporarily tainted by a raw read/write, + * preventing it from resizing. */ + unsigned int tainted:1; +}; + + + +// ========================= S2N_CONNECTION ========================== + +typedef enum { S2N_SERVER, S2N_CLIENT } s2n_mode; + +struct s2n_connection { + s2n_mode mode; + + struct s2n_crypto_parameters *initial; + struct s2n_crypto_parameters *secure; + + struct s2n_crypto_parameters *client; + struct s2n_crypto_parameters *server; + + struct s2n_stuffer out; +}; + + + + +// ========================= S2N_HMAC_UPDATE ========================= + +int s2n_hmac_update(struct s2n_hmac_state *state, const void *in, uint32_t size) + CONTRACT_REQUIRES(size != 0 && size <= __CPROVER_max_malloc_size) + CONTRACT_REQUIRES(RW_OK(state)) + CONTRACT_REQUIRES(RW_OK_SIZE(in, size)) + CONTRACT_REQUIRES(S2N_IMPLIES(s2n_is_in_fips_mode(), + RW_OK(state->inner.digest.high_level.evp.ctx) + && RW_OK(state->inner.digest.high_level.evp.ctx->digest) + && RW_OK(state->inner.digest.high_level.evp_md5_secondary.ctx) + && RW_OK(state->inner.digest.high_level.evp_md5_secondary.ctx->digest))) + CONTRACT_ASSIGNS(s2n_debug_str, s2n_errno; + state->currently_in_hash_block, + state->inner.hash_impl, + state->inner.currently_in_hash; + s2n_is_in_fips_mode(): + *(state->inner.digest.high_level.evp.ctx->digest), + *(state->inner.digest.high_level.evp_md5_secondary.ctx->digest)) + CONTRACT_ENSURES_VALID_RETURN_VALUE +{ + return 0; +} + + +// ======================== S2N_RECORD_WRITEV ======================== + +#define S2N_TLS_SEQUENCE_NUM_LEN 8 +#define S2N_TLS_CONTENT_TYPE_LENGTH 1 +#define S2N_TLS_PROTOCOL_VERSION_LEN 2 +#define S2N_TLS_RECORD_HEADER_LENGTH (S2N_TLS_CONTENT_TYPE_LENGTH + S2N_TLS_PROTOCOL_VERSION_LEN + 2) + + +int s2n_record_writev(struct s2n_connection *conn, uint8_t content_type, const struct iovec *in, size_t in_count, size_t offs, size_t to_write) + CONTRACT_REQUIRES(conn != NULL) + CONTRACT_REQUIRES(conn->initial != NULL) + CONTRACT_REQUIRES(conn->client != NULL) + CONTRACT_REQUIRES(conn->server != NULL) + CONTRACT_REQUIRES(S2N_IMPLIES(s2n_is_in_fips_mode(), + RW_OK(conn->client->client_record_mac.inner.digest.high_level.evp.ctx) + && RW_OK(conn->client->client_record_mac.inner.digest.high_level.evp.ctx->digest) + && RW_OK(conn->client->client_record_mac.inner.digest.high_level.evp_md5_secondary.ctx) + && RW_OK(conn->client->client_record_mac.inner.digest.high_level.evp_md5_secondary.ctx->digest) + && RW_OK(conn->server->server_record_mac.inner.digest.high_level.evp.ctx) + && RW_OK(conn->server->server_record_mac.inner.digest.high_level.evp.ctx->digest) + && RW_OK(conn->server->server_record_mac.inner.digest.high_level.evp_md5_secondary.ctx) + && RW_OK(conn->server->server_record_mac.inner.digest.high_level.evp_md5_secondary.ctx->digest) + && RW_OK(conn->initial->client_record_mac.inner.digest.high_level.evp.ctx) + && RW_OK(conn->initial->client_record_mac.inner.digest.high_level.evp.ctx->digest) + && RW_OK(conn->initial->client_record_mac.inner.digest.high_level.evp_md5_secondary.ctx) + && RW_OK(conn->initial->client_record_mac.inner.digest.high_level.evp_md5_secondary.ctx->digest) + && RW_OK(conn->initial->server_record_mac.inner.digest.high_level.evp.ctx) + && RW_OK(conn->initial->server_record_mac.inner.digest.high_level.evp.ctx->digest) + && RW_OK(conn->initial->server_record_mac.inner.digest.high_level.evp_md5_secondary.ctx) + && RW_OK(conn->initial->server_record_mac.inner.digest.high_level.evp_md5_secondary.ctx->digest))) +CONTRACT_ASSIGNS(s2n_debug_str, s2n_errno; + conn->initial, + conn->server, + conn->client, + conn->out, + __CPROVER_object_upto(conn->out.blob.data, conn->out.blob.size), + + conn->initial->client_sequence_number, + conn->initial->client_record_mac.inner.hash_impl, + conn->initial->client_record_mac.inner.currently_in_hash, + conn->initial->client_record_mac.currently_in_hash_block, + conn->initial->server_sequence_number, + conn->initial->server_record_mac.inner.hash_impl, + conn->initial->server_record_mac.inner.currently_in_hash, + conn->initial->server_record_mac.currently_in_hash_block, + conn->client->client_sequence_number, + conn->client->client_record_mac.inner.hash_impl, + conn->client->client_record_mac.inner.currently_in_hash, + conn->client->client_record_mac.currently_in_hash_block, + conn->server->server_sequence_number, + conn->server->server_record_mac.inner.hash_impl, + conn->server->server_record_mac.inner.currently_in_hash, + conn->server->server_record_mac.currently_in_hash_block; + s2n_is_in_fips_mode(): + *(conn->initial->client_record_mac.inner.digest.high_level.evp.ctx->digest), + *(conn->initial->client_record_mac.inner.digest.high_level.evp_md5_secondary.ctx->digest), + *(conn->initial->server_record_mac.inner.digest.high_level.evp.ctx->digest), + *(conn->initial->server_record_mac.inner.digest.high_level.evp_md5_secondary.ctx->digest), + *(conn->client->client_record_mac.inner.digest.high_level.evp.ctx->digest), + *(conn->client->client_record_mac.inner.digest.high_level.evp_md5_secondary.ctx->digest), + *(conn->server->server_record_mac.inner.digest.high_level.evp.ctx->digest), + *(conn->server->server_record_mac.inner.digest.high_level.evp_md5_secondary.ctx->digest) + ) +{ + /* if (conn->actual_protocol_version == S2N_TLS13 && content_type == TLS_CHANGE_CIPHER_SPEC) { */ + // THIS IS NECESSARY FOR HANG + conn->client = conn->initial; + conn->server = conn->initial; + /* } */ + + /* uint8_t *sequence_number = conn->server->server_sequence_number; */ + /* struct s2n_hmac_state *mac = &conn->server->server_record_mac; */ + uint8_t *sequence_number; + struct s2n_hmac_state *mac; + + if (conn->mode == S2N_CLIENT) { + sequence_number = conn->client->client_sequence_number; + mac = &conn->client->client_record_mac; + } else { + sequence_number = conn->server->server_sequence_number; + mac = &conn->server->server_record_mac; + } + + /* Start the MAC with the sequence number */ + POSIX_GUARD(s2n_hmac_update(mac, sequence_number, S2N_TLS_SEQUENCE_NUM_LEN)); + + // BOGUS ASSIGNMENT + /* mac->inner.hash_impl = &s2n_evp_hash; */ + + /* if (conn->actual_protocol_version > S2N_SSLv3) { */ + POSIX_GUARD(s2n_hmac_update(mac, conn->out.blob.data, S2N_TLS_RECORD_HEADER_LENGTH)); + /* } */ + + return 0; +} + + +// ============================ POPULATE ============================= + +void cbmc_populate_BIGNUM(BIGNUM *bignum) +{ + CBMC_ENSURE_REF(bignum); + bignum->d = malloc(sizeof(*(bignum->d))); +} + +BIGNUM *cbmc_allocate_BIGNUM() +{ + BIGNUM *bignum = malloc(sizeof(*bignum)); + cbmc_populate_BIGNUM(bignum); + return bignum; +} + + +void cbmc_populate_EC_GROUP(EC_GROUP *ec_group) +{ + CBMC_ENSURE_REF(ec_group); + ec_group->order = cbmc_allocate_BIGNUM(); +} + + +EC_GROUP *cbmc_allocate_EC_GROUP() +{ + EC_GROUP *ec_group = malloc(sizeof(*ec_group)); + cbmc_populate_EC_GROUP(ec_group); + return ec_group; +} + + +void cbmc_populate_EC_KEY(EC_KEY *ec_key) +{ + CBMC_ENSURE_REF(ec_key); + ec_key->group = cbmc_allocate_EC_GROUP(); + ec_key->priv_key = cbmc_allocate_BIGNUM(); +} + + +EC_KEY *cbmc_allocate_EC_KEY() +{ + EC_KEY *ec_key = malloc(sizeof(*ec_key)); + cbmc_populate_EC_KEY(ec_key); + return ec_key; +} + + +void cbmc_populate_EVP_PKEY(EVP_PKEY *evp_pkey) +{ + CBMC_ENSURE_REF(evp_pkey); + evp_pkey->ec_key = cbmc_allocate_EC_KEY(); +} + + +EVP_PKEY *cbmc_allocate_EVP_PKEY() +{ + EVP_PKEY *evp_pkey = malloc(sizeof(*evp_pkey)); + cbmc_populate_EVP_PKEY(evp_pkey); + return evp_pkey; +} + +void cbmc_populate_EVP_PKEY_CTX(EVP_PKEY_CTX *evp_pkey_ctx) +{ + CBMC_ENSURE_REF(evp_pkey_ctx); + evp_pkey_ctx->pkey = cbmc_allocate_EVP_PKEY(); +} + + +EVP_PKEY_CTX *cbmc_allocate_EVP_PKEY_CTX() +{ + EVP_PKEY_CTX *evp_pkey_ctx = malloc(sizeof(*evp_pkey_ctx)); + cbmc_populate_EVP_PKEY_CTX(evp_pkey_ctx); + return evp_pkey_ctx; +} + + +#define EVP_MAX_MD_SIZE 64 /* Longest known is SHA512. */ + +void cbmc_populate_EVP_MD_CTX(EVP_MD_CTX *ctx) +{ + CBMC_ENSURE_REF(ctx); + ctx->digest = malloc(sizeof(*(ctx->digest))); + ctx->md_data = malloc(EVP_MAX_MD_SIZE); + ctx->pctx = cbmc_allocate_EVP_PKEY_CTX(); +} + +EVP_MD_CTX *cbmc_allocate_EVP_MD_CTX() +{ + EVP_MD_CTX *ctx = malloc(sizeof(*ctx)); + cbmc_populate_EVP_MD_CTX(ctx); + return ctx; +} + +void cbmc_populate_s2n_evp_digest(struct s2n_evp_digest *evp_digest) { + CBMC_ENSURE_REF(evp_digest); + /* `evp_digest->md` is never allocated. + * It is always initialized based on the hashing algorithm. + * If required, this initialization should be done in the validation function. + */ + evp_digest->ctx = cbmc_allocate_EVP_MD_CTX(); +} + + +void cbmc_populate_s2n_hash_state(struct s2n_hash_state* state) +{ + CBMC_ENSURE_REF(state); + /* `state->hash_impl` is never allocated. + * It is always initialized based on the hashing algorithm. + * If required, this initialization should be done in the validation function. + */ + cbmc_populate_s2n_evp_digest(&state->digest.high_level.evp); + cbmc_populate_s2n_evp_digest(&state->digest.high_level.evp_md5_secondary); +} + +void cbmc_populate_s2n_hmac_state(struct s2n_hmac_state *state) +{ + CBMC_ENSURE_REF(state); + cbmc_populate_s2n_hash_state(&state->inner); + cbmc_populate_s2n_hash_state(&state->inner_just_key); + cbmc_populate_s2n_hash_state(&state->outer); + cbmc_populate_s2n_hash_state(&state->outer_just_key); +} + + + +void cbmc_populate_s2n_blob(struct s2n_blob *blob) +{ + CBMC_ENSURE_REF(blob); + if (blob->growable) { + blob->data = (blob->allocated == 0) ? NULL : malloc(blob->allocated); + } else { + blob->data = (blob->size == 0) ? NULL : malloc(blob->size); + } +} + +void cbmc_populate_s2n_stuffer(struct s2n_stuffer *stuffer) +{ + CBMC_ENSURE_REF(stuffer); + cbmc_populate_s2n_blob(&stuffer->blob); +} + +struct s2n_stuffer *cbmc_allocate_s2n_stuffer() +{ + struct s2n_stuffer *stuffer = malloc(sizeof(*stuffer)); + cbmc_populate_s2n_stuffer(stuffer); + return stuffer; +} + + + +// ============================= HARNESS ============================= + +void s2n_record_writev_harness() +{ + /* Non-deterministic input allocation. */ + struct s2n_connection *conn = malloc(sizeof(*conn)); + + + struct s2n_hmac_state client_record_mac; + cbmc_populate_s2n_hmac_state(&(client_record_mac)); + /* __CPROVER_assume(s2n_result_is_ok(s2n_hmac_state_validate(&(client_record_mac)))); */ + /* __CPROVER_file_local_s2n_hash_c_s2n_hash_set_impl(&(client_record_mac)); */ + struct s2n_hmac_state server_record_mac; + cbmc_populate_s2n_hmac_state(&(server_record_mac)); + /* __CPROVER_assume(s2n_result_is_ok(s2n_hmac_state_validate(&(server_record_mac)))); */ + /* __CPROVER_file_local_s2n_hash_c_s2n_hash_set_impl(&(server_record_mac)); */ + + struct s2n_stuffer *conn_out = cbmc_allocate_s2n_stuffer(); + /* __CPROVER_assume(s2n_result_is_ok(s2n_stuffer_validate(conn_out))); */ + + if(conn) { + conn->out = *conn_out; + /* initial */ + conn->initial = malloc(sizeof(*(conn->initial))); + if(conn->initial) { + conn->initial->client_record_mac = client_record_mac; + conn->initial->server_record_mac = server_record_mac; + } + + /* client */ + conn->client = malloc(sizeof(*(conn->client))); + if(conn->client) { + conn->client->client_record_mac = client_record_mac; + } + + /* server */ + conn->server = malloc(sizeof(*(conn->server))); + if(conn->server) { + conn->server->server_record_mac = server_record_mac; + } + + } + uint8_t content_type; + const struct iovec *in = malloc(sizeof(*in)); + size_t in_count; + uint32_t offs; + size_t to_write; + + /* Extra assumptions. */ + s2n_mem_init_nondet(); + + /* Initialize s2n_fips_mode nondetermistically. Check stub for + * details */ + s2n_fips_init(); + + /* Operation under verification. */ + s2n_record_writev(conn, content_type, in, in_count, offs, to_write); +} + +// clang-format on