Setup proof infrastructure for CBMC (#7)

* Add Litani and templates for CBMC

* Add sample proof

* Implement CBMC proof for SigV4_AwsIotDateToIso8601

* Unwind all loops such that no unwinding errors occur

.gitmodules

@@ -1,3 +1,9 @@
 [submodule "test/unit-test/CMock"]
 	path = test/unit-test/CMock
 	url = https://github.com/ThrowTheSwitch/CMock.git
+[submodule "test/cbmc/aws-templates-for-cbmc-proofs"]
+	path = test/cbmc/aws-templates-for-cbmc-proofs
+	url = [email protected]:awslabs/aws-templates-for-cbmc-proofs.git
+[submodule "test/cbmc/litani"]
+	path = test/cbmc/litani
+	url = https://github.com/awslabs/aws-build-accumulator

test/cbmc/.gitignore

@@ -0,0 +1,23 @@
+# Emitted when running CBMC proofs
+proofs/**/logs
+proofs/**/gotos
+proofs/**/report
+proofs/**/html
+
+# Emitted by CBMC Viewer
+TAGS-*
+
+# Emitted by Arpa
+arpa_cmake/
+arpa-validation-logs/
+Makefile.arpa
+
+# Emitted by litani
+.ninja_deps
+.ninja_log
+.litani_cache_dir
+
+# These files should be overwritten whenever prepare.py runs
+cbmc-batch.yaml
+
+__pycache__/

test/cbmc/include/README.md

@@ -0,0 +1 @@
+../aws-templates-for-cbmc-proofs/template-for-repository/include/README.md

test/cbmc/negative_tests/README.md

@@ -0,0 +1 @@
+../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/README.md

test/cbmc/negative_tests/assert/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/assert/Makefile

test/cbmc/negative_tests/assert/assert_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/assert/assert_harness.c

test/cbmc/negative_tests/bounds_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/bounds_check/Makefile

test/cbmc/negative_tests/bounds_check/bounds_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/bounds_check/bounds_check_harness.c

test/cbmc/negative_tests/conversion_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/conversion_check/Makefile

test/cbmc/negative_tests/conversion_check/conversion_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/conversion_check/conversion_check_harness.c

test/cbmc/negative_tests/div_by_zero_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/div_by_zero_check/Makefile

test/cbmc/negative_tests/div_by_zero_check/div_by_zero_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/div_by_zero_check/div_by_zero_check_harness.c

test/cbmc/negative_tests/float_overflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_overflow_check/Makefile

test/cbmc/negative_tests/float_overflow_check/float_overflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_overflow_check/float_overflow_check_harness.c

test/cbmc/negative_tests/float_underflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_underflow_check/Makefile

test/cbmc/negative_tests/float_underflow_check/float_underflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/float_underflow_check/float_underflow_check_harness.c

test/cbmc/negative_tests/nan_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/nan_check/Makefile

test/cbmc/negative_tests/nan_check/nan_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/nan_check/nan_check_harness.c

test/cbmc/negative_tests/pointer_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_check/Makefile

test/cbmc/negative_tests/pointer_check/pointer_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_check/pointer_check_harness.c

test/cbmc/negative_tests/pointer_overflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_overflow_check/Makefile

test/cbmc/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_overflow_check/pointer_overflow_check_harness.c

test/cbmc/negative_tests/pointer_primitive_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_primitive_check/Makefile

test/cbmc/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_primitive_check/pointer_primitive_check_harness.c

test/cbmc/negative_tests/pointer_underflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_underflow_check/Makefile

test/cbmc/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/pointer_underflow_check/pointer_underflow_check_harness.c

test/cbmc/negative_tests/signed_overflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_overflow_check/Makefile

test/cbmc/negative_tests/signed_overflow_check/signed_overflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_overflow_check/signed_overflow_check_harness.c

test/cbmc/negative_tests/signed_underflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_underflow_check/Makefile

test/cbmc/negative_tests/signed_underflow_check/signed_underflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/signed_underflow_check/signed_underflow_check_harness.c

test/cbmc/negative_tests/undefined_shift_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/undefined_shift_check/Makefile

test/cbmc/negative_tests/undefined_shift_check/undefined_shift_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/undefined_shift_check/undefined_shift_check_harness.c

test/cbmc/negative_tests/unsigned_overflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_overflow_check/Makefile

test/cbmc/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_overflow_check/unsigned_overflow_check_harness.c

test/cbmc/negative_tests/unsigned_underflow_check/Makefile

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_underflow_check/Makefile

test/cbmc/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c

@@ -0,0 +1 @@
+../../aws-templates-for-cbmc-proofs/template-for-repository/negative_tests/unsigned_underflow_check/unsigned_underflow_check_harness.c

test/cbmc/proofs/Makefile-project-defines

@@ -0,0 +1,42 @@
+# -*- 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: Apache-2.0
+
+################################################################
+# Use this file to give project-specific definitions of the command
+# line arguments to pass to CBMC tools like goto-cc to build the goto
+# binaries and cbmc to do the property and coverage checking.
+#
+# Use this file to override most default definitions of variables in
+# Makefile.common.
+################################################################
+
+# Flags to pass to goto-cc for compilation (typically those passed to gcc -c)
+# COMPILE_FLAGS =
+COMPILE_FLAGS += -fPIC
+COMPILE_FLAGS += -std=gnu90
+
+# Flags to pass to goto-cc for linking (typically those passed to gcc)
+# LINK_FLAGS =
+
+# Preprocessor include paths -I...
+# Consider adding
+#     INCLUDES += -I$(CBMC_ROOT)/include
+# You will want to decide what order that comes in relative to the other
+# include directories in your project.
+#
+# INCLUDES =
+INCLUDES += -I$(SRCDIR)/test/cbmc/include
+INCLUDES += -I$(SRCDIR)/source/include
+
+# Preprocessor definitions -D...
+# DEFINES =
+DEFINES += -DSIGV4_DO_NOT_USE_CUSTOM_CONFIG=1
+
+# Path to arpa executable
+# ARPA =
+
+# Flags to pass to cmake for building the project
+# ARPA_CMAKE_FLAGS =

test/cbmc/proofs/Makefile-project-targets

@@ -0,0 +1,10 @@
+# -*- 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: Apache-2.0
+
+################################################################
+# Use this file to give project-specific targets, including targets
+# that may depend on targets defined in Makefile.common.
+################################################################

test/cbmc/proofs/Makefile-project-testing

@@ -0,0 +1,11 @@
+# -*- 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: Apache-2.0
+
+################################################################
+# Use this file to define project-specific targets and definitions for
+# unit testing or continuous integration that may depend on targets
+# defined in Makefile.common
+################################################################

test/cbmc/proofs/Makefile-template-defines

@@ -0,0 +1,19 @@
+PROOF_ROOT ?= $(abspath .)
+
+# Absolute path to the root of the source tree.
+#
+SRCDIR ?= $(abspath $(PROOF_ROOT)/../../..)
+
+
+# Absolute path to the litani script.
+#
+LITANI ?= $(abspath $(PROOF_ROOT)/../litani/litani)
+
+
+# Name of this proof project, displayed in proof reports. For example,
+# "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots,
+# this may be overridden on the command-line to Make, for example
+#
+# 	  make PROJECT_NAME="FreeRTOS MQTT" report
+#
+PROJECT_NAME = "sigv4-for-aws-iot-embedded-sdk"

test/cbmc/proofs/Makefile.common

@@ -0,0 +1 @@
+../aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common

test/cbmc/proofs/README.md

@@ -0,0 +1 @@
+../aws-templates-for-cbmc-proofs/template-for-repository/proofs/README.md

test/cbmc/proofs/SigV4_AwsIotDateToIso8601/Makefile

@@ -0,0 +1,29 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = SigV4_AwsIotDateToIso8601_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = SigV4_AwsIotDateToIso8601
+
+DEFINES +=
+INCLUDES +=
+
+MONTH_ASCII_LEN=3
+ISO_YEAR_LEN=4
+MONTHS_IN_YEAR=12
+FORMAT_RFC_5322_LEN=32
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += __CPROVER_file_local_sigv4_c_parseDate.0:$(FORMAT_RFC_5322_LEN)
+UNWINDSET += __CPROVER_file_local_sigv4_c_scanValue.0:$(MONTHS_IN_YEAR)
+UNWINDSET += __CPROVER_file_local_sigv4_c_scanValue.1:$(ISO_YEAR_LEN)
+UNWINDSET += __CPROVER_file_local_sigv4_c_intToAscii.0:$(ISO_YEAR_LEN)
+UNWINDSET += strncmp.0:$(MONTH_ASCII_LEN)
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/source/sigv4.c
+
+include ../Makefile.common

test/cbmc/proofs/SigV4_AwsIotDateToIso8601/README.md

@@ -0,0 +1,20 @@
+SigV4_AwsIotDateToIso8601 proof
+==============
+
+This directory contains a memory safety proof for SigV4_AwsIotDateToIso8601.
+
+To run the proof.
+-------------
+
+* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
+  to your path.
+* Run `make`.
+* Open html/index.html in a web browser.
+
+To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles.
+-------------
+
+* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof.
+* Use Makefile.arpa as the starting point for your proof Makefile by:
+  1. Modifying Makefile.arpa (if required).
+  2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`).

test/cbmc/proofs/SigV4_AwsIotDateToIso8601/SigV4_AwsIotDateToIso8601_harness.c

@@ -0,0 +1,45 @@
+/*
+ * SigV4 Utility Library v1.0.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/**
+ * @file SigV4_AwsIotDateToIso8601_harness.c
+ * @brief Implements the proof harness for SigV4_AwsIotDateToIso8601 function.
+ */
+
+/* Include paths for public enums, structures, and macros. */
+#include "sigv4.h"
+
+void harness()
+{
+    char * pInputDate;
+    size_t dateLen;
+    char * pDateISO8601;
+    size_t dateISO8601Len;
+
+    __CPROVER_assume( dateLen == SIGV4_EXPECTED_LEN_RFC_3339 || dateLen == SIGV4_EXPECTED_LEN_RFC_5322 || dateLen == 0 );
+    pInputDate = malloc( dateLen );
+
+    __CPROVER_assume( dateISO8601Len < CBMC_MAX_OBJECT_SIZE );
+    pDateISO8601 = malloc( dateISO8601Len );
+
+    SigV4_AwsIotDateToIso8601( pInputDate, dateLen, pDateISO8601, dateISO8601Len );
+}

test/cbmc/proofs/SigV4_AwsIotDateToIso8601/cbmc-proof.txt

@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.

test/cbmc/proofs/SigV4_AwsIotDateToIso8601/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "SigV4_AwsIotDateToIso8601",
+  "proof-root": "test/cbmc/proofs"
+}

test/cbmc/proofs/prepare.py

@@ -0,0 +1 @@
+../aws-templates-for-cbmc-proofs/template-for-repository/proofs/prepare.py