CBMC: xGetSlotList (#32)

* Add CBMC proof for xGetSlotList.

source/core_pkcs11.c

@@ -73,10 +73,30 @@ CK_RV xGetSlotList( CK_SLOT_ID ** ppxSlotId,
                     CK_ULONG * pxSlotCount )
 {
     CK_RV xResult = CKR_OK;
-    CK_FUNCTION_LIST_PTR pxFunctionList;
+    CK_FUNCTION_LIST_PTR pxFunctionList = NULL;
     CK_SLOT_ID * pxSlotId = NULL;
 
-    xResult = C_GetFunctionList( &pxFunctionList );
+    if( ( ppxSlotId == NULL ) || ( pxSlotCount == NULL ) )
+    {
+        xResult = CKR_ARGUMENTS_BAD;
+    }
+    else
+    {
+        xResult = C_GetFunctionList( &pxFunctionList );
+
+        if( pxFunctionList == NULL )
+        {
+            xResult = CKR_FUNCTION_FAILED;
+        }
+        else if( pxFunctionList->C_GetSlotList == NULL )
+        {
+            xResult = CKR_FUNCTION_FAILED;
+        }
+        else
+        {
+            /* MISRA */
+        }
+    }
 
     if( xResult == CKR_OK )
     {

test/cbmc/proofs/Makefile-project-defines

@@ -29,6 +29,8 @@ COMPILE_FLAGS += -std=gnu90
 #
 # INCLUDES =
 INCLUDES += -I$(SRCDIR)/source/include
+INCLUDES += -I$(SRCDIR)/3rdparty/pkcs11
+INCLUDES += -I$(CBMC_ROOT)/proofs/config
 
 # Preprocessor definitions -D...
 # DEFINES =

test/cbmc/proofs/config/core_pkcs11_config.h

@@ -0,0 +1,164 @@
+/*
+ * FreeRTOS V202007.00
+ * 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 aws_pkcs11_config.h
+ * @brief PCKS#11 config options.
+ */
+
+
+#ifndef _AWS_PKCS11_CONFIG_H_
+#define _AWS_PKCS11_CONFIG_H_
+
+/*
+ * @brief define away log macros.
+ */
+#ifndef LogError
+    #define LogError( message )
+#endif
+
+#ifndef LogWarn
+    #define LogWarn( message )
+#endif
+
+#ifndef LogInfo
+    #define LogInfo( message )
+#endif
+
+#ifndef LogDebug
+    #define LogDebug( message )
+#endif
+
+/**
+ * @brief Malloc API used by core_pkcs11.h
+ */
+#define PKCS11_MALLOC    malloc
+
+/**
+ * @brief Free API used by core_pkcs11.h
+ */
+#define PKCS11_FREE      free
+
+
+/**
+ * @brief PKCS #11 default user PIN.
+ *
+ * The PKCS #11 standard specifies the presence of a user PIN. That feature is
+ * sensible for applications that have an interactive user interface and memory
+ * protections. However, since typical microcontroller applications lack one or
+ * both of those, the user PIN is assumed to be used herein for interoperability
+ * purposes only, and not as a security feature.
+ */
+#define configPKCS11_DEFAULT_USER_PIN                      "0000"
+
+/**
+ * @brief Maximum length (in characters) for a PKCS #11 CKA_LABEL
+ * attribute.
+ */
+#define pkcs11configMAX_LABEL_LENGTH                       32
+
+/**
+ * @brief Maximum number of token objects that can be stored
+ * by the PKCS #11 module.
+ */
+#define pkcs11configMAX_NUM_OBJECTS                        6
+
+/**
+ * @brief Maximum number of sessions that can be stored
+ * by the PKCS #11 module.
+ */
+#define pkcs11configMAX_SESSIONS                           10
+
+/**
+ * @brief Set to 1 if a PAL destroy object is implemented.
+ *
+ * If set to 0, no PAL destroy object is implemented, and this functionality
+ * is implemented in the common PKCS #11 layer.
+ */
+#define pkcs11configPAL_DESTROY_SUPPORTED                  0
+
+/**
+ * @brief Set to 1 if OTA image verification via PKCS #11 module is supported.
+ *
+ * If set to 0, OTA code signing certificate is built in via
+ * aws_ota_codesigner_certificate.h.
+ */
+#define pkcs11configOTA_SUPPORTED                          0
+
+/**
+ * @brief Set to 1 if PAL supports storage for JITP certificate,
+ * code verify certificate, and trusted server root certificate.
+ *
+ * If set to 0, PAL does not support storage mechanism for these, and
+ * they are accessed via headers compiled into the code.
+ */
+#define pkcs11configJITP_CODEVERIFY_ROOT_CERT_SUPPORTED    0
+
+/**
+ * @brief The PKCS #11 label for device private key.
+ *
+ * Private key for connection to AWS IoT endpoint.  The corresponding
+ * public key should be registered with the AWS IoT endpoint.
+ */
+#define pkcs11configLABEL_DEVICE_PRIVATE_KEY_FOR_TLS       "Device Priv TLS Key"
+
+/**
+ * @brief The PKCS #11 label for device public key.
+ *
+ * The public key corresponding to pkcs11configLABEL_DEVICE_PRIVATE_KEY_FOR_TLS.
+ */
+#define pkcs11configLABEL_DEVICE_PUBLIC_KEY_FOR_TLS        "Device Pub TLS Key"
+
+/**
+ * @brief The PKCS #11 label for the device certificate.
+ *
+ * Device certificate corresponding to pkcs11configLABEL_DEVICE_PRIVATE_KEY_FOR_TLS.
+ */
+#define pkcs11configLABEL_DEVICE_CERTIFICATE_FOR_TLS       "Device Cert"
+
+/**
+ * @brief The PKCS #11 label for the object to be used for code verification.
+ *
+ * Used by over-the-air update code to verify an incoming signed image.
+ */
+#define pkcs11configLABEL_CODE_VERIFICATION_KEY            "Code Verify Key"
+
+/**
+ * @brief The PKCS #11 label for Just-In-Time-Provisioning.
+ *
+ * The certificate corresponding to the issuer of the device certificate
+ * (pkcs11configLABEL_DEVICE_CERTIFICATE_FOR_TLS) when using the JITR or
+ * JITP flow.
+ */
+#define pkcs11configLABEL_JITP_CERTIFICATE                 "JITP Cert"
+
+/**
+ * @brief The PKCS #11 label for the AWS Trusted Root Certificate.
+ *
+ * @see aws_default_root_certificates.h
+ */
+#define pkcs11configLABEL_ROOT_CERTIFICATE                 "Root Cert"
+
+#endif /* _AWS_PKCS11_CONFIG_H_ include guard. */

test/cbmc/proofs/xGetSlotList/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 = xGetSlotList_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 = xGetSlotList
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/source/core_pkcs11.c
+
+include ../Makefile.common

test/cbmc/proofs/xGetSlotList/README.md

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

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

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

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

test/cbmc/proofs/xGetSlotList/xGetSlotList_harness.c

@@ -0,0 +1,44 @@
+/*
+ * 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 xGetSlotList_harness.c
+ * @brief Implements the proof harness for xGetSlotList function.
+ */
+#include "core_pkcs11.h"
+
+void harness()
+{
+    CK_SLOT_ID * pxSlotId;
+    CK_ULONG xSlotCount;
+    CK_RV xResult;
+
+    xResult = xGetSlotList( &pxSlotId, &xSlotCount );
+
+    if( xResult == CKR_OK )
+    {
+        __CPROVER_assert( xSlotCount == 1, "Expected a slot count of one. This library currently only supports 1 slot." );
+    }
+}

test/unit-test/core_pkcs11_utest.c

@@ -361,11 +361,11 @@ void test_IotPkcs11_xGetSlotListBadFunctionList( void )
     CK_SLOT_ID_PTR pxSlotId = NULL;
     CK_ULONG xSlotCount = 0;
 
-    C_GetFunctionList_IgnoreAndReturn( CKR_ARGUMENTS_BAD );
+    C_GetFunctionList_IgnoreAndReturn( CKR_FUNCTION_FAILED );
     mock_osal_malloc_IgnoreAndReturn( NULL );
     xResult = xGetSlotList( &pxSlotId, &xSlotCount );
 
-    TEST_ASSERT_EQUAL( CKR_ARGUMENTS_BAD, xResult );
+    TEST_ASSERT_EQUAL( CKR_FUNCTION_FAILED, xResult );
 }
 
 /*!
@@ -379,11 +379,11 @@ void test_IotPkcs11_xGetSlotListBadSlotList( void )
     CK_ULONG xSlotCount = 0;
 
     vCommonStubs();
-    C_GetSlotList_IgnoreAndReturn( CKR_ARGUMENTS_BAD );
+    C_GetSlotList_IgnoreAndReturn( CKR_FUNCTION_FAILED );
     mock_osal_malloc_IgnoreAndReturn( NULL );
     xResult = xGetSlotList( &pxSlotId, &xSlotCount );
 
-    TEST_ASSERT_EQUAL( CKR_ARGUMENTS_BAD, xResult );
+    TEST_ASSERT_EQUAL( CKR_FUNCTION_FAILED, xResult );
 }
 
 /*!