From e1c60e5073cab9aa607b720260dcd76c1e5be66f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 23 Aug 2024 13:13:35 +0000 Subject: [PATCH] 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. --- .github/workflows/ci.yml | 3 +- test/cbmc/proofs/C_CloseSession/Makefile | 2 +- test/cbmc/proofs/C_CreateObject/Makefile | 6 +- test/cbmc/proofs/C_DestroyObject/Makefile | 2 +- test/cbmc/proofs/C_DigestFinal/Makefile | 2 +- test/cbmc/proofs/C_DigestInit/Makefile | 2 +- test/cbmc/proofs/C_DigestUpdate/Makefile | 2 +- test/cbmc/proofs/C_Finalize/Makefile | 2 +- test/cbmc/proofs/C_FindObjects/Makefile | 6 +- test/cbmc/proofs/C_FindObjectsFinal/Makefile | 2 +- test/cbmc/proofs/C_FindObjectsInit/Makefile | 2 +- test/cbmc/proofs/C_GenerateKeyPair/Makefile | 6 +- test/cbmc/proofs/C_GenerateRandom/Makefile | 2 +- test/cbmc/proofs/C_GetAttributeValue/Makefile | 4 +- test/cbmc/proofs/C_GetFunctionList/Makefile | 2 +- test/cbmc/proofs/C_GetMechanismInfo/Makefile | 2 +- test/cbmc/proofs/C_GetSlotList/Makefile | 2 +- test/cbmc/proofs/C_Initialize/Makefile | 2 +- .../C_OpenSession/C_OpenSession_harness.c | 2 +- test/cbmc/proofs/C_OpenSession/Makefile | 2 +- test/cbmc/proofs/C_Sign/Makefile | 2 +- test/cbmc/proofs/C_SignInit/Makefile | 4 +- test/cbmc/proofs/C_Verify/Makefile | 2 +- test/cbmc/proofs/C_VerifyInit/Makefile | 4 +- test/cbmc/proofs/Makefile-project-targets | 10 + test/cbmc/proofs/Makefile.common | 396 ++++++++++-------- .../xFindObjectWithLabelAndClass/Makefile | 4 +- test/cbmc/proofs/xInitializePKCS11/Makefile | 5 +- .../proofs/xInitializePkcs11Session/Makefile | 6 +- .../proofs/xInitializePkcs11Token/Makefile | 6 +- test/cbmc/stubs/mbedtls_stubs.c | 209 +++++++++ 31 files changed, 490 insertions(+), 213 deletions(-) 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/test/cbmc/proofs/C_CloseSession/Makefile b/test/cbmc/proofs/C_CloseSession/Makefile index a0655f54..98bc66ca 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)/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 index cce61508..a23dd0b9 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)/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 index 31b6d1dc..0748fa66 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)/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 index 3da4cd80..05ff5dc9 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)/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 index 880396a3..22451bb3 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)/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 index cbae7dbf..8520a388 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)/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 index 70be916e..e57a88e9 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)/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 index 301c9543..8a1d5ada 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)/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 @@ -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..ef9505a7 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)/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 index 297408a2..bf67a996 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)/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 index ab342938..4a8f3f8b 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)/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 index 58f535de..ef788c27 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)/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 index 854751b3..fffa27eb 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)/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 index ac2a7d6e..f8fbf3fb 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)/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 index 8e5a5b17..433fe6c2 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)/source/dependency/3rdparty/mbedtls/include REMOVE_FUNCTION_BODY += diff --git a/test/cbmc/proofs/C_GetSlotList/Makefile b/test/cbmc/proofs/C_GetSlotList/Makefile index 4774d925..cc1c14c4 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)/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 index ad5cc1ac..1dd2f842 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)/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 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..8f1fe65f 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)/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 index 6da48da5..1a79e2d7 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)/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 index ceca613e..169cf406 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)/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 index 6f3c1443..63a72069 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)/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 index 00760b42..3969228f 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)/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 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/xFindObjectWithLabelAndClass/Makefile b/test/cbmc/proofs/xFindObjectWithLabelAndClass/Makefile index 4631b94b..ac6edb69 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)/source/dependency/3rdparty/mbedtls/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/xInitializePKCS11/Makefile b/test/cbmc/proofs/xInitializePKCS11/Makefile index 5f332b83..e6b5f5d1 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)/source/dependency/3rdparty/mbedtls/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..faa3c747 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)/source/dependency/3rdparty/mbedtls/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..7f542442 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)/source/dependency/3rdparty/mbedtls/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..14687705 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,205 @@ 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; +}