Getting started with the CBMC starter kit

The CBMC starter kit makes it easy to add CBMC verification to an existing software project.

CBMC is a model checker for C. This means that CBMC will explore all possible paths through your code on all possible inputs, and will check that all assertions in your code are true. CBMC can also check for the possibility of memory safety errors (like buffer overflow) and for instances of undefined behavior (like signed integer overflow). CBMC is a bounded model checker, however, which means that the set of all possible inputs may have to be restricted to all inputs of some bounded size.

For a quick start on using the starter kit, see

• Installation
• Tutorial

Installation

The starter kit is a command line tool distributed as both a brew package and a pip package. The starter kit release page gives installation instructions that we repeat here.

Note: The starter kit used to be distributed as a git repository that you submoduled into your own repository. The starter kit is now distributed as a command line tool. Follow the update instructions below to upgrade your project from using the submodule to using the command line tool.

Installing with brew

On MacOS, we recommend using brew to install the starter kit:

brew tap aws/tap
brew install cbmc-starter-kit cbmc-viewer litani

The brew home page gives instructions for installing brew. The command brew tap aws/tap taps the AWS repository that contains the brew packages. The cbmc-viewer and litani packages are tools used by the starter kit. See the cbmc-viewer release page and the litani release page for other ways to install them if you don't want to use brew.

Installing with pip

On any machine, you can use pip to install the starter kit:

python3 -m pip install cbmc-starter-kit cbmc-viewer

The python download page gives instructions for installing python and pip. The cbmc-viewer and litani packages are tools used by the starter kit. See the cbmc-viewer release page and the litani release page for installation instructions (we used pip to install cbmc-viewer in the command above).

Installing for developers

Developers can install the package in "editable mode" which makes it possible to modify the code in the source tree and then run the command from the command line as usual to test the changes. First, install cbmc-viewer and litani as described above if you haven't already. Then

• Clone the repository and install dependencies with

  git clone https://github.com/model-checking/cbmc-starter-kit cbmc-starter-kit
  python3 -m pip install virtualenv gitpython
  

• Install into a virtual environment with

  cd cbmc-starter-kit
  make develop
  

  At this point you can either activate the virtual environment with

  source /tmp/cbmc-starter-kit/bin/activate
  

  or simply add the virtual environment to your path with

  export PATH=/tmp/cbmc-starter-kit/bin:$PATH
  

• Uninstall with

  cd cbmc-starter-kit
  make undevelop
  

Updating

To update to the the latest version of the starter kit:

• Update the starter kit itself with

  brew upgrade cbmc-starter-kit
  

  or

  python3 -m pip install cbmc-starter-kit --upgrade
  

• Update your repository by changing to the cbmc directory that contains the proofs directory installed by the starter kit and running the update script:

  cd cbmc
  cbmc-starter-kit-update
  

  This will overwrite Makefile.common and run-cbmc-proofs.py in the proofs directory with the latest versions.

Updating to the command line tool

The starter kit used to be distributed as a git repository that you submoduled into your own repository. The same used to be true for litani, the build tool used by the starter kit. Now both are distributed a command line tools. We recommend that you migrate to using these command line tools.

• Install the starter kit and litani as command line tools

  • On MacOS

    brew install cbmc-starter-kit litani
    

  • On Ubuntu, first download the litani debian package from the litani release page then

    python3 -m pip install cbmc-starter-kit
    apt install ./litani-*.deb
    

• Change to the cbmc directory that contains the proofs directory installed by the starter kit, and run the update script

  cd cbmc
  cbmc-starter-kit-update --remove-starter-kit-submodule --remove-litani-submodule
  

  This will overwrite Makefile.common and run-cbmc-proofs.py in the proofs directory with the latest versions, and remove the submodules for the starter kit and litani if they are present. It will also perform some cleanup actions, such as replacing symbolic links into the starter kit submodule with copies of the files being linked to, and removing a set of negative tests that are rarely used.

  See cbmc-starter-kit-update for more information.

While you are at it, we have changed the starter kit license from Apache 2.0 to MIT-0, and you might want to run a script to change copyright headers from Apache to MIT in files under the cbmc directory:

cd cbmc
cbmc-starter-kit-migrate-license --remove

