Add CBMC proof of base64Decode function (#268)

* Add CBMC-proofs infrastructure * Add CBMC-proofs infrastructure (#242) * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Update ci.yml * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Addition to CBMC infrastructure (#243) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace Co-authored-by: Aniruddha Kanhere <[email protected]> * Added CBMC proof of setDataInterface function (#245) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for setDataInterface function * removed unnecessary variables * Updated documentation * Uncrustified * Updated year in copyright notice Co-authored-by: Aniruddha Kanhere <[email protected]> * Added template inside proof directory * Added CBMC proof of OTA_HTTP_strerror function (#252) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Add CBMC proof of OTA_HTTP_strerror function * Removed extra line and updated error log * Updated error log Co-authored-by: Aniruddha Kanhere <[email protected]> * Add CBMC proofs for RequestdataBlock_Http function (#248) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC Proof of requestDataBlock_Http function * Removed extra line * Update Comments Co-authored-by: Aniruddha Kanhere <[email protected]> * Added CBMC proofs for OTA_MQTT_strerror function (#247) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for OTA_MQTT_strerror function * Removed extra line * Updated comments * Fixed formatting errors * Updated error log Co-authored-by: Aniruddha Kanhere <[email protected]> * Added CBMC proofs for setControlInterface function (#246) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for setControlInterface function * Removed extra line * Added macro for the function * Fix formating errors * Fix spell check errors * Added preprocessor definition for setControlInterface function Co-authored-by: Aniruddha Kanhere <[email protected]> * removed extra line * Uncrustified' * CBMC Proof of initFileTransfer_Http function (#249) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Add CBMC proof of initFileTransfer_Http function * Removed extra line * Updated Comments * Updated error log and comments * Updated comments * Fix formatting errors Co-authored-by: Aniruddha Kanhere <[email protected]> * CBMC proof of decodeFileBlock_Http function (#250) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for decodeFileBlock_Http function * Removed extra line * Updated Comments * Fix formatting errors * Updated comments * Fix spell check error * Updated comments * Fix spell check errors * Updated arugments to malloc * updated the datatype in malloc argument Co-authored-by: Aniruddha Kanhere <[email protected]> * Added CBMC proof of CleanupData_Http function (#251) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for cleanupData_Http function * removed extra line * Updated Comments * Fixed formatting errors * Update error log * Updated comments Co-authored-by: Aniruddha Kanhere <[email protected]> * Added CBMC proof for stringBuilderUInt32Hex function (#253) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * added CBMC-proof files * Added Unwinding flag * Updated buffer initialization * Fixed spell check and formatting errorst * Updated comments * Added loop unwinding * Updated comments * Fix formatting errors * Added comment * updated the arguments to malloc * Updated comments Co-authored-by: Joshua Yan <[email protected]> * Updated comments Co-authored-by: Aniruddha Kanhere <[email protected]> Co-authored-by: Joshua Yan <[email protected]> * Added CBMC proof of stringBuilderUInt32Decimal function (#254) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Add CBMC-proof files for stringBuilderUInt32Decimal * Fixed spell check and formatting errors * Updated Comments * Add loop unwinding * Updated comments * Updated comments * Updated spellings * updated arguments to the malloc Co-authored-by: Aniruddha Kanhere <[email protected]> * Add CBMC proofs for base64Decode function * Update doxygen in cbmc-proof branch (#275) * Add assert checks for http interface functions (#231) * Add assert checks for http interface functions * Uncrustified * Added spaces in assertion arguments Co-authored-by: Prasad Vyawahare <[email protected]> * Adding a Pull request template (#239) * Adding a Pull request template * Exclude .github from formatting check * Applying PR feedback * Update doxygen version to 1.9.2 (#274) Co-authored-by: Prasad Vyawahare <[email protected]> Co-authored-by: Shubham Divekar <[email protected]> Co-authored-by: Archit Gupta <[email protected]> * Free dynamic allocated variables * Updated comment * Updated comments Co-authored-by: Aniruddha Kanhere <[email protected]> Co-authored-by: Joshua Yan <[email protected]> Co-authored-by: Prasad Vyawahare <[email protected]> Co-authored-by: Shubham Divekar <[email protected]> Co-authored-by: Archit Gupta <[email protected]>
aws · Sep 9, 2021 · c42a16c · c42a16c
1 parent f9e1168
commit c42a16c
Show file tree

Hide file tree

Showing 5 changed files with 143 additions and 0 deletions.
diff --git a/test/cbmc/proofs/base64Decode/Makefile b/test/cbmc/proofs/base64Decode/Makefile
@@ -0,0 +1,26 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY = base64Decode_harness
+HARNESS_FILE = $(HARNESS_ENTRY)
+
+# 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 = base64Decode
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET += base64Decode.0:400
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/source/ota_base64.c
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+include ../Makefile.common
diff --git a/test/cbmc/proofs/base64Decode/README.md b/test/cbmc/proofs/base64Decode/README.md
@@ -0,0 +1,20 @@
+base64Decode proof
+==============
+
+This directory contains a memory safety proof for base64Decode.
+
+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`).
diff --git a/test/cbmc/proofs/base64Decode/base64Decode_harness.c b/test/cbmc/proofs/base64Decode/base64Decode_harness.c
@@ -0,0 +1,89 @@
+/* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. */
+/* SPDX-License-Identifier: Apache-2.0 */
+
+/**
+ * @file base64Decode_harness.c
+ * @brief Implements the proof harness for base64Decode function.
+ */
+/* Include headers for base64 decoding. */
+#include "ota_base64_private.h"
+#include <stdlib.h>
+
+#define VALID_BASE64_SYMBOL_INDEX_RANGE_MAX    63U
+
+/* Maximum size of the decode buffer for storing the PEM signature. */
+#define MAX_DECODE_BUFFER_SIZE                 256
+
+/* For every 3 bytes in the decode there are 4 bytes in the encode buffer. The
+ * maximum size of the encode buffer is 4/3 times the decode buffer. */
+#define MAX_ENCODE_BUFFER_SIZE                 344
+
+/* Returns the number of whitespace and padding in the encoded buffer. */
+Base64Status_t __CPROVER_file_local_ota_base64_c_preprocessBase64Index( uint8_t base64Index,
+                                                                        int64_t * pNumPadding,
+                                                                        int64_t * pNumWhitespace )
+{
+    Base64Status_t status;
+
+    return status;
+}
+
+/* updates the number of valid symbol in the decoding buffer. */
+void __CPROVER_file_local_ota_base64_c_updateBase64DecodingBuffer( const uint8_t base64Index,
+                                                                   uint32_t * pBase64IndexBuffer,
+                                                                   uint32_t * pNumDataInBuffer )
+{
+    uint32_t numDataInBuffer = *pNumDataInBuffer;
+
+    /* Increment the number of valid symbols present in the index buffer. */
+    if( base64Index <= VALID_BASE64_SYMBOL_INDEX_RANGE_MAX )
+    {
+        numDataInBuffer++;
+    }
+
+    *pNumDataInBuffer = numDataInBuffer;
+}
+
+/* This functions decodes every 4 bytes of encoded data. */
+Base64Status_t __CPROVER_file_local_ota_base64_c_decodeBase64IndexBuffer( uint32_t * pBase64IndexBuffer,
+                                                                          uint32_t * pNumDataInBuffer,
+                                                                          uint8_t * pDest,
+                                                                          const size_t destLen,
+                                                                          size_t * pOutputLen )
+{
+    Base64Status_t status;
+
+    /* After decoding, Reset the number of valid bytes present in the decoding Buffer. */
+    *pNumDataInBuffer = 0;
+
+    return status;
+}
+
+void base64Decode_harness()
+{
+    uint8_t * pDest;
+    size_t destLen;
+    size_t * pResultLen;
+    uint8_t * pEncodedData;
+    size_t encodedLen;
+
+    size_t resultLen;
+
+    /* The base64Decode function is used to decode the PEM signature and
+     * the maximum size of the decoded signature is 256. This limit is set
+     * to limit loop unwinding in the base64Decode function. */
+    __CPROVER_assume( destLen <= MAX_DECODE_BUFFER_SIZE );
+
+    /* This limit is set to limit loop unwinding in the base64Decode function.   */
+    __CPROVER_assume( encodedLen <= MAX_ENCODE_BUFFER_SIZE );
+
+    pDest = ( uint8_t * ) malloc( destLen * sizeof( uint8_t ) );
+    pEncodedData = ( uint8_t * ) malloc( encodedLen * sizeof( uint8_t ) );
+
+    pResultLen = &resultLen;
+
+    ( void ) base64Decode( pDest, destLen, pResultLen, pEncodedData, encodedLen );
+
+    free( pDest );
+    free( pEncodedData );
+}
diff --git a/test/cbmc/proofs/base64Decode/cbmc-proof.txt b/test/cbmc/proofs/base64Decode/cbmc-proof.txt
@@ -0,0 +1,2 @@
+# This file marks this directory as containing a CBMC proof.
+# This file is required by the run-cbmc-proofs.py to differentiate between a proof directory from a normal directory.
diff --git a/test/cbmc/proofs/base64Decode/cbmc-viewer.json b/test/cbmc/proofs/base64Decode/cbmc-viewer.json
@@ -0,0 +1,6 @@
+{ "expected-missing-functions":
+  [
+  ],
+  "proof-name": "base64Decode",
+  "proof-root": "test/cbmc/proofs"
+}
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		# This file marks this directory as containing a CBMC proof.
		# This file is required by the run-cbmc-proofs.py to differentiate between a proof directory from a normal directory.