diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f2915acc..87f7e8ab 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -261,8 +261,7 @@ jobs: - name: Set up CBMC runner uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main with: - cbmc_version: "5.61.0" - cbmc_viewer_version: "3.5" + cbmc_version: "6.3.1" - name: Install cmake run: | sudo apt-get install -y cmake diff --git a/source/core_pkcs11.c b/source/core_pkcs11.c index b22d8380..d8e2be40 100644 --- a/source/core_pkcs11.c +++ b/source/core_pkcs11.c @@ -30,6 +30,7 @@ /* C runtime includes. */ #include #include +#include #include /** diff --git a/test/cbmc/proofs/C_CloseSession/Makefile b/test/cbmc/proofs/C_CloseSession/Makefile index a0655f54..b28da18c 100644 --- a/test/cbmc/proofs/C_CloseSession/Makefile +++ b/test/cbmc/proofs/C_CloseSession/Makefile @@ -9,8 +9,8 @@ HARNESS_FILE = C_CloseSession_harness PROOF_UID = C_CloseSession DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += C_Finalize REMOVE_FUNCTION_BODY += C_GetFunctionList diff --git a/test/cbmc/proofs/C_CreateObject/Makefile b/test/cbmc/proofs/C_CreateObject/Makefile index cce61508..61c4600d 100644 --- a/test/cbmc/proofs/C_CreateObject/Makefile +++ b/test/cbmc/proofs/C_CreateObject/Makefile @@ -25,11 +25,14 @@ MAX_LABEL_SIZE=32 # Should be one more than the total number of objects in the PKCS stack. MAX_OBJECT_NUM=2 +CBMC_OBJECT_BITS = 9 + DEFINES += -DTEMPLATE_SIZE=$(TEMPLATE_SIZE) DEFINES += -DTEMPLATE_ATTRIBUTE_MAX_SIZE=$(TEMPLATE_ATTRIBUTE_MAX_SIZE) -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include +INCLUDES += -I$(SRCDIR)/source/portable/os REMOVE_FUNCTION_BODY += C_Initialize REMOVE_FUNCTION_BODY += C_Finalize @@ -61,5 +64,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c +PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c include ../Makefile.common diff --git a/test/cbmc/proofs/C_DestroyObject/Makefile b/test/cbmc/proofs/C_DestroyObject/Makefile index 31b6d1dc..849b2a1f 100644 --- a/test/cbmc/proofs/C_DestroyObject/Makefile +++ b/test/cbmc/proofs/C_DestroyObject/Makefile @@ -16,8 +16,8 @@ MAX_LABEL_SIZE=32 DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM) -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += C_Finalize REMOVE_FUNCTION_BODY += C_GetFunctionList diff --git a/test/cbmc/proofs/C_DigestFinal/Makefile b/test/cbmc/proofs/C_DigestFinal/Makefile index 3da4cd80..be737ee6 100644 --- a/test/cbmc/proofs/C_DigestFinal/Makefile +++ b/test/cbmc/proofs/C_DigestFinal/Makefile @@ -9,8 +9,8 @@ HARNESS_FILE = C_DigestFinal_harness PROOF_UID = C_DigestFinal DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += UNWINDSET += diff --git a/test/cbmc/proofs/C_DigestInit/Makefile b/test/cbmc/proofs/C_DigestInit/Makefile index 880396a3..e241eeff 100644 --- a/test/cbmc/proofs/C_DigestInit/Makefile +++ b/test/cbmc/proofs/C_DigestInit/Makefile @@ -9,8 +9,8 @@ HARNESS_FILE = C_DigestInit_harness PROOF_UID = C_DigestInit DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += UNWINDSET += diff --git a/test/cbmc/proofs/C_DigestUpdate/Makefile b/test/cbmc/proofs/C_DigestUpdate/Makefile index cbae7dbf..b9ac4e69 100644 --- a/test/cbmc/proofs/C_DigestUpdate/Makefile +++ b/test/cbmc/proofs/C_DigestUpdate/Makefile @@ -9,8 +9,8 @@ HARNESS_FILE = C_DigestUpdate_harness PROOF_UID = C_DigestUpdate DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += UNWINDSET += diff --git a/test/cbmc/proofs/C_Finalize/Makefile b/test/cbmc/proofs/C_Finalize/Makefile index 70be916e..4c7262ca 100644 --- a/test/cbmc/proofs/C_Finalize/Makefile +++ b/test/cbmc/proofs/C_Finalize/Makefile @@ -9,8 +9,8 @@ HARNESS_FILE = C_Finalize_harness PROOF_UID = C_Finalize DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += UNWINDSET += diff --git a/test/cbmc/proofs/C_FindObjects/Makefile b/test/cbmc/proofs/C_FindObjects/Makefile index 301c9543..6fdd5c98 100644 --- a/test/cbmc/proofs/C_FindObjects/Makefile +++ b/test/cbmc/proofs/C_FindObjects/Makefile @@ -9,14 +9,16 @@ HARNESS_FILE = C_FindObjects_harness PROOF_UID = C_FindObjects DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include +INCLUDES += -I$(SRCDIR)/source/portable/os REMOVE_FUNCTION_BODY += C_Finalize REMOVE_FUNCTION_BODY += C_GetFunctionList # This should be similar to the dummy data length in "core_pkcs11_pal_stubs.c" PKCS11_PAL_GetObjectValue UNWINDSET += __CPROVER_file_local_core_pkcs11_mbedtls_c_prvFindObjectInListByLabel.0:13 +UNWINDSET += strncmp.0:20 # This should align with the max object count configured in core_pkcs11_config.h UNWINDSET += __CPROVER_file_local_core_pkcs11_mbedtls_c_prvAddObjectToList.0:2 @@ -24,5 +26,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c +PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c +PROJECT_SOURCES += $(SRCDIR)/source/portable/os/core_pkcs11_pal_utils.c include ../Makefile.common diff --git a/test/cbmc/proofs/C_FindObjectsFinal/Makefile b/test/cbmc/proofs/C_FindObjectsFinal/Makefile index 7d86ad49..921467ec 100644 --- a/test/cbmc/proofs/C_FindObjectsFinal/Makefile +++ b/test/cbmc/proofs/C_FindObjectsFinal/Makefile @@ -9,8 +9,8 @@ HARNESS_FILE = C_FindObjectsFinal_harness PROOF_UID = C_FindObjectsFinal DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += UNWINDSET += diff --git a/test/cbmc/proofs/C_FindObjectsInit/Makefile b/test/cbmc/proofs/C_FindObjectsInit/Makefile index 297408a2..d4f8cab7 100644 --- a/test/cbmc/proofs/C_FindObjectsInit/Makefile +++ b/test/cbmc/proofs/C_FindObjectsInit/Makefile @@ -11,8 +11,8 @@ PROOF_UID = C_FindObjectsInit TEMPLATE_SIZE=10 DEFINES += -DTEMPLATE_SIZE=$(TEMPLATE_SIZE) -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += UNWINDSET += C_FindObjectsInit.0:$(TEMPLATE_SIZE) diff --git a/test/cbmc/proofs/C_GenerateKeyPair/Makefile b/test/cbmc/proofs/C_GenerateKeyPair/Makefile index ab342938..f5d36068 100644 --- a/test/cbmc/proofs/C_GenerateKeyPair/Makefile +++ b/test/cbmc/proofs/C_GenerateKeyPair/Makefile @@ -12,8 +12,9 @@ TEMPLATE_SIZE=10 DEFINES += -DTEMPLATE_SIZE=$(TEMPLATE_SIZE) -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include +INCLUDES += -I$(SRCDIR)/source/portable/os REMOVE_FUNCTION_BODY += C_Initialize REMOVE_FUNCTION_BODY += C_Finalize @@ -29,6 +30,7 @@ UNWINDSET += harness.0:10 UNWINDSET += harness.1:10 UNWINDSET += memcmp.0:32 UNWINDSET += memcpy.0:32 +UNWINDSET += strncmp.0:20 # The nested memcmp in this loop will exponentially increase the CBMC bounds checking. # Be very careful increasing this. At the time of writing this, the PKCS stack was @@ -42,5 +44,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c +PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c +PROJECT_SOURCES += $(SRCDIR)/source/portable/os/core_pkcs11_pal_utils.c include ../Makefile.common diff --git a/test/cbmc/proofs/C_GenerateRandom/Makefile b/test/cbmc/proofs/C_GenerateRandom/Makefile index 58f535de..fb7492e0 100644 --- a/test/cbmc/proofs/C_GenerateRandom/Makefile +++ b/test/cbmc/proofs/C_GenerateRandom/Makefile @@ -9,8 +9,8 @@ HARNESS_FILE = C_GenerateRandom_harness PROOF_UID = C_GenerateRandom DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += C_Initialize REMOVE_FUNCTION_BODY += __CPROVER_file_local_core_pkcs11_mbedtls_c_prvMbedTLS_Initialize diff --git a/test/cbmc/proofs/C_GetAttributeValue/Makefile b/test/cbmc/proofs/C_GetAttributeValue/Makefile index 854751b3..4710e4f1 100644 --- a/test/cbmc/proofs/C_GetAttributeValue/Makefile +++ b/test/cbmc/proofs/C_GetAttributeValue/Makefile @@ -20,8 +20,9 @@ MAX_OBJECT_NUM=2 DEFINES += -DTEMPLATE_SIZE=$(TEMPLATE_SIZE) DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM) -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include +INCLUDES += -I$(SRCDIR)/source/portable/os REMOVE_FUNCTION_BODY += @@ -37,5 +38,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c +PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c include ../Makefile.common diff --git a/test/cbmc/proofs/C_GetFunctionList/Makefile b/test/cbmc/proofs/C_GetFunctionList/Makefile index ac2a7d6e..937ffbe3 100644 --- a/test/cbmc/proofs/C_GetFunctionList/Makefile +++ b/test/cbmc/proofs/C_GetFunctionList/Makefile @@ -9,8 +9,8 @@ HARNESS_FILE = C_GetFunctionList_harness PROOF_UID = C_GetFunctionList DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += UNWINDSET += diff --git a/test/cbmc/proofs/C_GetMechanismInfo/Makefile b/test/cbmc/proofs/C_GetMechanismInfo/Makefile index 8e5a5b17..a8e1f537 100644 --- a/test/cbmc/proofs/C_GetMechanismInfo/Makefile +++ b/test/cbmc/proofs/C_GetMechanismInfo/Makefile @@ -9,8 +9,8 @@ HARNESS_FILE = C_GetMechanismInfo_harness PROOF_UID = C_GetMechanismInfo DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += diff --git a/test/cbmc/proofs/C_GetSlotList/Makefile b/test/cbmc/proofs/C_GetSlotList/Makefile index 4774d925..a367dd26 100644 --- a/test/cbmc/proofs/C_GetSlotList/Makefile +++ b/test/cbmc/proofs/C_GetSlotList/Makefile @@ -9,8 +9,8 @@ HARNESS_FILE = C_GetSlotList_harness PROOF_UID = C_GetSlotList DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include # This proof doesn't care about these stubs REMOVE_FUNCTION_BODY += C_Finalize diff --git a/test/cbmc/proofs/C_Initialize/Makefile b/test/cbmc/proofs/C_Initialize/Makefile index ad5cc1ac..d9fa5d0c 100644 --- a/test/cbmc/proofs/C_Initialize/Makefile +++ b/test/cbmc/proofs/C_Initialize/Makefile @@ -9,8 +9,8 @@ HARNESS_FILE = C_Initialize_harness PROOF_UID = C_Initialize DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += C_Finalize REMOVE_FUNCTION_BODY += C_GetFunctionList diff --git a/test/cbmc/proofs/C_OpenSession/C_OpenSession_harness.c b/test/cbmc/proofs/C_OpenSession/C_OpenSession_harness.c index e945df7d..d377bdf8 100644 --- a/test/cbmc/proofs/C_OpenSession/C_OpenSession_harness.c +++ b/test/cbmc/proofs/C_OpenSession/C_OpenSession_harness.c @@ -37,7 +37,7 @@ void harness() CK_SESSION_HANDLE * pxSession = malloc( sizeof( CK_SESSION_HANDLE ) ); xResult = C_Initialize( NULL ); - __CPROVER__assume( xResult == CKR_OK ); + __CPROVER_assume( xResult == CKR_OK ); xResult = C_OpenSession( 0, xFlags, NULL, 0, pxSession ); diff --git a/test/cbmc/proofs/C_OpenSession/Makefile b/test/cbmc/proofs/C_OpenSession/Makefile index f72ce7d9..50385015 100644 --- a/test/cbmc/proofs/C_OpenSession/Makefile +++ b/test/cbmc/proofs/C_OpenSession/Makefile @@ -9,8 +9,8 @@ HARNESS_FILE = C_OpenSession_harness PROOF_UID = C_OpenSession DEFINES += -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += C_Finalize REMOVE_FUNCTION_BODY += C_GetFunctionList diff --git a/test/cbmc/proofs/C_Sign/Makefile b/test/cbmc/proofs/C_Sign/Makefile index 6da48da5..23696662 100644 --- a/test/cbmc/proofs/C_Sign/Makefile +++ b/test/cbmc/proofs/C_Sign/Makefile @@ -13,8 +13,8 @@ PROOF_UID = C_Sign MAX_OBJECT_NUM=2 DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM) -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += C_Initialize REMOVE_FUNCTION_BODY += C_OpenSession diff --git a/test/cbmc/proofs/C_SignInit/Makefile b/test/cbmc/proofs/C_SignInit/Makefile index ceca613e..e434cd6a 100644 --- a/test/cbmc/proofs/C_SignInit/Makefile +++ b/test/cbmc/proofs/C_SignInit/Makefile @@ -13,8 +13,9 @@ PROOF_UID = C_SignInit MAX_OBJECT_NUM=2 DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM) -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include +INCLUDES += -I$(SRCDIR)/source/portable/os REMOVE_FUNCTION_BODY += C_Initialize REMOVE_FUNCTION_BODY += C_OpenSession @@ -32,5 +33,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c +PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c include ../Makefile.common diff --git a/test/cbmc/proofs/C_Verify/Makefile b/test/cbmc/proofs/C_Verify/Makefile index 6f3c1443..13a2cf87 100644 --- a/test/cbmc/proofs/C_Verify/Makefile +++ b/test/cbmc/proofs/C_Verify/Makefile @@ -13,8 +13,8 @@ PROOF_UID = C_Verify MAX_OBJECT_NUM=2 DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM) -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += C_Initialize REMOVE_FUNCTION_BODY += C_OpenSession diff --git a/test/cbmc/proofs/C_VerifyInit/Makefile b/test/cbmc/proofs/C_VerifyInit/Makefile index 00760b42..7c595ef8 100644 --- a/test/cbmc/proofs/C_VerifyInit/Makefile +++ b/test/cbmc/proofs/C_VerifyInit/Makefile @@ -13,8 +13,9 @@ PROOF_UID = C_VerifyInit MAX_OBJECT_NUM=2 DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM) -INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include +INCLUDES += -I$(SRCDIR)/source/portable/os REMOVE_FUNCTION_BODY += C_Initialize REMOVE_FUNCTION_BODY += C_OpenSession @@ -34,5 +35,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c +PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c include ../Makefile.common diff --git a/test/cbmc/proofs/Makefile-project-targets b/test/cbmc/proofs/Makefile-project-targets index e2517ba3..56a09191 100644 --- a/test/cbmc/proofs/Makefile-project-targets +++ b/test/cbmc/proofs/Makefile-project-targets @@ -8,3 +8,13 @@ # Use this file to give project-specific targets, including targets # that may depend on targets defined in Makefile.common. ################################################################ + +$(PROJECT_SOURCES): $(SRCDIR)/test/build/_deps/mbedtls_2-src/include/mbedtls/pk.h + +$(SRCDIR)/test/build/_deps/mbedtls_2-src/include/mbedtls/pk.h: + if [ ! -f $@ ] ; then cd $(SRCDIR)/test && cmake -B build ; fi + +clean: clean_mbedtls + +clean_mbedtls: + $(RM) -r $(SRCDIR)/test/build diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common index 1c05c2ef..7658ee5b 100644 --- a/test/cbmc/proofs/Makefile.common +++ b/test/cbmc/proofs/Makefile.common @@ -4,7 +4,7 @@ # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. # SPDX-License-Identifier: MIT-0 -CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.5 +CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.11 ################################################################ # The CBMC Starter Kit depends on the files Makefile.common and @@ -211,10 +211,13 @@ CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER) ifeq ($(strip $(ENABLE_POOLS)),) POOL = + INIT_POOLS = else ifeq ($(strip $(EXPENSIVE)),) POOL = + INIT_POOLS = else POOL = --pool expensive + INIT_POOLS = --pools expensive:1 endif # Similar to the pool feature above. If Litani is new enough, enable @@ -229,40 +232,45 @@ endif # # Each variable below controls a specific property checking flag # within CBMC. If desired, a property flag can be disabled within -# a particular proof by nulling the corresponding variable. For -# instance, the following line: +# a particular proof by nulling the corresponding variable when CBMC's default +# is not to perform such checks, or setting to --no--check when CBMC's +# default is to perform such checks. For instance, the following lines: # -# CHECK_FLAG_POINTER_CHECK = +# CBMC_FLAG_POINTER_CHECK = --no-pointer-check +# CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK = # -# would disable the --pointer-check CBMC flag within: +# would disable pointer checks and unsigned overflow checks with CBMC flag +# within: # * an entire project when added to Makefile-project-defines # * a specific proof when added to the harness Makefile -CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail -CBMC_FLAG_MALLOC_FAIL_NULL ?= --malloc-fail-null -CBMC_FLAG_BOUNDS_CHECK ?= --bounds-check +CBMC_FLAG_MALLOC_MAY_FAIL ?= # set to --no-malloc-may-fail to disable +CBMC_FLAG_BOUNDS_CHECK ?= # set to --no-bounds-check to disable CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check -CBMC_FLAG_DIV_BY_ZERO_CHECK ?= --div-by-zero-check +CBMC_FLAG_DIV_BY_ZERO_CHECK ?= # set to --no-div-by-zero-check to disable CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= --float-overflow-check CBMC_FLAG_NAN_CHECK ?= --nan-check -CBMC_FLAG_POINTER_CHECK ?= --pointer-check +CBMC_FLAG_POINTER_CHECK ?= #set to --no-pointer-check to disable CBMC_FLAG_POINTER_OVERFLOW_CHECK ?= --pointer-overflow-check -CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= --pointer-primitive-check -CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= --signed-overflow-check -CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= --undefined-shift-check +CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= # set to --no-pointer-primitive-check to disable +CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= # set to --no-signed-overflow-check to disable +CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= # set to --no-undefined-shift-check to disable CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK ?= --unsigned-overflow-check -CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions -CBMC_FLAG_UNWIND ?= --unwind 1 +CBMC_FLAG_UNWINDING_ASSERTIONS ?= # set to --no-unwinding-assertions to disable +CBMC_DEFAULT_UNWIND ?= --unwind 1 CBMC_FLAG_FLUSH ?= --flush # CBMC flags used for property checking and coverage checking -CBMCFLAGS += $(CBMC_FLAG_UNWIND) $(CBMC_UNWINDSET) $(CBMC_FLAG_FLUSH) +CBMCFLAGS += $(CBMC_FLAG_FLUSH) + +# CBMC 6.0.0 enables all standard checks by default, which can make coverage analysis +# very slow. See https://github.com/diffblue/cbmc/issues/8389 +# For now, we disable these checks when generating coverage info. +COVERFLAGS ?= --no-standard-checks --malloc-may-fail --malloc-fail-null # CBMC flags used for property checking -CHECKFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL) -CHECKFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL) CHECKFLAGS += $(CBMC_FLAG_BOUNDS_CHECK) CHECKFLAGS += $(CBMC_FLAG_CONVERSION_CHECK) CHECKFLAGS += $(CBMC_FLAG_DIV_BY_ZERO_CHECK) @@ -274,12 +282,6 @@ CHECKFLAGS += $(CBMC_FLAG_POINTER_PRIMITIVE_CHECK) CHECKFLAGS += $(CBMC_FLAG_SIGNED_OVERFLOW_CHECK) CHECKFLAGS += $(CBMC_FLAG_UNDEFINED_SHIFT_CHECK) CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK) -CHECKFLAGS += $(CBMC_FLAG_UNWINDING_ASSERTIONS) - -# CBMC flags used for coverage checking - -COVERFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL) -COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL) # Additional CBMC flag to CBMC control verbosity. # @@ -307,10 +309,13 @@ COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL) NONDET_STATIC ?= # Flags to pass to goto-cc for compilation and linking -COMPILE_FLAGS ?= -Wall -LINK_FLAGS ?= -Wall +COMPILE_FLAGS ?= -Wall -Werror +LINK_FLAGS ?= -Wall -Werror EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols +# During instrumentation, it adds models of C library functions +ADD_LIBRARY_FLAG := --add-library + # Preprocessor include paths -I... INCLUDES ?= @@ -349,9 +354,9 @@ UNWINDSET ?= # contracts). To satisfy this requirement, it may be necessary to # unwind some loops before the function contract and loop invariant # transformations are applied to the goto program. This variable -# EARLY_UNWINDSET is identical to UNWINDSET, and we assume that the -# loops mentioned in EARLY_UNWINDSET and UNWINDSET are disjoint. -EARLY_UNWINDSET ?= +# CPROVER_LIBRARY_UNWINDSET is identical to UNWINDSET, and we assume that the +# loops mentioned in CPROVER_LIBRARY_UNWINDSET and UNWINDSET are disjoint. +CPROVER_LIBRARY_UNWINDSET ?= # CBMC function removal (Normally set set in the proof Makefile) # @@ -396,12 +401,28 @@ PROOF_SOURCES ?= # report, making the proof run appear to "hang". CBMC_TIMEOUT ?= 21600 +# CBMC string abstraction +# +# Replace all uses of char * by a struct that carries that string, +# and also the underlying allocation and the C string length. +STRING_ABSTRACTION ?= +ifdef STRING_ABSTRACTION + ifneq ($(strip $(STRING_ABSTRACTION)),) + CBMC_STRING_ABSTRACTION := --string-abstraction + endif +endif + +# Optional configuration library flags +OPT_CONFIG_LIBRARY ?= +CBMC_OPT_CONFIG_LIBRARY := $(CBMC_FLAG_MALLOC_MAY_FAIL) $(CBMC_STRING_ABSTRACTION) + # Proof writers could add function contracts in their source code. # These contracts are ignored by default, but may be enabled in two distinct # contexts using the following two variables: # 1. To check whether one or more function contracts are sound with respect to # the function implementation, CHECK_FUNCTION_CONTRACTS should be a list of -# function names. +# function names. Use CHECK_FUNCTION_CONTRACTS_REC to check contracts on +# recursive functions. # 2. To replace calls to certain functions with their correspondent function # contracts, USE_FUNCTION_CONTRACTS should be a list of function names. # One must check separately whether a function contract is sound before @@ -409,17 +430,52 @@ CBMC_TIMEOUT ?= 21600 CHECK_FUNCTION_CONTRACTS ?= CBMC_CHECK_FUNCTION_CONTRACTS := $(patsubst %,--enforce-contract %, $(CHECK_FUNCTION_CONTRACTS)) +CHECK_FUNCTION_CONTRACTS_REC ?= +CBMC_CHECK_FUNCTION_CONTRACTS_REC := $(patsubst %,--enforce-contract-rec %, $(CHECK_FUNCTION_CONTRACTS_REC)) + USE_FUNCTION_CONTRACTS ?= CBMC_USE_FUNCTION_CONTRACTS := $(patsubst %,--replace-call-with-contract %, $(USE_FUNCTION_CONTRACTS)) +CODE_CONTRACTS := $(CHECK_FUNCTION_CONTRACTS)$(USE_FUNCTION_CONTRACTS)$(APPLY_LOOP_CONTRACTS) + +# Proof writers may also apply function contracts using the Dynamic Frame +# Condition Checking (DFCC) mode. For more information on DFCC, +# please see https://diffblue.github.io/cbmc/contracts-dev-spec-dfcc.html. +USE_DYNAMIC_FRAMES ?= +ifdef USE_DYNAMIC_FRAMES + ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) + CBMC_USE_DYNAMIC_FRAMES := $(CBMC_OPT_CONFIG_LIBRARY) --dfcc $(HARNESS_ENTRY) $(CBMC_CHECK_FUNCTION_CONTRACTS_REC) + endif +endif + # Similarly, proof writers could also add loop contracts in their source code # to obtain unbounded correctness proofs. Unlike function contracts, loop # contracts are not reusable and thus are checked and used simultaneously. # These contracts are also ignored by default, but may be enabled by setting -# the APPLY_LOOP_CONTRACTS variable to 1. -APPLY_LOOP_CONTRACTS ?= 0 -ifeq ($(APPLY_LOOP_CONTRACTS),1) - CBMC_APPLY_LOOP_CONTRACTS ?= --apply-loop-contracts +# the APPLY_LOOP_CONTRACTS variable. +APPLY_LOOP_CONTRACTS ?= +ifdef APPLY_LOOP_CONTRACTS + ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),) + CBMC_APPLY_LOOP_CONTRACTS := --apply-loop-contracts + endif +endif + +# The default unwind should only be used in DFCC mode without loop contracts. +# When loop contracts are applied, we only unwind specified loops. +# If any loops remain after loop contracts have been applied, CBMC might try +# to unwind the program indefinitely, because we do not pass default unwind +# (i.e., --unwind 1) to CBMC when in DFCC mode. +# We must not use a default unwind command in DFCC mode, because contract instrumentation +# introduces loops encoding write set inclusion checks that must be dynamically unwound during +# symex. +ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) +ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),) + UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) + UNWIND_0500_DESC="$(PROOF_UID): unwinding specified subset of loops" +else + UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_FLAG_UNWINDING_ASSERTIONS) + UNWIND_0500_DESC="$(PROOF_UID): unwinding all loops" +endif endif # Silence makefile output (eg, long litani commands) unless VERBOSE is set. @@ -442,7 +498,6 @@ GOTO_CC ?= goto-cc GOTO_INSTRUMENT ?= goto-instrument CRANGLER ?= crangler VIEWER ?= cbmc-viewer -MAKE_SOURCE ?= make-source VIEWER2 ?= cbmc-viewer CMAKE ?= cmake @@ -465,26 +520,34 @@ COMMA :=, # Set C compiler defines CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS) -COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS) DEFINES += -DCBMC=1 DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS) DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))" # CI currently assumes cbmc invocation has at most one --unwindset + +# UNWINDSET is designed for user code (i.e., proof and project code) ifdef UNWINDSET - ifneq ($(strip $(UNWINDSET)),"") + ifneq ($(strip $(UNWINDSET)),) CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET))) endif endif -ifdef EARLY_UNWINDSET - ifneq ($(strip $(EARLY_UNWINDSET)),"") - CBMC_EARLY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(EARLY_UNWINDSET))) + +# CPROVER_LIBRARY_UNWINDSET is designed for CPROVER library functions +ifdef CPROVER_LIBRARY_UNWINDSET + ifneq ($(strip $(CPROVER_LIBRARY_UNWINDSET)),) + CBMC_CPROVER_LIBRARY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(CPROVER_LIBRARY_UNWINDSET))) endif endif CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY)) -CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER)) + +ifdef RESTRICT_FUNCTION_POINTER + ifneq ($(strip $(RESTRICT_FUNCTION_POINTER)),) + CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER)) + endif +endif ################################################################ # Targets for rewriting source files with crangler @@ -568,7 +631,7 @@ $(REWRITTEN_SOURCES): # Build targets that make the relevant .goto files # Compile project sources -$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES) +$(PROJECT_GOTO)0100.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES) $(LITANI) add-job \ --command \ '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \ @@ -580,7 +643,7 @@ $(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES) --description "$(PROOF_UID): building project binary" # Compile proof sources -$(PROOF_GOTO)1.goto: $(PROOF_SOURCES) +$(PROOF_GOTO)0100.goto: $(PROOF_SOURCES) $(LITANI) add-job \ --command \ '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \ @@ -592,7 +655,7 @@ $(PROOF_GOTO)1.goto: $(PROOF_SOURCES) --description "$(PROOF_UID): building proof binary" # Remove function bodies from project sources -$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto +$(PROJECT_GOTO)0200.goto: $(PROJECT_GOTO)0100.goto $(LITANI) add-job \ --command \ '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \ @@ -604,7 +667,7 @@ $(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto --description "$(PROOF_UID): removing function bodies from project sources" # Link project and proof sources into the proof harness -$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto +$(HARNESS_GOTO)0100.goto: $(PROOF_GOTO)0100.goto $(PROJECT_GOTO)0200.goto $(LITANI) add-job \ --command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ $(LINK_FLAGS) -o $@' \ --inputs $^ \ @@ -615,10 +678,10 @@ $(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto --description "$(PROOF_UID): linking project to proof" # Restrict function pointers -$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto +$(HARNESS_GOTO)0200.goto: $(HARNESS_GOTO)0100.goto $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) $^ $@' \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \ --inputs $^ \ --outputs $@ \ --stdout-file $(LOGDIR)/restrict_function_pointer-log.txt \ @@ -627,7 +690,17 @@ $(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto --description "$(PROOF_UID): restricting function pointers in project sources" # Fill static variable with unconstrained values -$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto +$(HARNESS_GOTO)0300.goto: $(HARNESS_GOTO)0200.goto +ifneq ($(strip $(CODE_CONTRACTS)),) + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/nondet_static-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not setting static variables to nondet (will do during contract instrumentation)" +else $(LITANI) add-job \ --command \ '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \ @@ -637,83 +710,102 @@ $(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto --pipeline-name "$(PROOF_UID)" \ --ci-stage build \ --description "$(PROOF_UID): setting static variables to nondet" +endif -# Omit unused functions (sharpens coverage calculations) -$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto +# Link CPROVER library if DFCC mode is on +$(HARNESS_GOTO)0400.goto: $(HARNESS_GOTO)0300.goto +ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(ADD_LIBRARY_FLAG) $(CBMC_OPT_CONFIG_LIBRARY) $^ $@' \ --inputs $^ \ --outputs $@ \ - --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \ + --stdout-file $(LOGDIR)/linking-library-models-log.txt \ --pipeline-name "$(PROOF_UID)" \ --ci-stage build \ - --description "$(PROOF_UID): dropping unused functions" + --description "$(PROOF_UID): linking CPROVER library" +else + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/linking-library-models-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not linking CPROVER library" +endif -# Omit initialization of unused global variables (reduces problem size) -$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto +# Early unwind all loops on DFCC mode; otherwise, only unwind loops in proof and project code +$(HARNESS_GOTO)0500.goto: $(HARNESS_GOTO)0400.goto +ifneq ($(strip $(USE_DYNAMIC_FRAMES)),) $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \ --inputs $^ \ --outputs $@ \ - --stdout-file $(LOGDIR)/slice_global_inits-log.txt \ + --stdout-file $(LOGDIR)/unwind_loops-log.txt \ --pipeline-name "$(PROOF_UID)" \ --ci-stage build \ - --description "$(PROOF_UID): slicing global initializations" - -# Replace function calls with function contracts -# This must be done before enforcing function contracts, -# since contract enforcement inlines all function calls. -$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto + --description $(UNWIND_0500_DESC) +else ifneq ($(strip $(CODE_CONTRACTS)),) $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \ --inputs $^ \ --outputs $@ \ - --stdout-file $(LOGDIR)/use_function_contracts-log.txt \ + --stdout-file $(LOGDIR)/unwind_loops-log.txt \ --pipeline-name "$(PROOF_UID)" \ --ci-stage build \ - --description "$(PROOF_UID): replacing function calls with function contracts" + --description "$(PROOF_UID): unwinding loops in proof and project code" +else + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/unwind_loops-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not unwinding loops" +endif -# Unwind loops for loop and function contracts -$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto +# Replace function contracts, check function contracts, instrument for loop contracts +$(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_EARLY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \ + '$(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \ --inputs $^ \ --outputs $@ \ - --stdout-file $(LOGDIR)/unwind_loops-log.txt \ + --stdout-file $(LOGDIR)/check_function_contracts-log.txt \ --pipeline-name "$(PROOF_UID)" \ --ci-stage build \ - --description "$(PROOF_UID): unwinding loops" + --description "$(PROOF_UID): checking function contracts" -# Apply loop contracts -$(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto +# Omit initialization of unused global variables (reduces problem size) +$(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \ --inputs $^ \ --outputs $@ \ - --stdout-file $(LOGDIR)/apply_loop_contracts-log.txt \ + --stdout-file $(LOGDIR)/slice_global_inits-log.txt \ --pipeline-name "$(PROOF_UID)" \ --ci-stage build \ - --description "$(PROOF_UID): applying loop contracts" + --description "$(PROOF_UID): slicing global initializations" -# Check function contracts -$(HARNESS_GOTO)9.goto: $(HARNESS_GOTO)8.goto +# Omit unused functions (sharpens coverage calculations) +$(HARNESS_GOTO)0800.goto: $(HARNESS_GOTO)0700.goto $(LITANI) add-job \ --command \ - '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $^ $@' \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \ --inputs $^ \ --outputs $@ \ - --stdout-file $(LOGDIR)/check_function_contracts-log.txt \ + --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \ --pipeline-name "$(PROOF_UID)" \ --ci-stage build \ - --description "$(PROOF_UID): checking function contracts" + --description "$(PROOF_UID): dropping unused functions" # Final name for proof harness -$(HARNESS_GOTO).goto: $(HARNESS_GOTO)9.goto +$(HARNESS_GOTO).goto: $(HARNESS_GOTO)0800.goto $(LITANI) add-job \ --command 'cp $< $@' \ --inputs $^ \ @@ -725,11 +817,19 @@ $(HARNESS_GOTO).goto: $(HARNESS_GOTO)9.goto ################################################################ # Targets to run the analysis commands -$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto +ifdef CBMCFLAGS + ifeq ($(strip $(CODE_CONTRACTS)),) + CBMCFLAGS += $(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_OPT_CONFIG_LIBRARY) + else ifeq ($(strip $(USE_DYNAMIC_FRAMES)),) + CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_OPT_CONFIG_LIBRARY) + endif +endif + +$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto $(LITANI) add-job \ $(POOL) \ --command \ - '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \ --inputs $^ \ --outputs $@ \ --ci-stage test \ @@ -742,11 +842,11 @@ $(LOGDIR)/result.txt: $(HARNESS_GOTO).goto --stderr-file $(LOGDIR)/result-err-log.txt \ --description "$(PROOF_UID): checking safety properties" -$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto +$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto $(LITANI) add-job \ $(POOL) \ --command \ - '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \ --inputs $^ \ --outputs $@ \ --ci-stage test \ @@ -789,54 +889,19 @@ $(LOGDIR)/coverage.xml: $(HARNESS_GOTO).goto --stderr-file $(LOGDIR)/coverage-err-log.txt \ --description "$(PROOF_UID): calculating coverage" -define VIEWER_CMD - $(VIEWER) \ - --result $(LOGDIR)/result.txt \ - --block $(LOGDIR)/coverage.xml \ - --property $(LOGDIR)/property.xml \ - --srcdir $(SRCDIR) \ - --goto $(HARNESS_GOTO).goto \ - --htmldir $(PROOFDIR)/html -endef -export VIEWER_CMD - -$(PROOFDIR)/html: $(LOGDIR)/result.txt $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml - $(LITANI) add-job \ - --command "$$VIEWER_CMD" \ - --inputs $^ \ - --outputs $(PROOFDIR)/html \ - --pipeline-name "$(PROOF_UID)" \ - --ci-stage report \ - --stdout-file $(LOGDIR)/viewer-log.txt \ - --description "$(PROOF_UID): generating report" - +COVERAGE ?= $(LOGDIR)/coverage.xml +VIEWER_COVERAGE_FLAG ?= --coverage $(COVERAGE) -# Caution: run make-source before running property and coverage checking -# The current make-source script removes the goto binary -$(LOGDIR)/source.json: - mkdir -p $(dir $@) - $(RM) -r $(GOTODIR) - $(MAKE_SOURCE) --srcdir $(SRCDIR) --wkdir $(PROOFDIR) > $@ - $(RM) -r $(GOTODIR) - -define VIEWER2_CMD - $(VIEWER2) \ - --result $(LOGDIR)/result.xml \ - --coverage $(LOGDIR)/coverage.xml \ - --property $(LOGDIR)/property.xml \ - --srcdir $(SRCDIR) \ - --goto $(HARNESS_GOTO).goto \ - --reportdir $(PROOFDIR)/report \ - --config $(PROOFDIR)/cbmc-viewer.json -endef -export VIEWER2_CMD - -# Omit logs/source.json from report generation until make-sources -# works correctly with Makefiles that invoke the compiler with -# mutliple source files at once. -$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml +$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(COVERAGE) $(LITANI) add-job \ - --command "$$VIEWER2_CMD" \ + --command " $(VIEWER) \ + --result $(LOGDIR)/result.xml \ + $(VIEWER_COVERAGE_FLAG) \ + --property $(LOGDIR)/property.xml \ + --srcdir $(SRCDIR) \ + --goto $(HARNESS_GOTO).goto \ + --reportdir $(PROOFDIR)/report \ + --config $(PROOFDIR)/cbmc-viewer.json" \ --inputs $^ \ --outputs $(PROOFDIR)/report \ --pipeline-name "$(PROOF_UID)" \ @@ -859,7 +924,7 @@ litani-path: _goto: $(HARNESS_GOTO).goto goto: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _goto @ echo Running 'litani build' @@ -868,7 +933,7 @@ goto: _result: $(LOGDIR)/result.txt result: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _result @ echo Running 'litani build' @@ -877,7 +942,7 @@ result: _property: $(LOGDIR)/property.xml property: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _property @ echo Running 'litani build' @@ -886,30 +951,26 @@ property: _coverage: $(LOGDIR)/coverage.xml coverage: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _coverage @ echo Running 'litani build' $(LITANI) run-build -# Choose the invocation of cbmc-viewer depending on which version of -# cbmc-viewer is installed. The --version flag is not implemented in -# version 1 --- it is an "unrecognized argument" --- but it is -# implemented in version 2. -_report1: $(PROOFDIR)/html -_report2: $(PROOFDIR)/report -_report: - (cbmc-viewer --version 2>&1 | grep "unrecognized argument" > /dev/null) && \ - $(MAKE) -B _report1 || $(MAKE) -B _report2 - -report report1 report2: +_report: $(PROOFDIR)/report +report: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _report @ echo Running 'litani build' $(LITANI) run-build +_report_no_coverage: + $(MAKE) COVERAGE="" VIEWER_COVERAGE_FLAG="" _report +report-no-coverage: + $(MAKE) COVERAGE="" VIEWER_COVERAGE_FLAG=" " report + ################################################################ # Targets to clean up after ourselves clean: @@ -919,7 +980,7 @@ clean: -$(RM) $(REWRITTEN_SOURCES) $(foreach rs,$(REWRITTEN_SOURCES),$(rs).json) veryclean: clean - -$(RM) -r html report + -$(RM) -r report -$(RM) -r $(LOGDIR) $(GOTODIR) .PHONY: \ @@ -927,15 +988,14 @@ veryclean: clean _goto \ _property \ _report \ - _report2 \ - _result \ + _report_no_coverage \ clean \ coverage \ goto \ litani-path \ property \ report \ - report2 \ + report-no-coverage \ result \ setup_dependencies \ testdeps \ @@ -944,38 +1004,6 @@ veryclean: clean ################################################################ -# Rule for generating cbmc-batch.yaml, used by the CI at -# https://github.com/awslabs/aws-batch-cbmc/ - -JOB_OS ?= ubuntu16 -JOB_MEMORY ?= 32000 - -# Proofs that are expected to fail should set EXPECTED to -# "FAILED" in their Makefile. Values other than SUCCESSFUL -# or FAILED will cause a CI error. -EXPECTED ?= SUCCESSFUL - -define yaml_encode_options - "$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')" -endef - -CI_FLAGS = $(CBMCFLAGS) $(CHECKFLAGS) $(COVERFLAGS) - -cbmc-batch.yaml: - @$(RM) $@ - @echo 'build_memory: $(JOB_MEMORY)' > $@ - @echo 'cbmcflags: $(strip $(call yaml_encode_options,$(CI_FLAGS)))' >> $@ - @echo 'coverage_memory: $(JOB_MEMORY)' >> $@ - @echo 'expected: $(EXPECTED)' >> $@ - @echo 'goto: $(HARNESS_GOTO).goto' >> $@ - @echo 'jobos: $(JOB_OS)' >> $@ - @echo 'property_memory: $(JOB_MEMORY)' >> $@ - @echo 'report_memory: $(JOB_MEMORY)' >> $@ - -.PHONY: cbmc-batch.yaml - -################################################################ - # Run "make echo-proof-uid" to print the proof ID of a proof. This can be # used by scripts to ensure that every proof has an ID, that there are # no duplicates, etc. diff --git a/test/cbmc/proofs/vAppendSHA256AlgorithmIdentifierSequence/vAppendSHA256AlgorithmIdentifierSequence_harness.c b/test/cbmc/proofs/vAppendSHA256AlgorithmIdentifierSequence/vAppendSHA256AlgorithmIdentifierSequence_harness.c index a116f801..63dd997b 100644 --- a/test/cbmc/proofs/vAppendSHA256AlgorithmIdentifierSequence/vAppendSHA256AlgorithmIdentifierSequence_harness.c +++ b/test/cbmc/proofs/vAppendSHA256AlgorithmIdentifierSequence/vAppendSHA256AlgorithmIdentifierSequence_harness.c @@ -27,6 +27,7 @@ * @brief Implements the proof harness for vAppendSHA256AlgorithmIdentifierSequence function. */ #include +#include #include "core_pkcs11.h" diff --git a/test/cbmc/proofs/xFindObjectWithLabelAndClass/Makefile b/test/cbmc/proofs/xFindObjectWithLabelAndClass/Makefile index 4631b94b..5c737a2d 100644 --- a/test/cbmc/proofs/xFindObjectWithLabelAndClass/Makefile +++ b/test/cbmc/proofs/xFindObjectWithLabelAndClass/Makefile @@ -12,7 +12,8 @@ PROOF_UID = xFindObjectWithLabelAndClass MAX_LABEL_SIZE=32 DEFINES += -DMAX_LABEL_SIZE=$(MAX_LABEL_SIZE) -INCLUDES += + +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += C_Initialize REMOVE_FUNCTION_BODY += C_Login @@ -22,5 +23,6 @@ UNWINDSET += strlen.0:$(MAX_LABEL_SIZE) PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/pkcs11_interface_stubs.c PROJECT_SOURCES += $(SRCDIR)/source/core_pkcs11.c +PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c include ../Makefile.common diff --git a/test/cbmc/proofs/xGetSlotList/xGetSlotList_harness.c b/test/cbmc/proofs/xGetSlotList/xGetSlotList_harness.c index f87f253a..3e6c92c9 100644 --- a/test/cbmc/proofs/xGetSlotList/xGetSlotList_harness.c +++ b/test/cbmc/proofs/xGetSlotList/xGetSlotList_harness.c @@ -27,6 +27,7 @@ * @brief Implements the proof harness for xGetSlotList function. */ #include +#include #include "core_pkcs11.h" void harness() diff --git a/test/cbmc/proofs/xInitializePKCS11/Makefile b/test/cbmc/proofs/xInitializePKCS11/Makefile index 5f332b83..341e5ba4 100644 --- a/test/cbmc/proofs/xInitializePKCS11/Makefile +++ b/test/cbmc/proofs/xInitializePKCS11/Makefile @@ -9,13 +9,16 @@ HARNESS_FILE = xInitializePKCS11_harness PROOF_UID = xInitializePKCS11 DEFINES += -INCLUDES += + +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/pkcs11_interface_stubs.c PROJECT_SOURCES += $(SRCDIR)/source/core_pkcs11.c +PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c include ../Makefile.common diff --git a/test/cbmc/proofs/xInitializePkcs11Session/Makefile b/test/cbmc/proofs/xInitializePkcs11Session/Makefile index 60b5c0c4..d651f254 100644 --- a/test/cbmc/proofs/xInitializePkcs11Session/Makefile +++ b/test/cbmc/proofs/xInitializePkcs11Session/Makefile @@ -9,12 +9,16 @@ HARNESS_FILE = xInitializePkcs11Session_harness PROOF_UID = xInitializePkcs11Session DEFINES += -INCLUDES += + +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include + +CBMC_OBJECT_BITS = 10 UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/pkcs11_interface_stubs.c PROJECT_SOURCES += $(SRCDIR)/source/core_pkcs11.c +PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c include ../Makefile.common diff --git a/test/cbmc/proofs/xInitializePkcs11Token/Makefile b/test/cbmc/proofs/xInitializePkcs11Token/Makefile index 5db829c9..f86d2f38 100644 --- a/test/cbmc/proofs/xInitializePkcs11Token/Makefile +++ b/test/cbmc/proofs/xInitializePkcs11Token/Makefile @@ -9,7 +9,10 @@ HARNESS_FILE = xInitializePkcs11Token_harness PROOF_UID = xInitializePkcs11Token DEFINES += -INCLUDES += + +INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include + +CBMC_OBJECT_BITS = 10 REMOVE_FUNCTION_BODY += UNWINDSET += @@ -17,5 +20,6 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/pkcs11_interface_stubs.c PROJECT_SOURCES += $(SRCDIR)/source/core_pkcs11.c +PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c include ../Makefile.common diff --git a/test/cbmc/stubs/mbedtls_stubs.c b/test/cbmc/stubs/mbedtls_stubs.c index 64cb8c89..7d029bec 100644 --- a/test/cbmc/stubs/mbedtls_stubs.c +++ b/test/cbmc/stubs/mbedtls_stubs.c @@ -31,6 +31,13 @@ #include "mbedtls/entropy.h" #include "mbedtls/ctr_drbg.h" #include "mbedtls/threading.h" +#include "mbedtls/bignum.h" +#include "mbedtls/cipher.h" +#include "mbedtls/cmac.h" +#include "mbedtls/ecp.h" +#include "mbedtls/md.h" +#include "mbedtls/sha256.h" +#include "mbedtls/x509_crt.h" void mbedtls_entropy_init( mbedtls_entropy_context * ctx ) @@ -178,3 +185,206 @@ void (* mbedtls_mutex_init)( mbedtls_threading_mutex_t * ) = threading_mutex_ini void (* mbedtls_mutex_free)( mbedtls_threading_mutex_t * ) = threading_mutex_free; int (* mbedtls_mutex_lock)( mbedtls_threading_mutex_t * ) = threading_mutex_lock; int (* mbedtls_mutex_unlock)( mbedtls_threading_mutex_t * ) = threading_mutex_unlock; + +int mbedtls_cipher_cmac_finish( mbedtls_cipher_context_t * ctx, + unsigned char * output ) +{ + int result; + + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( output != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_havoc_object( output ); + + return result; +} + +int mbedtls_cipher_cmac_starts( mbedtls_cipher_context_t * ctx, + const unsigned char * key, + size_t keybits ) +{ + int result; + + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( key != NULL, "Received an unexpected NULL pointer." ); + + return result; +} + +int mbedtls_cipher_cmac_update( mbedtls_cipher_context_t * ctx, + const unsigned char * input, + size_t ilen ) +{ + int result; + + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( input != NULL, "Received an unexpected NULL pointer." ); + + return result; +} + +void mbedtls_cipher_free( mbedtls_cipher_context_t * ctx ) +{ + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); +} + +const mbedtls_cipher_info_t * mbedtls_cipher_info_from_type( const mbedtls_cipher_type_t cipher_type ) +{ + mbedtls_cipher_info_t * r = malloc( sizeof( mbedtls_cipher_info_t ) ); + + return r; +} + +int mbedtls_cipher_setup( mbedtls_cipher_context_t * ctx, + const mbedtls_cipher_info_t * cipher_info ) +{ + int result; + + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( cipher_info != NULL, "Received an unexpected NULL pointer." ); + + return result; +} + +int mbedtls_ecp_point_read_binary( const mbedtls_ecp_group * grp, + mbedtls_ecp_point * P, + const unsigned char * buf, + size_t ilen ) +{ + int result; + + __CPROVER_assert( grp != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( P != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( buf != NULL, "Received an unexpected NULL pointer." ); + + return result; +} + +int mbedtls_ecp_tls_write_point( const mbedtls_ecp_group * grp, + const mbedtls_ecp_point * pt, + int format, + size_t * olen, + unsigned char * buf, + size_t blen ) +{ + int result; + + __CPROVER_assert( grp != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( pt != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( olen != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( buf != NULL, "Received an unexpected NULL pointer." ); + + return result; +} + +void mbedtls_md_free( mbedtls_md_context_t * ctx ) +{ + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); +} + +int mbedtls_md_hmac_finish( mbedtls_md_context_t * ctx, + unsigned char * output ) +{ + int result; + + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( output != NULL, "Received an unexpected NULL pointer." ); + + return result; +} + +int mbedtls_md_hmac_update( mbedtls_md_context_t * ctx, + const unsigned char * input, + size_t ilen ) +{ + int result; + + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( input != NULL, "Received an unexpected NULL pointer." ); + + return result; +} + +int mbedtls_mpi_read_binary( mbedtls_mpi * X, + const unsigned char * buf, + size_t buflen ) +{ + int result; + + __CPROVER_assert( X != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( buf != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_havoc_object( X ); + + return result; +} + +void mbedtls_pk_free( mbedtls_pk_context * ctx ) +{ + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); +} + +int mbedtls_pk_write_key_der( mbedtls_pk_context * ctx, + unsigned char * buf, + size_t size ) +{ + int result; + + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( buf != NULL, "Received an unexpected NULL pointer." ); + + return result; +} + +mbedtls_pk_type_t mbedtls_pk_get_type( const mbedtls_pk_context * ctx ) +{ + mbedtls_pk_type_t result; + + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); + + return result; +} + +int mbedtls_pk_write_pubkey_der( mbedtls_pk_context * ctx, + unsigned char * buf, + size_t size ) +{ + int result; + + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( buf != NULL, "Received an unexpected NULL pointer." ); + + return result; +} + +void mbedtls_sha256_free( mbedtls_sha256_context * ctx ) +{ + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); +} + +int mbedtls_sha256_update_ret( mbedtls_sha256_context * ctx, + const unsigned char * input, + size_t ilen ) +{ + int result; + + __CPROVER_assert( ctx != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( input != NULL, "Received an unexpected NULL pointer." ); + + return result; +} + +void mbedtls_x509_crt_free( mbedtls_x509_crt * crt ) +{ + __CPROVER_assert( crt != NULL, "Received an unexpected NULL pointer." ); +} + +int mbedtls_x509_crt_parse( mbedtls_x509_crt * chain, + const unsigned char * buf, + size_t buflen ) +{ + int result; + + __CPROVER_assert( chain != NULL, "Received an unexpected NULL pointer." ); + __CPROVER_assert( buf != NULL, "Received an unexpected NULL pointer." ); + + return result; +} diff --git a/test/cbmc/stubs/pkcs11_interface_stubs.c b/test/cbmc/stubs/pkcs11_interface_stubs.c index 4452a8c3..1cadf919 100644 --- a/test/cbmc/stubs/pkcs11_interface_stubs.c +++ b/test/cbmc/stubs/pkcs11_interface_stubs.c @@ -28,6 +28,7 @@ */ #include +#include #include #include "core_pkcs11.h"