The Intel TDX Module Benchmark Set

This archive contains the source code of Intel TDX Module (intel-tdx/src/; version 1.5.05), the developed proof harnesses (intel-tdx/formal/), the derived verification tasks (default-size*/), and the scripts and tools for generating verification tasks (scripts/ and harnessforge/). Verification Tasks The verification tasks derived from the Intel TDX Module are located in the directories default-size/ and default-size-eager-init/. These two sets differ in how state variables are initialized. Within each directory, subdirectories contain tasks that use different initialization strategies for mock variables. Please refer to Configurable Flags for more details. Files with suffix *.i are the single-file, self-contained verification tasks assembled by HarnessForge. The task-definition YAML files include additional information, such as the expected verdict (true for the safety tasks where the postcondition holds; false for tasks where the inserted reachability label is reachable). Task Generation Before starting the task-generation process, please ensure that the submodule intel-tdx/ has been initialized and the required dependencies for HarnessForge are installed. To generate verification tasks from the selected interface function and check their syntax, run the following command from the directory intel-tdx/: ../scripts/generate_tasks.sh <config YAML file(s)> [-d <-DTDXFV_FLAGS>] [-o <output path>] [-s <suffix>] Example command: ../scripts/generate_tasks.sh formal/config/tdh_sys_config_config.yml -d "-DTDXFV_KLEE_MAKE_SYMBOLIC" -o ../default-size/klee_make_symbolic -s klee_make_symbolic (You may need to clean the output folder with the flag --clean if it is not empty.) Configurable Flags The generation script supports the following configurable flags: Mock variable initialization (mutually exclusive): <None> (default): use object havocking TDXFV_HAVOC_MEMORY: use byte-wise memory havocking TDXFV_CPROVER_HAVOC_OBJECT: use __CPROVER_havoc_object TDXFV_ESBMC_INIT_OBJECT: use __ESBMC_init_object TDXFV_KLEE_MAKE_SYMBOLIC: use klee_make_symbolic State initialization: <None> (default): initialize only the state variables required by the respective interface function TDXFV_EAGER_INIT: eagerly initialize all state variables