CBMC proof projects

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. These developers, who had little more hands-on experience than 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. Choose some location within the repository to create a cbmc directory to hold the CBMC verification work.

mkdir cbmc
cd cbmc
cbmc-starter-kit-setup

What is the project name? Kernel

The first line creates 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 the repository for the CBMC verification of a particular function. The function we want to verify is 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 /proj/kernel/portable/ARMv8M/secure/heap/secure_heap.c
   1 /proj/kernel/portable/GCC/ARM_CM23/secure/secure_heap.c
   2 /proj/kernel/portable/GCC/ARM_CM33/secure/secure_heap.c
   3 /proj/kernel/portable/GCC/ARM_CM55/secure/secure_heap.c
   4 /proj/kernel/portable/IAR/ARM_CM23/secure/secure_heap.c
   5 /proj/kernel/portable/IAR/ARM_CM33/secure/secure_heap.c
   6 /proj/kernel/portable/IAR/ARM_CM55/secure/secure_heap.c
   7 /proj/kernel/portable/MemMang/heap_1.c
   8 /proj/kernel/portable/MemMang/heap_2.c
   9 /proj/kernel/portable/MemMang/heap_3.c
  10 /proj/kernel/portable/MemMang/heap_4.c
  11 /proj/kernel/portable/MemMang/heap_5.c
  12 /proj/kernel/portable/WizC/PIC18/port.c
  13 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, 12, 13): 11

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 11.

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. In the directory containing the proof, we run

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.

Run all the proofs

To run a single proof, as we have already seen, just change to the directory containing the proof and run

make
open report/html/index.html

to run the proof and open a summary of the results in a web browser.

To run all proofs in the repository, there a script installed by the starter kit that will run all proofs in the repository and summarize the results in a report that you can open in a web browser. Just change to the directory cbmc/proofs and run the script with

run-cbmc-proofs.py

When the script is done it will print a line like

Report was rendered at file:////repository/cbmc/proofs/output/latest/html/index.html

You can open this report in a web browser

open file:////repository/cbmc/proofs/output/latest/html/index.html

and see a summary of the results. The results will list the proofs that failed at the top. For each proof, you can click within the column labeled "Report" to see the same html report you would see if you ran the proof on its own. You can also click on the "pipeline" icon on the left to see the logs for each stage in the pipeline that built the code and ran the proof.

This run script is the script to run from continuous integration. Continuous integration can run this script and use the report it generates to report the results back to the users.