Adjust proof tooling to support CBMC v6

With CBMC v6, unwinding assertions are enabled by default, and object bits no longer need to be set at compile time. Update various build rules to use the latest template as provided with CBMC starter kit. Also fixes missing function definitions.
FreeRTOS · Oct 1, 2024 · e1c60e5 · e1c60e5
1 parent a5cd1c0
commit e1c60e5
Show file tree

Hide file tree

Showing 31 changed files with 490 additions and 213 deletions.
diff --git 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/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)/source/dependency/3rdparty/mbedtls/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
@@ -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)/source/dependency/3rdparty/mbedtls/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
@@ -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)/source/dependency/3rdparty/mbedtls/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
@@ -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)/source/dependency/3rdparty/mbedtls/include
 
 REMOVE_FUNCTION_BODY +=
 UNWINDSET +=

diff --git 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)/source/dependency/3rdparty/mbedtls/include
 
 REMOVE_FUNCTION_BODY +=
 UNWINDSET +=

diff --git 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)/source/dependency/3rdparty/mbedtls/include
 
 REMOVE_FUNCTION_BODY +=
 UNWINDSET +=

diff --git 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)/source/dependency/3rdparty/mbedtls/include
 
 REMOVE_FUNCTION_BODY +=
 UNWINDSET +=

diff --git a/test/cbmc/proofs/C_FindObjects/Makefile b/test/cbmc/proofs/C_FindObjects/Makefile
@@ -9,20 +9,24 @@ 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)/source/dependency/3rdparty/mbedtls/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
 
 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
@@ -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)/source/dependency/3rdparty/mbedtls/include
 
 REMOVE_FUNCTION_BODY +=
 UNWINDSET +=

diff --git 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)/source/dependency/3rdparty/mbedtls/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
@@ -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)/source/dependency/3rdparty/mbedtls/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
@@ -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)/source/dependency/3rdparty/mbedtls/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
@@ -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)/source/dependency/3rdparty/mbedtls/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
@@ -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)/source/dependency/3rdparty/mbedtls/include
 
 REMOVE_FUNCTION_BODY +=
 UNWINDSET +=

diff --git 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)/source/dependency/3rdparty/mbedtls/include
 
 REMOVE_FUNCTION_BODY +=
 

diff --git 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)/source/dependency/3rdparty/mbedtls/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
@@ -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)/source/dependency/3rdparty/mbedtls/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
@@ -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
@@ -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)/source/dependency/3rdparty/mbedtls/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
@@ -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)/source/dependency/3rdparty/mbedtls/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
@@ -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)/source/dependency/3rdparty/mbedtls/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
@@ -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)/source/dependency/3rdparty/mbedtls/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
@@ -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)/source/dependency/3rdparty/mbedtls/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
@@ -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