See cbmc-starter-kit-migrate-license for more information.

Installation notes

If you have difficulty installing these tools, please let us know by submitting a GitHub issue.

CBMC starter kit tutorial

The CBMC starter kit makes it easy to add CBMC verification to an existing software project.

In this tutorial, we show how to begin proving the memory safety of a memory allocator that comes with the FreeRTOS Kernel. The kernel comes with five allocators, and we look at the simplest one. It allocates blocks from a region of memory set aside for the heap. It maintains a linked list of free blocks and allocates a block from the first block in the free list that is big enough to satisfy the request. When the block is freed, it is added back to the free list and merged with adjacent free blocks already in the free list. The function we want to prove memory safe is the allocator pvPortMalloc in the source file portable/MemMang/heap_5.c.

This tutorial is actually a slightly cleaned-up version of the work done by two developers who used the starter kit to begin verification of pvPortMalloc. Two developers who had little more hand-on experience that the demonstration of CBMC running on a few simple examples were able to use the starter kit to begin verification in about ten or fifteen minutes, and were able to breathe some real life into the proof within a few more hours.

Using the starter kit consists of five steps

• Clone the source repository
• Configure the repository
• Configure the proof
• Write the proof
• Run the proof

Clone the source repository

The first step is to clone the FreeRTOS Kernel repository.

git clone https://github.com/FreeRTOS/FreeRTOS-Kernel.git kernel
cd kernel
git submodule update --init --checkout --recursive

The first line clones the repository into the directory kernel. The remaining lines step into the directory kernel and clone the kernel's submodules.

Configure the repository

The next step is to configure the repository for CBMC verification.

mkdir cbmc
cd cbmc
cbmc-starter-kit-setup

What is the project name? Kernel

The first line create a cbmc directory to hold everything related to CBMC verification. The last line runs a setup script to configure the repository for CBMC verification. It examines the layout of the repository and asks for a name to use for the CBMC verification project. We use the project name Kernel.

Looking at the cbmc directory, we see that some infrastructure has been installed:

ls

include         proofs          sources         stubs

We see directories for holding header files, source files, and stubs written for the verification work. Examples of useful stubs for a verification project are send and receive methods for a physical communication network that isn't being explicitly modeled.

The most important directory here is the proofs directory that will hold the CBMC proofs themselves:

ls proofs

Makefile-project-defines        Makefile.common
Makefile-project-targets        README.md
Makefile-project-testing        run-cbmc-proofs.py
Makefile-template-defines

The most important files here are

• Makefile.common This makefile implements our best practices for CBMC verification: our best practices for building code for CBMC, our best practices for running CBMC, and for building a report of CBMC results in a form that makes it easy to debug issues found by CBMC.
• run-cbmc-proofs.py This python script runs all of the CBMC proofs in the proofs directory with maximal concurrency, and builds a dashboard of the results. This script is invoked by continuous integration to recheck the proofs on changes proposed in a pull request.

The remaining Makefiles are just hooks for describing project-specific modifications or definitions. For example, within Makefile-project-defines you can define the INCLUDES variable to set the search path for the header files needed to build the project functions being verified.

Configure the proof

The next step is to configure CBMC verification of the memory allocator pvPortMalloc in the source file portable/MemMang/heap_5.c.

cd proofs
cbmc-starter-kit-setup-proof

What is the function name? pvPortMalloc
These source files define a function 'pvPortMalloc':
   0 ../../portable/ARMv8M/secure/heap/secure_heap.c
   1 ../../portable/GCC/ARM_CM23/secure/secure_heap.c
   2 ../../portable/GCC/ARM_CM33/secure/secure_heap.c
   3 ../../portable/IAR/ARM_CM23/secure/secure_heap.c
   4 ../../portable/IAR/ARM_CM33/secure/secure_heap.c
   5 ../../portable/MemMang/heap_1.c
   6 ../../portable/MemMang/heap_2.c
   7 ../../portable/MemMang/heap_3.c
   8 ../../portable/MemMang/heap_4.c
   9 ../../portable/MemMang/heap_5.c
  10 ../../portable/WizC/PIC18/port.c
  11 The source file is not listed here
