Skip to content

Install CBMC starter kit

Jump to bottom
Mark R. Tuttle edited this page Oct 28, 2020 · 4 revisions

The CBMC starter kit is a collection of templates and scripts that make it easy for you to start writing proofs of C code with CBMC. Installing and using the starter kit consists of three steps:

For your own convenience, to simplify these instructions, set three environment variables:

  • SRCDIR: This is the root of the source tree. It can be anything, but it is typically the root of a GitHub repository.

    export SRCDIR=/usr/project

  • CBMC_ROOT: This is the root of the subtree containing the CBMC proof infrastructure installed by this starter kit. It can be anything, but it is particularly convenient if it is a directory somewhere under the source root. For example, it could be a directory along with other directories containing your unit tests.

    export CBMC_ROOT=${SRCDIR}/cbmc

  • PROOF_ROOT: This is the root of the subtree containing the CBMC proofs themselves. This must be the proofs subdirectory of CBMC_ROOT.

    export PROOF_ROOT=${CBMC_ROOT}/proofs

Install the starter kit

  • Install the starter kit itself.

    cd ${CBMC_ROOT}
git submodule add https://github.com/awslabs/aws-templates-for-cbmc-proofs.git aws-templates-for-cbmc-proofs

  • Install litani, a build tool used by the starter kit that makes it easy to build and check proofs concurrently.

    cd ${CBMC_ROOT}
git submodule add https://github.com/awslabs/aws-build-accumulator.git litani

  • Install ninja, a build tool used by litani.

    On MacOS:   brew install ninja
On Ubuntu:  sudo apt-get install ninja-build
On Windows: Download from https://github.com/ninja-build/ninja/releases

Set up the proof infrastructure

To set up the proof infrastructure, run the script scripts/setup.py. It will ask you for the source root (which is ${SRCDIR}) and it will ask you for the path to the litani executable (which is ${CBMC_ROOT}/litani/litani using the names chosen in the instructions above).

For example,

cd ${CBMC_ROOT}
python3 aws-templates-for-cbmc-proofs/scripts/setup.py
  What is the path to the source root? /usr/project
  What is the path to the litani script? ./litani/litani

The script will install four directories:

  • include: Extra include files for your proofs go here.
  • sources: Extra source code for your proofs goes here. For example, you might write a method allocate_header to allocate a header struct taken as input by several of the functions you are proving correct.
  • stubs: Stubs for your proofs go here. For example, you might write stubs read and write for the methods used to read and write a device controlled by several of the functions you are proving correct.
  • proofs: This is the subtree containing your proofs. This is the root of the proof subtree denoted by PROOF_ROOT in the instructions above.

The script will install four Makefiles:

  • proofs/Makefile.common: Do not edit this makefile. It encodes how to build and check proofs with CBMC using what we consider to be best practices. You will be able to build and check your proof with just make report. The makefile, however, does define four targets you may find helpful:
    • make goto: Compile your code and build the goto binary used by CBMC.
    • make result: Do property checking (eg, check for buffer overflow with CBMC).
    • make coverage: Do coverage checking (eg, compute the lines of code exercised by CBMC).
    • make report: Generate a report summarizing the results of CBMC with CBMC viewer.
  • proofs/Makefile-project-defines: Edit this makefile to configure the starter kit for your project. Three definitions are particularly important:
    • COMPILE_FLAGS: The list of flags your project passes to the compiler.
    • INCLUDES: The list of include directories your project uses.
    • DEFINES: The list of preprocessor definitions your project uses.
  • proofs/Makefile-project-targets: Edit this makefile only if there are targets useful to your project that are not in Makefile.common.

Set up the proof harnesses

For each proof, run the script scripts/setup-proof.py to create a directory containing all the files you need to write a proof for a functions. The script will ask you for

  • The name of the function under test.
  • The path to the source file defining the function under test.
  • The path to the source root (which is ${SRCDIR}).
  • The path to the proof root (which is ${CBMC_ROOT}/proofs).
cd ${CBMC_ROOT}
python3 aws-templates-for-cbmc-proofs/scripts/setup-proof.py
  What is the function name? device_read
  What is the path to the source file defining the function? /usr/project/src/device.c
  What is the path to the source root? /usr/project
  What is the path to the 'proofs' directory (usually '.')? .

The script will use the function name FUNCTION you that you give to create a directory FUNCTION. Files in that directory include:

  • FUNCTION_harness.c: This is a template for the proof harness for the function FUNCTION.
  • Makefile: This is a template for the Makefile to build and check your proof (using ../Makefile.common described above).

That this point you should be able to cut-and-paste into these templates, type make report, and being debugging your first proof!

You can cut and paste into the files, and type make to run and debug the proof.

Clone this wiki locally