Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adjust proof tooling to support CBMC v6 #200

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions source/core_pkcs11.c
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@
/* C runtime includes. */
#include <stdio.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>

/**
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_CloseSession/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 5 additions & 1 deletion test/cbmc/proofs/C_CreateObject/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_DestroyObject/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_DigestFinal/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 +=
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_DigestInit/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 +=
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_DigestUpdate/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 +=
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_Finalize/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 +=
Expand Down
6 changes: 5 additions & 1 deletion test/cbmc/proofs/C_FindObjects/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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)/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

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
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_FindObjectsFinal/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 +=
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_FindObjectsInit/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
6 changes: 5 additions & 1 deletion test/cbmc/proofs/C_GenerateKeyPair/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_GenerateRandom/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion test/cbmc/proofs/C_GetAttributeValue/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 +=

Expand All @@ -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
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_GetFunctionList/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 +=
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_GetMechanismInfo/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 +=

Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_GetSlotList/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_Initialize/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_OpenSession/C_OpenSession_harness.c
Original file line number Diff line number Diff line change
Expand Up @@ -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 );

Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_OpenSession/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_Sign/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion test/cbmc/proofs/C_SignInit/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
2 changes: 1 addition & 1 deletion test/cbmc/proofs/C_Verify/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion test/cbmc/proofs/C_VerifyInit/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
10 changes: 10 additions & 0 deletions test/cbmc/proofs/Makefile-project-targets
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading
Loading