Select a source file (the options are 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11): 9

This runs a setup script for the proof that first asks for the name of the function being verified. We give it the name pvPortMalloc. It then examines the source code in the repository and lists all of the source files that define a function named pvPortMalloc. It lists these files and asks us to chose the file with the implementation we want to verify. We choose source file number 9.

The proofs directory now contains a subdirectory pvPortMalloc for verification of the memory allocator pvPortMalloc.

cd pvPortMalloc
ls

Makefile                cbmc-proof.txt          pvPortMalloc_harness.c
README.md               cbmc-viewer.json

The most important files in this directory are

• Makefile This is a skeleton of a Makefile to build and run the proof.
• pvPortMalloc_harness.c This is a skeleton of a proof harness for pvPortMalloc.

Write the proof

The Makefile

The Makefile is very simple.

HARNESS_ENTRY = harness
HARNESS_FILE = pvPortMalloc_harness

# This should be a unique identifier for this proof, and will appear on the
# Litani dashboard. It can be human-readable and contain spaces if you wish.
PROOF_UID = pvPortMalloc

DEFINES +=
INCLUDES +=

REMOVE_FUNCTION_BODY +=
UNWINDSET +=

PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/portable/MemMang/heap_5.c

# If this proof is found to consume huge amounts of RAM, you can set the
# EXPENSIVE variable. With new enough versions of the proof tools, this will
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
# documentation in Makefile.common under the "Job Pools" heading for details.
# EXPENSIVE = true

include ../Makefile.common

You can see that it identifies the the function pvPortMalloc, it identifies the source file portable/MemMang/heap_5.c, and it includes the Makefile.common describing our best practices for using CBMC.

It also gives us the option of defining INCLUDES to set the include path for header files. We do need a few header files to build pvPortMalloc, so let us update the Makefile with

INCLUDES += -I$(PROOFDIR)
INCLUDES += -I$(SRCDIR)/include
INCLUDES += -I$(SRCDIR)/portable/ThirdParty/GCC/Posix

The final Makefile is:

HARNESS_ENTRY = harness
HARNESS_FILE = pvPortMalloc_harness

# This should be a unique identifier for this proof, and will appear on the
# Litani dashboard. It can be human-readable and contain spaces if you wish.
PROOF_UID = pvPortMalloc

DEFINES +=
INCLUDES += -I$(PROOFDIR)
INCLUDES += -I$(SRCDIR)/include
INCLUDES += -I$(SRCDIR)/portable/ThirdParty/GCC/Posix

REMOVE_FUNCTION_BODY +=
UNWINDSET +=

PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/portable/MemMang/heap_5.c

# If this proof is found to consume huge amounts of RAM, you can set the
# EXPENSIVE variable. With new enough versions of the proof tools, this will
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
# documentation in Makefile.common under the "Job Pools" heading for details.
# EXPENSIVE = true

include ../Makefile.common

The proof harness

The proof harness is also very simple (especially after omitting some comments at the top of the file).

/**
 * @file pvPortMalloc_harness.c
 * @brief Implements the proof harness for pvPortMalloc function.
 */

void harness()
{

  /* Insert argument declarations */

  pvPortMalloc( /* Insert arguments */ );
}

We need to add the main header file FreeRTOS.h for the FreeRTOS project, and we need to add a function prototype for pvPortMalloc saying that it takes a size and returns a pointer.

#include <stdlib.h>
#include "FreeRTOS.h"
void *pvPortMalloc(size_t size);

All that is left is to declare an unconstrained size of type size_t and pass it to pvPortMalloc.

size_t size;
pvPortMalloc(size);

The final pvPortMalloc_harness.c is:

/**
 * @file pvPortMalloc_harness.c
 * @brief Implements the proof harness for pvPortMalloc function.
 */

#include <stdlib.h>
#include "FreeRTOS.h"
void *pvPortMalloc(size_t size);

void harness()
{
  size_t size;
  pvPortMalloc(size);
}

And that is it, with the exception of one last detail. Building FreeRTOS requires a configuration file that sets all the parameters used to define a system configuration. This kernel repository does not contain a configuration file, so let us use a simplified configuration file from a demonstration in another repository. Let us add FreeRTOSConfig.h to the pvPortMalloc directory.

