Added a proof for PKI_pkcs11SignatureTombedTLS. (#31)

* Added a proof for PKI_pkcs11SignatureTombedTLS.

source/core_pki_utils.c

@@ -160,6 +160,7 @@ int8_t PKI_pkcs11SignatureTombedTLSSignature( uint8_t * pucSig,
         pucSig[ 0 ] = 0x30; /* Sequence. */
         pucSig[ 1 ] = 0x44; /* The minimum length the signature could be. */
         pucSig[ 2 ] = 0x02; /* Integer. */
+        *pxSigLen = 0;      /* Set signature length output to 0. */
 
         /*************** R Component. *******************/
 
@@ -169,13 +170,15 @@ int8_t PKI_pkcs11SignatureTombedTLSSignature( uint8_t * pucSig,
         {
             pucSig[ 1 ]++;                               /* Increment the length of the structure to account for the 0x00 pad. */
             pucSig[ 3 ] = 0x21;                          /* Increment the length of the R value to account for the 0x00 pad. */
+            *pxSigLen += 0x21;                           /* Add R length to the signature length. */
             pucSig[ 4 ] = 0x0;                           /* Write the 0x00 pad. */
             ( void ) memcpy( &pucSig[ 5 ], ucTemp, 32 ); /* Copy the 32-byte R value. */
             pucSigPtr = pucSig + 33;                     /* Increment the pointer to compensate for padded R length.    */
         }
         else
         {
             pucSig[ 3 ] = 0x20;                          /* R length with be 32 bytes. */
+            *pxSigLen += 0x20;                           /* Add R length to the signature length. */
             ( void ) memcpy( &pucSig[ 4 ], ucTemp, 32 ); /* Copy 32 bytes of R into the signature buffer. */
             pucSigPtr = pucSig + 32;                     /* Increment the pointer for 32 byte R length. */
         }
@@ -192,6 +195,7 @@ int8_t PKI_pkcs11SignatureTombedTLSSignature( uint8_t * pucSig,
         {
             pucSig[ 1 ]++;                                   /* Increment the length of the structure to account for the 0x00 pad. */
             pucSigPtr[ 0 ] = 0x21;                           /* Increment the length of the S value to account for the 0x00 pad. */
+            *pxSigLen += 0x21;                               /* Add S length to the signature length. */
             pucSigPtr[ 1 ] = 0x00;                           /* Write the 0x00 pad. */
             pucSigPtr += 2;                                  /* pucSigPtr was pointing at the S-length.  Increment by 2 to hop over length and 0 padding. */
 
@@ -200,13 +204,19 @@ int8_t PKI_pkcs11SignatureTombedTLSSignature( uint8_t * pucSig,
         else
         {
             pucSigPtr[ 0 ] = 0x20;                           /* S length will be 32 bytes. */
+            *pxSigLen += 0x20;                               /* Add S length to the signature length. */
             pucSigPtr++;                                     /* Hop pointer over the length byte. */
             ( void ) memcpy( pucSigPtr, &ucTemp[ 32 ], 32 ); /* Copy the S value. */
         }
 
         /* The total signature length is the length of the R and S integers plus 2 bytes for
          * the SEQUENCE and LENGTH wrapping the entire struct. */
-        *pxSigLen = pucSig[ 1 ] + 2UL;
+        *pxSigLen += 2UL;
+
+        if( *pxSigLen >= 72 )
+        {
+            xReturn = FAILURE;
+        }
     }
 
     return xReturn;

test/cbmc/proofs/PKI_pkcs11SignatureTombedTLSSignature/Makefile

@@ -0,0 +1,20 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = PKI_pkcs11SignatureTombedTLSSignature_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 = PKI_pkcs11SignatureTombedTLSSignature
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/source/core_pki_utils.c
+
+include ../Makefile.common

test/cbmc/proofs/PKI_pkcs11SignatureTombedTLSSignature/PKI_pkcs11SignatureTombedTLSSignature_harness.c

@@ -0,0 +1,51 @@
+/*
+ * corePKCS11 V2.0.0
+ * Copyright (C) 2020 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.
+ *
+ * http://aws.amazon.com/freertos
+ * http://www.FreeRTOS.org
+ */
+
+/**
+ * @file PKI_pkcs11SignatureTombedTLSSignature_harness.c
+ * @brief Implements the proof harness for PKI_pkcs11SignatureTombedTLSSignature function.
+ */
+
+#include "core_pki_utils.h"
+
+void harness()
+{
+    int8_t ucReturn;
+    uint8_t * pucSig;
+    uint32_t ulSigLen;
+    size_t ulReturnLen;
+
+    __CPROVER_assume( ulSigLen == 72 );
+    pucSig = malloc( ulSigLen * sizeof( uint8_t ) );
+
+    ucReturn = PKI_pkcs11SignatureTombedTLSSignature( pucSig, &ulReturnLen );
+
+    if( ucReturn != -1 )
+    {
+        __CPROVER_assert( ulReturnLen <= 72, "The signature was larger than expected." );
+    }
+
+    free( pucSig );
+}

test/cbmc/proofs/PKI_pkcs11SignatureTombedTLSSignature/README.md

@@ -0,0 +1,20 @@
+PKI_pkcs11SignatureTombedTLSSignature proof
+==============
+
+This directory contains a memory safety proof for PKI_pkcs11SignatureTombedTLSSignature.
+
+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/PKI_pkcs11SignatureTombedTLSSignature/cbmc-proof.txt

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

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

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