From 3671f86ea8138f4eddbdbb2775e8bf827b2ff4d1 Mon Sep 17 00:00:00 2001 From: Carl Lundin <53273776+lundinc2@users.noreply.github.com> Date: Tue, 10 Nov 2020 10:45:46 -0800 Subject: [PATCH] CBMC: xGetSlotList (#32) * Add CBMC proof for xGetSlotList. --- source/core_pkcs11.c | 24 ++- test/cbmc/proofs/Makefile-project-defines | 2 + test/cbmc/proofs/config/core_pkcs11_config.h | 164 ++++++++++++++++++ test/cbmc/proofs/xGetSlotList/Makefile | 20 +++ test/cbmc/proofs/xGetSlotList/README.md | 20 +++ test/cbmc/proofs/xGetSlotList/cbmc-proof.txt | 1 + .../cbmc/proofs/xGetSlotList/cbmc-viewer.json | 7 + .../xGetSlotList/xGetSlotList_harness.c | 44 +++++ test/unit-test/core_pkcs11_utest.c | 8 +- 9 files changed, 284 insertions(+), 6 deletions(-) create mode 100644 test/cbmc/proofs/config/core_pkcs11_config.h create mode 100644 test/cbmc/proofs/xGetSlotList/Makefile create mode 100644 test/cbmc/proofs/xGetSlotList/README.md create mode 100644 test/cbmc/proofs/xGetSlotList/cbmc-proof.txt create mode 100644 test/cbmc/proofs/xGetSlotList/cbmc-viewer.json create mode 100644 test/cbmc/proofs/xGetSlotList/xGetSlotList_harness.c diff --git a/source/core_pkcs11.c b/source/core_pkcs11.c index a58cac2b..aa41332f 100644 --- a/source/core_pkcs11.c +++ b/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 ) { diff --git a/test/cbmc/proofs/Makefile-project-defines b/test/cbmc/proofs/Makefile-project-defines index 8a267520..64808594 100644 --- a/test/cbmc/proofs/Makefile-project-defines +++ b/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 = diff --git a/test/cbmc/proofs/config/core_pkcs11_config.h b/test/cbmc/proofs/config/core_pkcs11_config.h new file mode 100644 index 00000000..4ab55e74 --- /dev/null +++ b/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. */ diff --git a/test/cbmc/proofs/xGetSlotList/Makefile b/test/cbmc/proofs/xGetSlotList/Makefile new file mode 100644 index 00000000..f5b79617 --- /dev/null +++ b/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 diff --git a/test/cbmc/proofs/xGetSlotList/README.md b/test/cbmc/proofs/xGetSlotList/README.md new file mode 100644 index 00000000..7bff0d47 --- /dev/null +++ b/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`). diff --git a/test/cbmc/proofs/xGetSlotList/cbmc-proof.txt b/test/cbmc/proofs/xGetSlotList/cbmc-proof.txt new file mode 100644 index 00000000..6ed46f12 --- /dev/null +++ b/test/cbmc/proofs/xGetSlotList/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/xGetSlotList/cbmc-viewer.json b/test/cbmc/proofs/xGetSlotList/cbmc-viewer.json new file mode 100644 index 00000000..8d0ada24 --- /dev/null +++ b/test/cbmc/proofs/xGetSlotList/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "xGetSlotList", + "proof-root": "test/cbmc/proofs" +} diff --git a/test/cbmc/proofs/xGetSlotList/xGetSlotList_harness.c b/test/cbmc/proofs/xGetSlotList/xGetSlotList_harness.c new file mode 100644 index 00000000..55b9c0fe --- /dev/null +++ b/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." ); + } +} diff --git a/test/unit-test/core_pkcs11_utest.c b/test/unit-test/core_pkcs11_utest.c index e9acb6ee..7840fd7e 100644 --- a/test/unit-test/core_pkcs11_utest.c +++ b/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 ); } /*!