Run the proof

Finally, we can run the proof:

make

This builds a report of the results that we can open in a browser

open report/html/index.html

Examining the report, we see a list of coverage results, a list of warnings, and a list of errors or issues found by CBMC. In this report, there are no errors, but the coverage is terrible: only 40% of the lines in the function are exercised by CBMC!

Further thought makes it clear that we haven't set up the heap that the allocator is supposed to be using. We have invoked an allocator to allocate space on a heap, but we haven't allocated or initialized the heap itself yet!

At this point it is interesting to see what the developers did to breathe some life into this verification effort. Their proof harness looked something like this pvPortMalloc_harness.c:

/**
 * @file pvPortMalloc_harness.c
 * @brief Implements the proof harness for pvPortMalloc function.
 */

#include <stdlib.h>
#include "FreeRTOS.h"
void * pvPortMalloc( size_t xWantedSize );

void harness()
{
  /* allocate heap */
  uint8_t app_heap[ configTOTAL_HEAP_SIZE ];

  /* initialize heap */
  HeapRegion_t xHeapRegions[] =
    {
      { ( unsigned char * ) app_heap, sizeof( app_heap ) },
      { NULL,                         0                  }
    };
  vPortDefineHeapRegions( xHeapRegions );

  /* mess up heap */
  size_t xWantedSize1, xWantedSize2, xWantedSize3;
  void* pv1 = pvPortMalloc( xWantedSize1 );
  void* pv2 = pvPortMalloc( xWantedSize2 );
  void* pv3 = pvPortMalloc( xWantedSize3 );
  vPortFree( pv2 );

  size_t xWantedSize;
  pvPortMalloc( xWantedSize );
}

You can see that they allocate the heap, they initialize the heap data structures, and then they mess up the heap a bit by allocating three chunks of unconstrained size and freeing the middle one. Then they invoke pvPortMalloc with an unconstrained size. Doing this was enough to get complete code coverage and uncover a few minor instances of integer overflow.

Of course, this is not a complete proof of memory safety. This is a proof that if you allocate a heap consisting of a single chunk of memory of a size fixed by the configuration, and if you allocate three chunks of unconstrained size and free the middle one, then pvPortMalloc will exhibit no memory safety errors or other undefined behaviors. But it is an elegant example of how quickly developers were able to get started doing real work. Good for them! And, soon, good for you.

Reference manual

The CBMC Starter Kit makes it easy to add CBMC verification to a software project.

• cbmc-starter-kit-setup
• cbmc-starter-kit-setup-proof
• cbmc-starter-kit-update
• cbmc-starter-kit-migrate-license

Reference manual

Name

cbmc-starter-kit-setup - Set up CBMC proof infrastructure for a repository

Synopsis

cbmc-starter-kit-setup [-h] [--verbose] [--debug] [--version]

Description

This script sets up the CBMC proof infrastructure for a repository. It locates the root of the repository, it asks for a name to use for the CBMC verification activity (any name will do, and the name can be changed at any time), and it copies into the current directory a collection of files that simplify getting started with CBMC.

We recommend that you create a directory with a name like cbmc somewhere within the repository to hold the CBMC verification work. This script assumes that it is running in this verification directory, and assumes that this directory is under the root of a git repository.

This script needs to be run only one time to prepare the repository for CBMC verification.

Options

--verbose

• Verbose output.

--debug

• Debugging output.

--version

• Display version number and exit.

--help, -h

• Print the help message and exit.

Reference manual

Name

cbmc-starter-kit-setup-proof - Set up CBMC proof infrastructure for a proof

Synopsis

cbmc-starter-kit-setup-proof [-h] [--verbose] [--debug] [--version]

Description

This script sets up the CBMC proof infrastructure for an individual proof. It asks for the name of the function under test. It then searches the repository for source files that define a function with that name, and asks you to select the file giving the implementation you want to test. If none of the files listed is the correct file, you can give the path to the correct source file yourself. Finally, the script creates a directory with the name of the function and copies into that directory some files to simplify getting started with the verification of that function. Most important, it copies a skeleton of a Makefile and skeleton of a proof harness that you can edit to get started.

This script is usually run in the CBMC verification root (the directory you created to hold the CBMC verification work, and in which you ran the cbmc-stater-kit-setup script). This script can, however, be run in any subdirectory of the CBMC verification root. In this way, you can group verification of similar functions together in a hierarchy of subdirectories.

This script will need to be run once for each function you want to verify.

Options

--verbose

• Verbose output.

--debug

• Debugging output.

--version

• Display version number and exit.

--help, -h

• Print the help message and exit.

Reference manual

Name

cbmc-starter-kit-update - Update CBMC starter kit in a CBMC proof repository

Synopsis

cbmc-starter-kit-update [-h] [--cbmc-root CBMC]
                        [--starter-kit-root STARTER_KIT] [--no-migrate]
                        [--no-test-removal] [--no-update]
                        [--remove-starter-kit-submodule]
                        [--remove-litani-submodule] [--verbose]
                        [--debug] [--version]

Description

This script is used to update the CBMC starter kit installed in your repository to the lastest version. It copies (overwrites) two files into your repository (Makefile.common and run-cbmc-proofs.py). These are the two files in the starter kit that encode our best practices for how to use CBMC in a software verification project.

This script will also migrate your repository from early versions of the starter kit and litani (the build system used by the starter kit) to modern versions. Early versions of the starter kit and litani were distributed as as git repositories that you submoduled into your repository. The starter kit also installed symbolic links from your repository into the starter kit submodule. This script will remove the symbolic links (replace them with the files they are linking to) and will also remove the starter kit and litani submodules from your repository if you give the --remove-stater-kit-submodule and --remove-litani-submodule flags (flags you almost certainly want to use during the migration). Finally, it will remove some regression tests that were distributed with early versions of the starter kit that most people don't use.

Options

--cbmc-root CBMC

• Root of CBMC proof infrastructure (default: ".")

--starter-kit-root STARTER_KIT

• Root of CBMC starter kit submodule (default: None or root of starter kit submodule installed in repository containing CBMC)

--no-migrate

• Do not remove symlinks under CBMC. Normally remove symlinks under CBMC to files under STARTER_KIT.

--no-test-removal

• Do not remove negative tests in CBMC/negative_tests. Normally remove the directory CBMC/negative_tests since most projects don't use these tests.

--no-update

• Do not update Makefile.common and run-cbmc-proofs.py under CBMC/proofs. Normally update these files with the versions in the starter kit package.

--remove-starter-kit-submodule

• Remove the starter kit submodule if it is present. Normally just recommend removal.

--remove-litani-submodule

• Remove the litani submodule and update the definition of LITANI in Makefile-template-defines if the litani submodule is present and the litani command is in PATH. Normally just recommend removal.

--verbose

• Verbose output

--debug

• Debug output

--version

• Display version and exit

--help, -h

• Print the help message and exit.

Reference manual

Name

cbmc-starter-kit-migrate-license - Remove references to Apache license from CBMC starter kit.

Synopsis

cbmc-starter-kit-migrate-license [-h] [--proofdir PROOFDIR] [--remove]
                                 [--verbose] [--debug] [--version]

Description

This script is used to remove references to the Apache license installed by early versions of the starter kit.

The CBMC starter kit was originally released under the Apache license. All files in the starter kit contained references to the Apache license. The starter kit installation scripts copied files from the stater kit into the project repository. This became an issue when the project repository was released under a more permissive license. This script removes all references to the Apache license from the files copied into the project repository from the starter kit, and uses the MIT-0 license instead.

Options

--proofdir PROOFDIR

• Root of the proof subtree (default: .)

--remove

• Remove Apache references from files under PROOFDIR (otherwise just list them)

--help, -h

--verbose

• Verbose output.

--debug

• Debugging output.

--version

• Display version number and exit.

CBMC starter kit resources

• CBMC (the model checker used by the starter kit)

  • Documentation and tutorial
  • Source code

• Litani (the build system used by the starter kit)

  • Documentation
  • Source code

• CBMC starter kit

  • Source code

Contributing

This material is a work in progress. If you have suggestions, corrections, or questions, contact us by submitting a GitHub issue. If you have some examples of your own that you would like to contribute, submit your contributions as a GitHub pull request.