CBMC quick start

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, and using CBMC may require restricting inputs to inputs of some bounded size. The result is assurance that your code behaves as expected for all such inputs.

CBMC has been used on over a dozen industrial software verification projects as a routine part of software development and continuous integration. This experience has resulted in some "best practices" for how to build software for CBMC and how to run CBMC in development. The CBMC starter kit is an implementation of these best practices, and is intended to make it easy to deploy CBMC to a software project as part of software development and continuous integration.

This document is a guide to using CBMC and to deploying CBMC to an industrial software verification project.

Getting started

For a quick start on writing proofs that includes simple exercises, read

• CBMC installation
• CBMC as unit testing
• CBMC as debugging
• CBMC proofs

For a quick start on deploying CBMC to a software project, we recommend that you read our tutorial, but if you want to dive right in, you can install the tools and

• Read configure the repository to set up a software repository for CBMC proof
• Read configure the proof to add a new CBMC proof to an existing set of CBMC proofs
• Read run all proofs to run a set of existing CBMC proofs and examine the results.

For advice on planning and managing a CBMC proof project, read CBMC project management.

To learn more, see our list of CBMC resources and CBMC projects, and see

• CBMC starter kit reference manual and documentation
• CBMC viewer reference manual and documentation
• CBMC developer guide
• Litani reference manual

Helping others

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

CBMC installation

MacOS

On MacOS, we recommend installing with brew. Install with

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

The brew home page gives instructions for installing brew. The first command taps the AWS repository that contains some of the brew packages, and the second command installs the packages. Installing ctags is recommended but optional, see below.

Ubuntu

On Ubuntu, we recommend installing by downloading the cbmc and litani installation packages for your operating system from the CBMC release page and the Litani release page. Install with

sudo apt install python3 python3-pip *cbmc*.deb *litani*.deb universal-ctags
python3 -m pip install cbmc-viewer cbmc-starter-kit

The python download page gives instructions for installing python and pip. Installing ctags is recommended but optional, see below. The pip installation packages for cbmc-viewer and cbmc-starter-kit can be used on any machine with python3 including MacOS.

Windows

On Windows, we recommend using the Windows Subsystem for Linux (WSL) and using the Ubuntu instructions above. CBMC and CBMC viewer will run natively on Windows, but Litani and the CBMC starter kit that depends on Litani are not supported on Windows. To install natively on Windows (without using WSL), download the Windows installation package from the CBMC release page and run

python3 -m pip install cbmc-viewer
msiexec /i cbmc*.msi
PATH="C:\Program Files\cbmc\bin";%PATH%

Installation notes

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

The installation of ctags is optional, but without ctags, cbmc-viewer will fail to link some symbols appearing in error traces to their definitions in the source code. The ctags tool has a long history. The original ctags was replaced by exuberant ctags which was replaced by universal ctags. Any version will work better than none, but we recommend universal ctags.

CBMC as unit testing

Think of CBMC as a form of unit testing: If you can write a unit test, then you can write a CBMC proof. One of the things we can do with unit testing is to run a function on a set of inputs, and to compare the result with the expected result. Think of CBMC as a unit tester that runs the function on all possible inputs.

Here is a function quartile from quartile.c that returns the quartile of an integer between 0 and 99.

int quartile(int x) {
  int y;

  if (x < 0 || x > 99) return 0;

  if (x < 50)
    if (x < 25)
      y = 1;
    else
      y = 2;
  else
    if (x < 75)
      y = 3;
    else
      y = 4;

  return y;
}

Here a unit test from unit-test.c that tests quartile using a number from the first quartile.

#include <assert.h>
int quartile(int x);

int main() {
  int x = 1;
  int result = quartile(x);
  assert(result == 1);
}

We can build the unit test with gcc and run it. When we do, the unit test runs successfully, and the assertion does not fail:

gcc quartile.c unit-test.c -o unit-test
./unit-test

We can also build the unit test with goto-cc, which is a drop-in replacement for gcc that comes with CBMC. Now we can use CBMC to run the unit test, and again the assertion does not fail:

goto-cc quartile.c unit-test.c -o unit-test
cbmc ./unit-test

** Results:
unit-test.c function main
[main.assertion.1] line 8 assertion result == 1: SUCCESS

** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL

For examples as simple as this, we can actually run CBMC directly on the source files (without explicitly invoking goto-cc):

cbmc quartile.c unit-test.c

** Results:
unit-test.c function main
[main.assertion.1] line 8 assertion result == 1: SUCCESS

** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL

But now we can do something interesting with CBMC. The unit test currently initializes the variable x to 1, and CBMC considers 1 to be the initial value of x. If we remove the initializer, CBMC allows any integer value to be the initial value of x. This is a general rule: If CBMC encounters an uninitialized variable, then CBMC allows any value from the variable's type to be the variable's initial value. We say that CBMC treats uninitialized variables as having unconstrained initial values.

If we rewrite the unit test

#include <assert.h>
int quartile(int x);

int main() {
  int x; // The value of x is now any value of type int
  int result = quartile(x);
  assert(result == 1);
}

and rerun CBMC

cbmc quartile.c unit-test.c

** Results:
unit-test.c function main
[main.assertion.1] line 8 assertion result == 1: FAILURE

** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

we can see that the assertion has failed. We can ask CBMC to produce an error trace that demonstrates one way in which the assertion can fail

cbmc quartile.c unit-test.c --trace

** Results:
unit-test.c function main
[main.assertion.1] line 8 assertion result == 1: FAILURE

Trace for main.assertion.1:

State 21 file unit-test.c function main line 6 thread 0
----------------------------------------------------
  x=-2147483547 (10000000 00000000 00000000 01100101)

State 22 file unit-test.c function main line 7 thread 0
----------------------------------------------------
  result=0 (00000000 00000000 00000000 00000000)

State 26 file unit-test.c function main line 7 thread 0
----------------------------------------------------
  x=-2147483547 (10000000 00000000 00000000 01100101)

State 27 file quartile.c function quartile line 2 thread 0
----------------------------------------------------
  y=0 (00000000 00000000 00000000 00000000)

State 33 file unit-test.c function main line 7 thread 0
----------------------------------------------------
  result=0 (00000000 00000000 00000000 00000000)

Violated property:
  file unit-test.c function main line 8 thread 0
  assertion result == 1
  !((signed long int)(signed long int)!(result == 1) != 0l)

** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

and we see that in the first step of this error trace the variable x is initialized to the integer value x=-2147483547.

Well, that's not quite what we intended, but we don't expect quartile to return 1 on every integer, just on integers in the first quartile. We can constrain x to be an integer in the first quartile by adding an assumption to the unit test:

#include <assert.h>
int quartile(int x);

int main() {
  int x;
  __CPROVER_assume(0 <= x && x < 25);    // this is a precondition
  int result = quartile(x);
  assert(result == 1);                   // this is a postcondition
}

Rerunning CBMC, we see that the assertion is always true:

cbmc quartile.c unit-test.c

** Results:
unit-test.c function main
[main.assertion.1] line 9 assertion result == 1: SUCCESS

** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL

Let's pause for a moment to notice that we have already done something interesting. We have proved that the function quartile returns 1 when it is called on any integer in the first quartile. We have partially specified the behavior of the function using a precondition (the assumption that x is in the first quartile) and a postcondition (the assertion that the return value is 1). If the function is called with an input that satisfies the precondition, then the function returns with a value that satisfies the postcondition. Of course, we have only partially specified the behavior of the function. What happens when it is called with an integer in the second quartile? The specification doesn't say. But we have taken the first step toward specification and verification of our function.

CBMC as debugging

Think of CBMC as a form of debugging: CBMC does an exhaustive search for issues affecting functional correctness and memory safety. Let's look at a few examples of the kinds of things that CBMC can find.

Memory safety

The source code in memory-safety.c

#define SIZE 20
char buffer[SIZE];

char read_buffer(int i)  { return buffer[i];     }
char read_pointer(int i) { return *(buffer + i); }

int main() {
  int index;
  read_buffer(index);
  read_pointer(index);
}

allocates a buffer of 20 characters and defines two functions that return a character from the buffer. The first function read_buffer uses array indexing to access the character. The second function read_pointer uses pointer dereferencing. Neither function does any bounds checking. The main function declares an integer-valued index and invokes the two functions to access the character at this index. The fact that index is uninitialized is significant to CBMC: When CBMC sees an uninitialized variable, it considers as possible values for that variable all values a variable of that type can assume.

If you ask CBMC to check buffer accesses,

cbmc memory-safety.c --bounds-check

CBMC reports violations of both the lower and upper bounds of the array (because index can assume both negative and positive values):

line 3 array 'buffer' lower bound in buffer[(signed long int)i]: FAILURE
line 3 array 'buffer' upper bound in buffer[(signed long int)i]: FAILURE

If you ask CBMC to check pointer dereferencing,

cbmc memory-safety.c --pointer-check

CBMC reports that the pointer can point outside the bounds of the buffer:

line 4 dereference failure:
  pointer outside object bounds in buffer[(signed long int)i]: FAILURE

If you ask CBMC to produce an error trace,

cbmc memory-safety.c --pointer-check  --trace

you get a step-by-step execution of the program leading to the error, and the trace ends with the following steps:

State 42 file memory-safety.c function main line 7 thread 0
----------------------------------------------------
  index=21 (00000000 00000000 00000000 00010101)

State 45 file memory-safety.c function main line 8 thread 0
----------------------------------------------------
  i=21 (00000000 00000000 00000000 00010101)

State 49 file memory-safety.c function main line 9 thread 0
----------------------------------------------------
  i=21 (00000000 00000000 00000000 00010101)

Violated property:
  file memory-safety.c function read_pointer line 4 thread 0
  dereference failure: pointer outside object bounds in buffer[(signed long int)i]
  (signed long int)i >= 0l && !((unsigned long int)(signed long int)i + 1ul >= 21ul)

CBMC is saying in step 42 that if you choose the value 21 for the index, then *(buffer + index) points to a location outside the 20-character buffer.

Termination

The source code in termination.c

#include <stdlib.h>
int main() {
  size_t initial_size;
  size_t requested_size;

  size_t size = initial_size;
  while (size < requested_size) {
    size *= 2;
  }
}

illustrates a bug found with CBMC that actually required some unexpected code changes. This example reduces the problem to a single loop from an allocator, and makes the mistake more obvious than it was in the original code. The allocator begins with an initial (recommended) size for chunk allocation, and repeatedly doubles this size until it is large enough to hold the requested size. Each iteration of the loop doubles the size (shifts the size left by one bit) until the size overflows to 0. Once the size is 0, doubling the size results in 0, and the loop never ends.

How would you find this with CBMC (without already knowing the problem exists)? If you run simply CBMC with

cbmc termination.c

CBMC will go on forever unwinding the loop forever because it cannot easily tell from the source code how many times the loop iterates.

You can coach CBMC to unwind the loop just four times with the --unwind flag

cbmc termination.c --unwind 4

and CBMC terminates with apparent success:

VERIFICATION SUCCESSFUL

But how do you know that unwinding the loop 4 times is enough? What if something bad happens on the 5th iteration and you just never asked CBMC to look beyond the 4th iteration?

CBMC has a solution. We always run CBMC with an extra flag

cbmc termination.c --unwind 4  --unwinding-assertions

that checks that loops have been completely unwound: It checks that the loop termination condition is true after the loop unwinding. If you run CBMC with this flag, CBMC reports failure (the loop unwinding assertion has failed):

line 7 unwinding assertion loop 0: FAILURE

Try unwinding 40 times:

cbmc termination.c --unwind 40  --unwinding-assertions

line 7 unwinding assertion loop 0: FAILURE

Try unwinding 80 times:

cbmc termination.c --unwind 80  --unwinding-assertions

line 7 unwinding assertion loop 0: FAILURE

Try asking for a trace:

cbmc termination.c --unwind 80  --unwinding-assertions --trace

Now you see that size is stuck at 0. The final steps of the trace are

State 257 file termination.c function main line 8 thread 0
----------------------------------------------------
  size=0ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 260 file termination.c function main line 8 thread 0
----------------------------------------------------
  size=0ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 263 file termination.c function main line 8 thread 0
----------------------------------------------------
  size=0ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

Violated property:
  file termination.c function main line 7 thread 0
  unwinding assertion loop 0

Try unwinding 64 times since you probably have a 64-bit machine:

cbmc termination.c --unwind 64 --unwinding-assertions --trace

In the final two steps of the trace you can see the overflow from a large integer to 0:

State 212 file termination.c function main line 8 thread 0
----------------------------------------------------
  size=9223372036854775808ul (10000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 215 file termination.c function main line 8 thread 0
----------------------------------------------------
  size=0ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

Violated property:
  file termination.c function main line 7 thread 0
  unwinding assertion loop 0



** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

CBMC as proof

Think of CBMC as a tool for doing mathematical proof. CBMC does an exhaustive search for issues affecting functional correctness and memory safety. If CBMC finds an issue, as we have seen, then CBMC has likely found a bug. But if CBMC does not find any issues, then you can rest assured that the issues like memory safety that you are asking CBMC to check for will not occur in your program with the inputs you are asking CBMC to check.

We note, however, that using CBMC may require bounding the size of the inputs you are asking CBMC to check. It may be necessary, for example, to assume that packets coming off the network are of size at most 1024 bytes in order to fit the problem into CBMC. We refer to assumptions like this as proof assumptions. It is important to remember that proof assumptions exists, and to communicate them clearly to the reader or consumer of any proof you write with CBMC.

Let's look again at memory-safety.c

#define SIZE 20
char buffer[SIZE];

char read_buffer(int i)  { return buffer[i];     }
char read_pointer(int i) { return *(buffer + i); }

int main() {
  int index;
  read_buffer(index);
  read_pointer(index);
}

that we found to have memory safety issues in the last section. The problem was obviously the lack of bounds checking in the code. Let's fix that.

Memory safety proof

Let's try adding bounds checking. Consider memory-safety1.c

#define SIZE 20
char buffer[SIZE];

char read_buffer(int i)  {
  if (i < SIZE) return buffer[i];
  return '\0';
}
char read_pointer(int i) {
  if (i < SIZE) return *(buffer + i);
  return '\0';
}

int main() {
  int index;
  read_buffer(index);
  read_pointer(index);
}

We probably want better error handling than just returning NULL, but let's run CBMC to prove memory safety:

cbmc memory-safety1.c --bounds-check --pointer-check

** Results:
memory-safety1.c function read_buffer
[read_buffer.array_bounds.1] line 10
  array 'buffer' lower bound in buffer[(signed long int)i]: FAILURE
[read_buffer.array_bounds.2] line 10
  array 'buffer' upper bound in buffer[(signed long int)i]: SUCCESS

memory-safety1.c function read_pointer
[read_pointer.pointer_dereference.1] line 14
  dereference failure: pointer outside object bounds in buffer[(signed long int)i]:
  FAILURE

** 2 of 3 failed (2 iterations)
VERIFICATION FAILED

Oh, nuts. We failed. We added bounds checking only for the upper bound.

Memory safety proof 2.0

Let's try adding bounds checking for both the upper and lower bounds. Consider memory-safety2.c

#define SIZE 20
char buffer[SIZE];

char read_buffer(int i)  {
  if (0 <= i && i < SIZE) return buffer[i];
  return '\0';
}
char read_pointer(int i) {
  if (0 <= i && i < SIZE) return *(buffer + i);
  return '\0';
}

int main() {
  int index;
  read_buffer(index);
  read_pointer(index);
}

and run CBMC

cbmc memory-safety2.c --bounds-check --pointer-check

** 0 of 3 failed (1 iterations)
VERIFICATION SUCCESSFUL

and declare victory.

Memory safety proof harness

Let's pivot back to the notion of a proof harness before we declare complete victory.

Back when we introduced CBMC as a form of unit testing, we had a function quartile under test and a unit test for quartile. The unit test set up the software environment for the function under test and invoked the function. The function quartile was so simple that all the unit test had to do was initialize the argument x passed to quartile and invoke quartile on x. Then we removed the initialization of x so that CBMC could consider all possible integer values for the argument x. We transformed the unit test into what we call a proof harness for the function quartile and used that with CBMC.

We routinely find ourselves with a library and wanting to use CBMC to prove that all of the public entry points in the library's API are memory safe. Our style is to write a memory safety proof for each entry point independently. We write one proof harness for each entry point. The purpose of the proof harness is to model the software environment in which the entry point will be called. The proof harness will always have to model the inputs to the entry point. But the proof harness might also have to model some aspects of the global state if, for example, there is a system table accessed by the entry point.

In the ideal world, a proof harness will construct arbitrary, unconstrained values for every variable and data structure in the software environment of an entry point, and invoke the entry point. In the real world, the entry point makes some assumptions about its inputs. It may, at the very least, assume that the system table is well-formed in the sense that it satisfies some data structure invariant. In the ideal world, the proof author will talk with the code author and convince the developer to write more bullet-proof code. In the real world, the proof author will model these assumptions in the proof harness to prove memory safety. But now these assumptions become part of the proof: CBMC has demonstrated that the entry point is memory safe, but only when the assumptions described in the proof harness are true when the entry point is invoked. A developer might want to include in the testing framework some checks that these assumptions really are true at all call sites calling the entry point. Or a developer might want to use CBMC to prove this...

But let's return to our memory safety example and transform it into something you are more likely to encounter in the real world.

The library

First, the buffer and the accessor functions are likely to be part of a library. Here is library.h

char read_buffer(int i);
char read_pointer(int i);

and library.c

#include "library.h"

#define SIZE 20
char buffer[SIZE];

char read_buffer(int i)  {
  if (0 <= i && i < SIZE) return buffer[i];
  return '\0';
}
char read_pointer(int i) {
  if (0 <= i && i < SIZE) return *(buffer + i);
  return '\0';
}

The proof harnesses

Second, we write one proof harness for each entry point. Here is read_buffer_harness.c

#include "library.h"

harness() {
  int index;
  read_buffer(index);
}

and read_pointer_harness.c

#include "library.h"

harness() {
  int index;
  read_pointer(index);
}

Notice that we have changed the function name from main to harness in these proof harnesses. This is not essential, it is just a matter of style, but it does avoid name conflicts with a real main that might exist in the real environment.

The proof

Now we can run the proofs just as before, giving both the library and the proof harness on the command line, and also indicating to CBMC that the function to test is now called harness and not main:

cbmc library.c read_buffer_harness.c --bounds-check --pointer-check --function harness
cbmc library.c read_pointer_harness.c --bounds-check --pointer-check --function harness

In both cases:

** 0 of 3 failed (1 iterations)
VERIFICATION SUCCESSFUL

Success!!

Building code for proof

One last thing. In the real world, the library is not this simple. There is probably a build process to compile the source code into a library using a compiler like gcc.

One approach is to build the library using goto-cc in place of gcc. The compiler goto-cc is intended to be a drop-in replacement for gcc. Using goto-cc should be as easy as building with CC=goto-cc in place of CC=gcc. The difference is that goto-cc produces an intermediate representation for the program called a "goto program" or "goto binary" that is used by CBMC for model checking. When we run cbmc directly on a source file, CBMC is invoking goto-cc on the source file before model checking, but we can run goto-cc ourselves to build the goto program, and run CBMC on that.

Our approach, however, is not to build the entire library. There are performance and complexity issues that we won't go into here related to symbolic execution and constraint solving. We usually build only the portions of the library that are required to prove that a particular entry point is memory safe.

Using our simple library above to illustrate, we would build and prove memory safe the entry point read_buffer as follows:

goto-cc library.c -o library.goto
goto-cc read_buffer_harness.c -o read_buffer_harness.goto
goto-cc library.goto read_buffer_harness.goto -o read_buffer.goto --function harness
cbmc read_buffer.goto --bounds-check --pointer-check

The first two lines build the source files, the third links them together (and identifies harness as the entry point), and the fourth line runs CBMC on the result. The process for read_pointer is similar.

Now, finally, and forever:

** 0 of 3 failed (1 iterations)
VERIFICATION SUCCESSFUL

Success!!

CBMC proofs

This chapter goes into greater detail on how to use CBMC on more realistic examples.

We assume that you are familiar with using CBMC on simple examples. We assume you have installed the tools and have read about proof enough to have passing familiarity with proof, proof harnesses, and building code for proof with CBMC.

• Running cbmc
• Loop unwinding
• Property checking
• Coverage checking
• Proof harnesses
• Proof assumptions
• Goto programs

Running cbmc

At this point we already have some experience with running CBMC on simple source files. For example, we have used CBMC to find memory safety issues and debug a termination issue.

One thing we have touched on only lightly is how to interpret the output of CBMC. Let's do that now.

Consider the following program vector.c

#include <stdlib.h>
#define LENGTH 2

void init(int *, size_t);

int main() {
  int vector[LENGTH];

  init(vector, LENGTH);
  for (int i=0; i<=LENGTH; i++)
    vector[i] = vector[i] + 1;

  return 0;
}

Suppose we run CBMC on this program and ask CBMC to do array bounds checking and to produce an error trace for every array bounds violation that it finds.

cbmc vector.c --bounds-check --trace

Let's examine the output of CBMC one section at a time. After some preliminary output, CBMC begins with

Starting Bounded Model Checking
**** WARNING: no body for function init
Unwinding loop main.0 iteration 1 file vector.c line 13 function main thread 0
Unwinding loop main.0 iteration 2 file vector.c line 13 function main thread 0
Unwinding loop main.0 iteration 3 file vector.c line 13 function main thread 0

CBMC is warning us that it found no function body for init. We included the function declaration but forgot to include the function definition. CBMC treats a function like init with no function body as a function with no side effects (init will not initialize the vector) that returns an unconstrained return value (though init returns no value since the return type is void).

CBMC is also telling us that it unwound the for loop three times. This makes sense since the array has LENGTH=2. Notice that CBMC gave this first (and only) loop in the function main the loop name main.0.

After some logging output (describing the sequence of transformations CBMC performs on the program to turn it into a Boolean constraint problem and the invocation of the SAT solver to solve the constraint problem), CBMC prints its results.

** Results:
vector.c function main
[main.array_bounds.1] line 14
  array 'vector' lower bound in vector[(signed long int)i]: SUCCESS
[main.array_bounds.2] line 14
  array 'vector' upper bound in vector[(signed long int)i]: FAILURE

CBMC is reporting that it performed two array bounds check on line 14: it checked whether the lower bound of vector could be violated, and whether the upper bound could be violated. The lower bound check succeeded and the upper bound check failed.

Finally, CBMC prints a complete error trace for each check that failed. In our case, it was the second array bounds check in the function main that failed, and CBMC gave that check the name main.array_bounds.2.

Trace for main.array_bounds.2:

State 21 file vector.c function main line 10 thread 0
----------------------------------------------------
  vector={ 2760991, 33628711 } ({ 00000000 00101010 00100001 00011111, 00000010 00000001 00100010 00100111 })

State 26 file vector.c function main line 13 thread 0
----------------------------------------------------
  i=0 (00000000 00000000 00000000 00000000)

State 28 file vector.c function main line 14 thread 0
----------------------------------------------------
  vector[0l]=2760992 (00000000 00101010 00100001 00100000)

State 29 file vector.c function main line 13 thread 0
----------------------------------------------------
  i=1 (00000000 00000000 00000000 00000001)

State 32 file vector.c function main line 14 thread 0
----------------------------------------------------
  vector[1l]=33628712 (00000010 00000001 00100010 00101000)

State 33 file vector.c function main line 13 thread 0
----------------------------------------------------
  i=2 (00000000 00000000 00000000 00000010)

Violated property:
  file vector.c function main line 14 thread 0
  array 'vector' upper bound in vector[(signed long int)i]
  !((signed long int)i >= 2l)

The trace is a step-by-step execution of the program from an initial state to the array bounds violation. The trace has six steps. The steps are numbered 21 through 33 because there were a lot of CBMC internal steps like initialization of CBMC internal variables that CBMC did not include in the program trace. The steps included in the trace are all assignments to program variables made during the execution.

The first step shows the initialization of vector. CBMC chose two fairly large integers as the initial values of the two integers in the array. Notice that CBMC is printing the values in both decimal and binary notation.

The next four steps show the variable assignments made during the first two iterations of the loop: each iteration does one assignment to i and one assignment to vector.

The final two steps show the assignment i=2 and the attempt to access vector[i] with i==2 that caused the array bounds violation.

CBMC viewer is a tool that summarizes the findings of CBMC in the form of a report that can be opened in any web browser. One thing that viewer does is render the list of findings together with links to the error traces demonstrating the findings. Each step of an error trace is linked back to the line of source code that is responsible for the step, making it easier to follow the trace and debug the issue. See the release page and the documentation for more information.

Loop unwinding

CBMC is a bounded model checker for C. CBMC works by unwinding the loops in our code (by inlining a finite number of iterations of the loop). CBMC needs to know a bound on the number of times it is expected to unwind any particular loop in our code. In the same way, CBMC needs to know a bound on the number of times to invoke any recursive function in our code.

Sometimes CBMC can figure this out on its own. Consider the program loop1.c

#include<assert.h>

int main() {
  unsigned array[10];

  for (int i = 0; i < 10; i++) {
    array[i] = 0;
  }

  for (int i = 0; i < 10; i++) {
    assert(array[i] == 0);
  }
  return 0;
}

and run CBMC with

cbmc loop1.c

and CBMC will print

[main.assertion.1] line 11 assertion array[i] == 0: SUCCESS
VERIFICATION SUCCESSFUL

Sometimes CBMC needs help. Consider the program loop2.c

#include<assert.h>

int main() {
  unsigned bound;
  unsigned array[bound];

  for (int i = 0; i < bound; i++) {
    array[i] = 0;
  }

  for (int i = 0; i < bound; i++) {
    assert(array[i] == 0);
  }
  return 0;
}

and run CBMC with

cbmc loop2.c

and CBMC will unwind the first loop until it runs out of resources or the loop index wraps around. We need to tell CBMC how many times to unwind the loops in the program. Run CBMC with

cbmc --unwind 11 loop2.c

and CBMC will unwind every loop in the program 10 times (not 11 times!) and print

[main.assertion.1] line 11 assertion array[i] == 0: SUCCESS
VERIFICATION SUCCESSFUL

In summary, we use the flag --unwind to tell CBMC to bound the unwinding of loops in the program. We use --unwind 11 to bound loop unwinding to 11 iterations. We can use the flag --unwindset to give different bounds to different loops. CBMC names the loops in a program with the name of the function containing the loop and the position of the loop within the function. We can ask CBMC to display loop names with the --show-loops flag

cbmc --show-loops loop2.c

and see that the two loops in loop2.c are named main.0 and main.1. We can run CBMC with

cbmc --unwindset main.0:11 --unwindset main.1:11 loop2.c

and get the same successful verification result as with --unwind 11. The flags --unwind and --unwindset can be used together and with different bounds. CBMC will use the --unwind bound by default and use the --unwindset bound for the loop it names.

Loop unwinding assertions

Now, however, we have a problem. CBMC has proved that there is no assertion failure in the program as long as we limit loops to 10 iterations. But how do we know that 10 iterations is enough? What if it is possible for a loop to iterate 11 times, and the error we are looking for occurs on the 11th iteration, and we missed it?

CBMC has a solution for this called loop unwinding assertions. We can ask CBMC to insert loop unwinding assertions with the flag --unwinding-assertions. Now, after CBMC has unrolled a loop, it will insert immediately after the unrolled loop an assertion that the loop termination is true. In other words, CBMC will check that it has completely unrolled the loop. For example, running CBMC on the first program loop1.c with

cbmc --unwind 11 --unwinding-assertions loop1.c

succeeds with

VERIFICATION SUCCESSFUL

but running CBMC on the second program loop2.c with

cbmc --unwind 11 --unwinding-assertions loop2.c

fails with output that includes

[main.unwind.0] line 7 unwinding assertion loop 0: FAILURE
VERIFICATION FAILED

Property checking

CBMC can check more than just assertions in the code. In this section, we describe properties like memory safety that we check for every time we run CBMC. For the full list of things that CBMC can check, run cbmc --help.

• Memory safety
• More pointer checks
• Malloc failure
• Integer overflow
• Floating point overflow
• Division by zero
• Type casting
• Bit shifting
• Loop unwinding

Memory safety

• --bounds-check enables array bounds checking.
• --pointer-check enables invalid pointer checking.

Given the program bounds.c

int main() {
  int array[10];
  for (int i=0; i<=10; i++) array[i] = i;
}

the command

cbmc --bounds-check bounds.c

finds the off-by-one error in the loop termination condition:

line 3 array 'array' lower bound in array[(signed long int)i]: SUCCESS
line 3 array 'array' upper bound in array[(signed long int)i]: FAILURE

Given the program pointers.c

int main() {
  int *ptr;
  int array[10];
  *ptr = 3;
  *(array + 10) = 4;
}

the command

cbmc --pointer-check pointers.c

finds that ptr may be null and that array + 10 points beyond the end of array:

line 4 dereference failure: pointer NULL in *ptr: FAILURE
line 4 dereference failure: pointer invalid in *ptr: FAILURE
line 4 dereference failure: deallocated dynamic object in *ptr: FAILURE
line 4 dereference failure: dead object in *ptr: FAILURE
line 4 dereference failure: pointer outside object bounds in *ptr: FAILURE
line 4 dereference failure: invalid integer address in *ptr: FAILURE
line 5 dereference failure: dead object in array[(signed long int)10]: SUCCESS
line 5 dereference failure:
  pointer outside object bounds in array[(signed long int)10]: FAILURE

These off-by-one errors caught with --bounds-check and --pointer-check feel quite similar to each other, but --bounds-check is for index expressions and --pointer-check is for pointer offsets. We always use these flags together.

More pointer checks

• --pointer-overflow-check checks pointer arithmetic for arithmetic overflow and underflow.
• --pointer-primitive-check checks that all pointers are either valid or null (all pointers, not just dereferenced pointers) when used within CBMC builtins like __CPROVER_r_okay(ptr, size) that returns true if reading the piece of memory starting at the given pointer with the given size is safe.

Given the file pointer-overflow.c

#include <stdint.h>
int main() {
  int array[10];
  int *x = array + SIZE_MAX;
}

the command

cbmc --pointer-check pointer-overflow.c

will succeed (because the bad pointer is never dereferenced) but the command

cbmc --pointer-check --pointer-overflow-check pointer-overflow.c

will find the overflow

line 4 pointer arithmetic:
  dead object in array + (signed long int)18446744073709551615ul: SUCCESS
line 4 pointer arithmetic:
  pointer outside object bounds in array + (signed long int)18446744073709551615ul:
  FAILURE

At the moment, the flag --pointer-overflow-check will detect the potential for integer overflow in the calculation of an offset into an object, and also for an offset that would take you outside the bounds of an object, but there is another form of overflow to be aware of. Arithmetic overflow in pointer arithmetic is an issue because the CBMC heap model interprets a pointer as an object id together with an offset into the object. Pointer arithmetic in C uses signed integers for offsets. So it is possible for the desired offset into the object to have a magnitude larger than the maximum offset CBMC is using for objects on the heap.

Malloc failure

• --malloc-may-fail allows any invocation of malloc to fail.
• --malloc-fail-null sets the malloc failure mode to returning a null pointer.

Taken together, these flags cause CBMC to use a model of malloc in which it is possible for any invocation of malloc to fail and return a null pointer. Given the program malloc.c

#include <stdlib.h>
main () {
  int *x = (int *) malloc(sizeof(int));
  *x = 1;
}

the command

cbmc --pointer-check malloc.c

will succeed but the command

cbmc --pointer-check --malloc-may-fail --malloc-fail-null malloc.c

will fail because it is possible for malloc to fail and return a null pointer causing *x to dereference a null pointer:

line 4 dereference failure: pointer NULL in *x: FAILURE
line 4 dereference failure: pointer invalid in *x: SUCCESS
line 4 dereference failure: deallocated dynamic object in *x: FAILURE
line 4 dereference failure: dead object in *x: FAILURE
line 4 dereference failure: pointer outside object bounds in *x: FAILURE
line 4 dereference failure: invalid integer address in *x: SUCCESS

Integer overflow

• --signed-overflow-check and --unsigned-overflow-check check for integer overflow.

Given the file integer.c

#include <limits.h>
int main() {
  int x;
  int y;
  if (x + y <= INT_MAX)
    x = x + y;
  if (y <= INT_MAX - x)
    x = x + y;
}

the command

cbmc --signed-overflow-check integer.c

finds several possibilities for signed integer overflow (an undefined behavior in the C standard):

line 5 arithmetic overflow on signed + in x + y: FAILURE
line 7 arithmetic overflow on signed - in 2147483647 - x: FAILURE
line 8 arithmetic overflow on signed + in x + y: FAILURE

Floating point overflow

• --float-overflow-check checks for +/-Inf in floating-point arithmetic.
• --nan-check checks for NaN in floating-point arithmetic.

Given the file float.c

int main() {
  float x = 100000000.0;
  for (int i = 0; i < 10; i++) x = x * x;
}

the command

cbmc float.c

will succeed but the command

cbmc --float-overflow-check float.c

will find the floating-point overflow:

line 3 arithmetic overflow on floating-point multiplication in x * x: FAILURE

Given the file nan.c

int main() {
  float x = 0.0 / 0.0;
}

the command

cbmc nan.c

will succeed but the command

cbmc --nan-check nan.c

will find the NaN:

line 2 NaN on / in 0.0 / 0.0: FAILURE

Division by zero

• --div-by-zero-check checks for division by zero.

Given the file zero.c

int main() {
  int a;
  int b;
  int result = a / b;
}

the command

cbmc --div-by-zero-check zero.c

finds the potential for division by zero:

line 4 division by zero in a / b: FAILURE

Type casting

• --conversion-check checks for values that can't be represented after type casts.

Given the file conversion.c

#include <stdint.h>
int main() {
  uint8_t x;
  uint16_t y;
  x = y;
}

the command

cbmc conversion.c

will succeed but the command

cbmc --conversion-check conversion.c

finds the potential for truncation of an integer value from 16 bits to 8 bits:

line 5 arithmetic overflow on unsigned to unsigned type conversion in (uint8_t)y:
  FAILURE

Bit shifting

• --undefined-shift-check enables checks for undefined shift behaviors like shifting too far or shifting a negative value

Given the program 'shift.c'

int main() {
  int x = 1;
  int y = -1;
  int z;
  z = x << 64;
  z = x << -1;
  z = y << 64;
  z = y << -1;
}

the command

cbmc --undefined-shift-check shift.c

finds a number of undefined shift behaviors:

line 5 shift distance too large in x << 64: FAILURE
line 5 shift operand is negative in x << 64: SUCCESS
line 6 shift distance is negative in x << -1: FAILURE
line 6 shift operand is negative in x << -1: SUCCESS
line 7 shift distance too large in y << 64: FAILURE
line 7 shift operand is negative in y << 64: FAILURE
line 8 shift distance is negative in y << -1: FAILURE
line 8 shift operand is negative in y << -1: FAILURE

Loop unwinding

• --unwinding-assertions enables checks that loops have been completely unwound.

Always run CBMC with the flag --unwinding-assertions.

Given the program loop.c

#include <stdbool.h>
int main() {
  int bound;
  for (int i=0; i<bound; i++)
    if (i > 9) assert(false);
}

the command

cbmc --unwind 10 loop.c

will report

line 5 assertion 0: SUCCESS

This is a surprise. The assertion is false. Why did CBMC not discover this? The problem is that the assertion fails only on the 10th iteration of the loop, and we gave CBMC the flag --unwind 10 that restricts CBMC to 9 iterations (not 10!). Use the flag --unwinding-assertions to detect mistakes like this. The command

cbmc --unwind 10 --unwinding-assertions loop.c

will report

line 4 unwinding assertion loop 0: FAILURE
line 5 assertion 0: SUCCESS

Always run CBMC with the flag --unwinding-assertions.

Coverage checking

CBMC can also do coverage checking. You can ask CBMC to do property checking with

cbmc program.goto --check1 --check2 --check3 --unwinding-assertions

and do coverage checking with

cbmc program.goto --check1 --check2 --check3 --cover location

The first command causes CBMC to do property checking, and the second command causes CBMC to do coverage checking. CBMC computes line coverage and computes the lines of code that CBMC was able to exercise while doing the property checking. Unexpectedly low code coverage is usually an indication that your proof harness is not modeling enough program state or is otherwise over-constraining the set of values the state can take on, something you should probably investigate. (Notice that the second command adds --cover location and omits --unwinding-assertions; the two flags cannot be used together.)

CBMC viewer is a tool that summarizes the findings of CBMC in the form of a report that can be opened in any web browser. One thing that viewer does is render the coverage data in two forms. First, it gives coverage data for the individual functions and for the code as a whole. Second, in the style of lcov, it annotates lines of source code with the colors green and red to indicate the lines hit and missed by CBMC. The two representations of coverage work together to make it easier to understand why coverage is lower than expected. See the release page and the documentation for more information.

The coverage data itself, without the aid of CBMC viewer, is a little overwhelming for most users. CBMC computes the set of basic blocks in the goto program. A basic block is a block of straight-line code ending with a goto statement (going to the next basic block). CBMC annotates each basic block with a test that amounts to saying "CBMC entered this basic block at least once during property checking". CBMC uses the SAT solver to determine if there is any input and any path through the code that could reach this basic block. The output is the list of basic blocks, and for each basic block whether CBMC entered the basic block and the lines of source code contributing steps to the basic block.

Coverage checking can take longer than property checking. Depending on what properties you are checking for, there can be many more basic blocks to check than there are properties to check. As a result, the constraint problem for coverage checking can be both bigger and harder to solve than for property checking.

Proof harnesses

This section is about writing proof harnesses for CBMC. Our proof harness overview has already introduced the notion of a proof harness, and this section goes into greater detail about the issues to consider when writing a harness. The purpose of a proof harness is to build a model of the environment of the function under test. The purpose of this model is to collect in one place all of the assumptions required for the proof to hold. The proof harness is responsible for:

• Modeling input
• Modeling global state
• Modeling interfaces
• Allocating data
• Validating data
• Proof assumptions

Modeling input

For simple functions, the model of the environment is just the input to the function.

Suppose we have a library library1.c

#include <assert.h>

int alpha1(int a) {
    return a+1;
}

int beta1(int b) {
    int bb = alpha1(b);
    assert(bb == b);
}

and we want to test function beta1. The input to function beta1 is an integer b. We write a proof harness harness1.c

int beta1(int b);

int main() {
   int x;
   beta1(x);
}

that allocates an unconstrained integer named x and invokes beta1 on x.

We run CBMC on the result with

goto-cc -o library1.goto library1.c
goto-cc -o harness1.goto harness1.c
goto-cc -o proof1.goto library1.goto harness1.goto
cbmc proof1.goto

and we see a violation of the assertion bb == b.

** Results:
library1.c function beta1
[beta1.assertion.1] line 9 assertion bb == b: FAILURE

** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

Correcting this assertion to bb == b + 1 fixes the problem.

Modeling global state

Sometimes a function depends on global state. A common example is low-level system code that depends on a system table, and we want to know the code works no matter what has been stored in the system table.

Suppose we have a library library2.c

#include <assert.h>

int counter = 0;

int alpha2(int a) {
    counter = counter + 1;
    return a+counter;
}

int beta2(int b) {
    int bb = alpha2(b);
    assert(bb == b + 1);
}

and we want to test function beta2. This time the function beta2 depends on its input b, but it also depends on a global variable counter that is initialized to 0 but is changed with each invocation of beta2. We want to know that beta2 always works, no matter how many times beta2 has been invoked in the past.

We do this by writing a proof harness that chooses an unconstrained value for both the function input b and the global variable counter. We write a proof harness harness2.c

extern int counter;
int beta2(int b);

int main() {
    int cnt;
    counter = cnt;

    int x;
    beta2(x);
}

We run CBMC on the result with

goto-cc -o library2.goto library2.c
goto-cc -o harness2.goto harness2.c
goto-cc -o proof2.goto library2.goto harness2.goto
cbmc proof2.goto

and see a violation of the assertion bb == b + 1.

** Results:
library2.c function beta2
[beta2.assertion.1] line 12 assertion bb == b + 1: FAILURE

** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

We correct this to bb >= b + 1 and we are done.

Modeling interfaces

Sometimes a function depends on an implementation of an interface or a library API that we don't care to test. A common example is a function that depends on a network communication protocol like HTTP with send and receive methods. We want our code to work independent of the protocol implementation, so we replace the implementations of the functions in the protocol interface with stubs that over-approximate the behaviors of the implementations.

Suppose we have a library library3.c

#include <assert.h>

void send(int msg);
int receive();

int alpha(int x) {
    int y = receive();
    assert(y > 0);
    return y+1;
}

that depends on send and receive methods from a network interface. We stub out the network interface with network3.c

int receive() {
    // model receiving an unconstrained integer value from the network
    int msg;
    return msg;
}

void send(int msg) {
    // model sending an integer over the network (nothing to do)
    return;
}

We write the proof harness harness3.c

int alpha(int x);

int main() {
    int x;
    alpha(x);
}

We run CBMC with

goto-cc -o network3.goto network3.c
goto-cc -o library3.goto library3.c
goto-cc -o harness3.goto harness3.c
goto-cc -o proof3.goto network3.goto library3.goto harness3.goto
cbmc proof3.goto

and we get a failure of the assertion y > 0.

Suppose the mistake is in our model of the network. Suppose our network only transmits positive integers. Then we can fix our stub of the receive method to return not an unconstrained integer but an unconstrained positive integer. We change our stubs for the network to network3a.c

int receive() {
    // model receiving an unconstrained POSITIVE integer value from the network
    int msg;
    __CPROVER_assume(msg > 0);
    return msg;
}

void send(int msg) {
    // model sending an integer over the network (nothing to do)
    return;
}

We run CBMC with

goto-cc -o network3a.goto network3a.c
goto-cc -o library3.goto library3.c
goto-cc -o harness3.goto harness3.c
goto-cc -o proof3.goto network3a.goto library3.goto harness3.goto
cbmc proof3.goto

and declare victory at the successful verification.

Allocating data

For projects where functions take pointers to data on the heap, we recommend writing functions to allocate unconstrained values on the heap of the appropriate types for use in proof harnesses.

Consider a string buffer defined by

typedef struct { size_t length; char* buffer; } strbuf;

and consider a function that takes a pointer to a string buffer and caches the fifth character in the buffer into a global variable

char cache;
void cache_fifth_char(strbuf* str) { cache = str->buffer[4]; }

Let's try to prove that this function is memory safe (although, obviously, it is not). Memory safety means that we never dereference an invalid pointer and we never try to access data outside the bounds of a valid object. We can do this by calling CBMC with the flags --pointer-check and --bounds-check. Let's prove this even in the case where malloc can fail and return NULL instead of a pointer. The default model of malloc in CBMC never fails, but we can change to a model of malloc that can fail and return NULL by calling CBMC with the flags --malloc-may-fail and --malloc-fail-null.

The function cache_fifth_char takes a pointer to a string buffer on the heap, so let write a function that allocates a string buffer.

strbuf* strbuf_allocate(size_t length) {
  strbuf* str = malloc(sizeof(strbuf));
  if (str == NULL) return NULL;
  str->length = length;
  str->buffer = malloc(length);
  return str;
}

Now we can write a proof harness for the function

int main() {
  size_t len;
  strbuf* str = strbuf_allocate(len);

  cache_fifth_char(str);
}

Pulling all of this together into a single file strbuf1.c, we can run cbmc on this file with

cbmc --pointer-check --bounds-check --malloc-may-fail --malloc-fail-null strbuf1.c

and the result is a slew of verification failures including

[cache_fifth_char.pointer_dereference.1] line 7 dereference failure: pointer NULL in str->buffer: FAILURE
[cache_fifth_char.pointer_dereference.7] line 7 dereference failure: pointer NULL in str->buffer[(signed long int)4]: FAILURE
[cache_fifth_char.pointer_dereference.11] line 7 dereference failure: pointer outside object bounds in str->buffer[(signed long int)4]: FAILURE

The first is saying that str may be NULL, the second is saying that str->buffer may be NULL, and the third is saying that str->buffer may not have 5 character in it.

We are obviously going to have to make some assumptions about the string buffer before we can prove that the function is memory safe.

Validating data

For projects that require allocating objects of various types on the heap, we recommend writing predicates that say what well-formed objects of these types look like.

In the case of our example, a valid pointer to a string buffer must be nonnull, and a valid string buffer must have a buffer that is nonnull.

bool strbuf_is_valid(strbuf* str) {
  if (str == NULL) return false;
  if (str->buffer == NULL) return false;
  return true;
}

With this predicate, we can write a proof harness that assumes the string buffer allocated on the heap is valid before calling the function. We can also assert that the string buffer remains valid after calling the function. And we can assume that the buffer has at least 5 characters in it. In fact, we can prove the this remains true after the function invocation, meaning that the function preserves the validity of its input.

int main() {
  size_t len;
  strbuf* str = strbuf_allocate(len);

  __CPROVER_assume(strbuf_is_valid(str));
  __CPROVER_assume(str->length > 4);

  cache_fifth_char(str);

  __CPROVER_assert(strbuf_is_valid(str), "String buffer remains valid");
  __CPROVER_assert(str->length > 4, "String buffer remains length >4");
}

Pulling all of this together into strbuf2.c, we can run CBMC

cbmc --pointer-check --bounds-check --malloc-may-fail --malloc-fail-null strbuf2.c

and rejoice in the successful validation.

Proof assumptions

Notice that in our last proof harness, we worked hard to make as explicit as possible all of the assumptions required for memory safety to hold: The pointer must be a valid pointer to a valid string buffer with at least five characters in it. It is the responsibility of the programmer to make certain that these assumptions are true when the function is called. All bets are off when the function is called in a weaker context where some of these assumptions are false. The memory safety proof of the function does not hold in that context since the assumptions it is based on do not hold.

Proof assumptions

A proof assumption is anything that limits the applicability of a statement that has been otherwise proved by CBMC. An example of a proof assumptions is the assumption that packets coming off a network are of size at most 1024 bytes. This proof assumption would arise if the proof harness for a function modeled an incoming packet as any character buffer of size at most 1024 characters. Suppose that we run CBMC with this proof harness, and CBMC is unable to find any memory safety errors. We might be tempted to say that CBMC has proved the function is memory safe. But the truth is that CBMC has proved the function is memory safe only when the function is invoked on a packet of size at most 1024 characters. We believe that such a proof has value, and that hard-to-find software issues will be discovered in the course of writing such a proof, but the result is not absolute proof of memory safety.

Just to clear, every proof in mathematics depends on proof assumptions. In number theory, a theorem may hold for all integers n, assuming n is nonzero. The theorem is powerful because it is applicable to nearly every integer. In cryptography, a theorem may hold only if n is the product of two prime numbers p and q of roughly the same size. The theorem may still have powerful applications, but it applies only to a much smaller set of integers.

Proof assumptions must be clearly and accurately communicated to any proof reader and to any consumer of the proof. Doing this right may be the hardest part of proof. It is particularly important in the context of software proof, however, because the credibility of the proof tool and the methodology for using the tool depends on getting this right. Trust is hard to earn and easy to lose.

The two most common sources of proof assumptions are memory allocation and function abstraction.

Memory allocation

There are two common proof assumptions about memory.

Size

One class of assumption is size. Some are obvious. If the proof harness includes

  size_t size;
  __CPROVER_assume(size < 100);

  char *buffer = (char *) malloc(size);

then the buffer is assumed to be of size smaller than 100. Some are implicit. If the proof harness includes

  size_t size;

  char *buffer = (char *) malloc(size);

then the buffer is implicitly bounded to the size of the maximum object that CBMC can model (which is probably smaller than the largest size representable in a 64-bit integer, see our discussion of the memory model for more information).

Invariants

One class of assumption is well-formedness or implicit data structure invariants. Suppose the proof harness includes

  typedef struct {
    size_t size;
    char *buffer;
  } buffer_t;

  buffer_t *buffer = (buffer_t *) malloc(sizeof(*buffer));
  buffer->buffer = (char *) malloc(buffer->size);

then the proof harness is implicitly assuming that the pointer buffer->buffer is either NULL or a valid pointer to a buffer of size buffer-size. This is implicitly assuming an data structure invariant about buffer. Is this really something you want to assume about a buffer you receive as input from an untrusted adversary. Is this really something want to assume even when buffer->size == 0?

Function abstraction

There are two common kinds of function abstraction with CBMC.

Missing functions

One is implicit function abstraction done automatically by CBMC.

When CBMC encounters the invocation of a function missing and cannot find a function definition for missing, CBMC issues a warning "no function body for missing" and models the function missing as a function that

• has no side-effects (makes no change to the state), and
• returns an arbitrary, unconstrained value of the appropriate return type.

This assumption of no side-effects is a serious assumption. Almost no functions in C are purely functional. On the other hand, it is an easy way to model something like a random number generator returning a unint64_t used in some cryptographic code under test. Including the actual function definition of the random number generator will probably be too much for CBMC, but by leaving the function undefined (omitting the code defining the random number generator from the build), CBMC will consider the impact on the property being testing of every unsigned, 64-bit integer value that can possibly be returned by the number generator.

Stubs

One is explicit function abstraction written by the proof author for the proof.

Consider a cryptographic key generator

  int key_generator(void *context, public_key_t *public, private_key_t *private)

As with the random number generator, including the code for a cryptographic key generator may be too much for CBMC. Reconstructing cryptographic keys is, after all, designed to be intractable!

A reasonable stub for the key generator is:

  int key_generator(void *context, public_key_t *public, private_key_t *private)
  {
    __CPROVER_havoc_object(public);
    __CPROVER_havoc_object(private);
    int rc;
    return rc;
  }

The __CPROVER_havoc_object function fills the objects pointed to by public and private with arbitrary, unconstrained data.

This stub has the pleasing effect of considering possible every value (well-formed or not) that could be written to public and private by the generator, and considering possible every integer value that could be used as a return code.

This stub is, however, making the implicit assumption that the pointers are valid. A better stub would check that the function is being called correctly:

  int key_generator(void *context, public_key_t *public, private_key_t *private)
  {
    __CPROVER_assert(context, "context is nonnull");
    __CPROVER_assert(public, "public is nonnull");
    __CPROVER_assert(private, "private is nonnull");

    __CPROVER_havoc_object(public);
    __CPROVER_havoc_object(private);
    int rc;
    return rc;
  }

Goto programs

The goto program is the intermediate representation of a program used by CBMC to do bounded model checking. CBMC comes with a compiler called goto-cc that is intended to be a drop-in replacement for gcc. The difference is that goto-cc produces a goto program instead of the executable binary produced by gcc. We've already touched on these topics in our overview of how to use CBMC. Most important, we've demonstrated how to use goto-cc to produce the goto program and how to run CBMC on the goto program.

Sometimes, however, it is helpful (and just plain interesting) to look at the goto program produced by goto-cc. Two commands are particularly helpful:

• cbmc program.goto --list-goto-functions displays the function names of all the functions appearing in the goto program program.goto
• cbmc program.goto --show-goto-functions displays function bodies of all the functions appearing in the goto program program.goto.

A goto program

Consider a little program function-pointer.c that declares two functions alpha and beta, assigns nondeterministically one of alpha and beta to a function pointer function, and then invokes the function pointed to by function.

#include <assert.h>

int alpha(int x) {
  return x+1;
}

int beta(int x) {
  return x+2;
}

int main() {
  int (*function)();

  int bool;
  function = bool ? alpha : beta;

  int x;
  int rc = function(x);
}

Let's compile the program into a goto program.

goto-cc function-pointer.c -o function-pointer.goto

The function names

Let's print the function names:

cbmc function-pointer.goto --list-goto-functions

__CPROVER__start /* __CPROVER__start */
__CPROVER_initialize /* __CPROVER_initialize */
alpha /* alpha */
beta /* beta */
main /* main */

The second initialize function initializes some CBMC internal variables. The first start function is the entry point for the goto program. It calls the initialize function followed by the main function. You can print the function bodies and see this for yourself.

The function bodies

Let's print the function bodies:

cbmc function-pointer.goto --show-goto-functions

The result is a little too long to include here, but in the middle of the function body for main we find

     // 7 file function-pointers.c line 18 function main
     IF main::1::function = cast(address_of(beta), code*) THEN GOTO 1
     // 8 file function-pointers.c line 18 function main
     IF main::1::function = cast(address_of(alpha), code*) THEN GOTO 2
     // 9 file function-pointers.c line 18 function main
     ASSUME false
     // 10 file function-pointers.c line 18 function main
  1: CALL main::$tmp::return_value := beta(main::1::x)
     // 11 file function-pointers.c line 18 function main
     GOTO 3
     // 12 file function-pointers.c line 18 function main
  2: CALL main::$tmp::return_value := alpha(main::1::x)
     // 13 no location
  3: ASSIGN main::1::rc := main::$tmp::return_value

This is interesting because it demonstrates how CBMC handles function pointers. What we see is essentially a switch statement that compares the function pointer function with pointers to each of the functions whose address has been taken anywhere in the program. In this case, pointers to the functions alpha and beta. Depending on the outcome of the comparison, either alpha or beta is invoked and its return value is assigned to rc.

We include this discussion as an example of how looking at the goto program can help debug issues with CBMC. If, for example, CBMC were surprisingly slow to terminate, you might look at the goto program and discover that there is another function gamma that is being considered as a possible value for function. This is impossible in our example, but if gamma is defined in another source file that was accidentally included in the build of the goto program, one solution might be simply to omit that source file from the build for this proof.

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.

Frequently asked questions

Here are answers to some frequently-asked questions about CBMC. Please send us any questions you have by filing an issue with us on GitHub.

• How does CBMC work?
• What is loop unwinding?
• How do memory pointers work?
• How do function pointers work?
• How does malloc work?
• What is a proof assumption?
• How do I write a good stub?
• What do I do when CBMC won't stop?

How does CBMC work?

The most complete descriptions of how CBMC works are

• Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking
• Behavioral Consistency of C and Verilog Programs
• CProver developer documentation

The first two documents are the original paper on CBMC and a follow-up technical report giving a bit more detail. They are excellent introductions, but they are a bit old. The third document is a collection of documents for developers. They provide guidance on how to understand the source code.

CBMC uses a technique called symbolic execution to turn a program into a set of symbolic constraints that describe the behavior of the program (the paths through the program).

For example, consider the following code fragment

  int x;
  x = x+1;

CBMC sees the first statement and knows that x should be represented by a vector of 32 binary variables describing the 32-bit binary value of x. CBMC sees the second statement and generates a constraint that says, "If X0 and X1 are binary vectors describing the value of x before and after the assignment, then X1 is X0 plus 1." CBMC uses a Boolean description of a binary adder that adds the 32 bits of X0 and the 32 bits of 1, and generates a constraint that the i-th bit of X1 is equal to the Boolean expression for the i-th bit of the adder's output on inputs X0 and 1.

Proceeding in this way, statement by statement, CBMC constructs a collection of constraints that describe the program behavior. The constraints describe as a collection of Boolean formulas how the state of the program changes during an execution.

CBMC then formulates the following question for each property we want to check about the program: "Does there exist an input and a path through the program that violates the property?" CBMC formulates this question as a constraint problem, and hands the constraint problem to a constraint solver called a SAT solver. The SAT solver looks for an assignment of values to variables that satisfies the constraint describing what a property violation would look like.

If the SAT solver can produce a satisfying assignment, then CBMC can take the satisfying assignment and --- essentially reversing the process of generating the constraints in the first place --- use the assignment to generate an error trace describing the input (the initial state) and each step through the program leading to a violation of the property.

If the SAT solver cannot produce a satisfying assignment, this amounts to a proof that there is no input and no path through the program that can violate the property. Taking all these properties together, if these properties describe memory safety, then this amounts to a proof that the program is memory safe.

A proof of memory safety, of course, assuming all the assumptions the proof harness is making. See our discussion of proof assumptions for more information.

What is loop unwinding?

CBMC is a bounded model checker. CBMC works by executing a program for some bounded number of steps and looking for issues that occur within those steps. CBMC does not execute a program concretely in the same way that a computer would execute the program (would execute the result of compiling the program). Instead, CBMC symbolically executes the program to turn it into a set of symbolic constraints that can be solved by a constraint solver like a SAT solver.

But where does this bound come from? And how do we know the bound is the right one?

Loop bounds

If the program contains no loops and contains no recursion, then every execution of the program is finite, and CBMC can figure out the length of the longest execution and use this as the bound. Sometime CBMC can figure this out even when the program contains loops. For example, CBMC can loop at the loop

  for (int i=0; i < 10; i++)
    buffer[i] = ' ';

and figure out on its own that the loop iterates at most 10 times. But CBMC needs some help with the loop

  while (TRUE)
    if (i < buffer.size) buffer.data[i] = ' ' else break;

We need to give CBMC a bound on the number of times this loop iterates. We need to tell CBMC how many times to unwind this loop during its symbolic execution of the program.

We can do this in two ways.

• Bound all loops: We can instruct CBMC to unwind every loop at most K times with cbmc --unwind K. If you are using the CBMC starter kit, this bound 1 by default, but you can change this to K in your Makefile with

    UNWIND=K
  

• Bound one loop: We can instruct CBMC to unwind a specific loop at most K times with cbmc --unwindset FUNC.NUM:K where FUNC is the name of the function containing the loop and NUM is the number of the loop within the function (more on loop numbers below). If you are using the CBMC starter kit, we recommend that you set this bound in your Makefile with

     UNWINDSET+=FUNC.NUM:K
  

Loop unwinding assertions

Now we know how to tell CBMC to unwind a loop K times, but how do we know that unwinding a loop K times is enough? What if the problem we are looking for occurs on iteration K+1 and we have asked CBMC to unwind the loop only K times? We could miss the issue and never know it because we didn't tell CBMC to work hard enough to find it!

CBMC has solution called "loop unwinding assertions." A loop unwinding assertion is a check that a loop has been completely unwound. It checks that the loop termination condition is guaranteed to be true after the specified number of unwindings. First CBMC unwinds the loop, and then CBMC inserts a assertion that the loop termination condition is true immediately after the final unwinding of the loop. If there is any execution of the program in which you haven't unwound the loop enough times, CBMC will identify the loop by its loop name FUNC.NUM in the list of checks that have failed.

Invoking CBMC with cbmc --unwinding-assertions will ask CBMC to check unwinding assertions.

You can rest assured that CBMC is always invoked with cbmc --unwinding-assertions if you are using the CBMC starter kit.

Counting loop iterations

There are two ways to count loop iterations:

• One is the number of times B that the loop body is traversed.
• One is the number of times T that the loop termination is checked.

These two numbers differ by one: T = B + 1.

When you invoke CBMC, the number K that you give to --unwind or --unwindset is interpreted as the number of times the loop termination is checked: K = T = B+1.

This off-by-one business sometimes confuses people, and sometimes makes it challenging to write a Makefile where arithmetic like B+1 is difficult. One style we have developed is to write a proof harness

int main() {
  size_t length;
  __CPROVER_assume(length < LENGTH);

  char *buffer = (char *) malloc(length);
  for (int i=0; i < length; i++) buffer[i] = ' ';
  ...
}

and to write a Makefile

LENGTH=100
DEFINES += -DLENGTH=$(LENGTH)
UNWINDSET += main.0:$(LENGTH)

Because length is assumed to be strictly less than LENGTH, we know that length + 1 is at most LENGTH, so unwinding the loop main.0 at most LENGTH times is unwinding the loop at least length + 1 times as desired.

A final comment on this off-by-one issue: At some point in the future, you may come to learn that you can also pass the cbmc flags --unwind and --unwindset to a tool named goto-instrument. For historical reasons, cbmc interprets K as K=T and goto-instrument interprets K as K=B. Of course, when choosing between unrolling a loop T=B+1 and B times, it is always safe to unroll a loop more times than necessary. But it may not be practical: If the loop body is large and you are already unrolling a loop many times, the difference between unrolling K and K+1 times many push CBMC execution time from "okay" to "way too long." Just something to keep in mind when using these tools.

Debugging loop unwinding

When not using the starter kit, which uses --unwind 1 by default, you may find yourself in a situation where CBMC keeps unwinding a loop, even when you expected CBMC to be able to determine the loop bound. CBMC uses constant propagation and algebraic simplification to evaluate the loop guard. CBMC will stop unwinding the loop when, using this process, the loop guard evaluates to false. If you would like to debug a case of unexpected loop unwinding, proceed as described below. We will use the following example to illustrate these steps:

int main()
{
  int step;
  for(int i = 0; i < 5; i += step) ;
}

Note that step is unconstrained, perhaps unintentionally so. Running CBMC on this example without any additional options yields:

> cbmc loop.c
[...]
Starting Bounded Model Checking
Unwinding loop main.0 iteration 1 file loop.c line 4 function main thread 0
Unwinding loop main.0 iteration 2 file loop.c line 4 function main thread 0
Unwinding loop main.0 iteration 3 file loop.c line 4 function main thread 0
Unwinding loop main.0 iteration 4 file loop.c line 4 function main thread 0
Unwinding loop main.0 iteration 5 file loop.c line 4 function main thread 0
Unwinding loop main.0 iteration 6 file loop.c line 4 function main thread 0
Unwinding loop main.0 iteration 7 file loop.c line 4 function main thread 0
Unwinding loop main.0 iteration 8 file loop.c line 4 function main thread 0
Unwinding loop main.0 iteration 9 file loop.c line 4 function main thread 0
Unwinding loop main.0 iteration 10 file loop.c line 4 function main thread 0
[...]

until you manually abort this process. One way to understand why this is happening is to undertake the following steps:

1. Run CBMC with whatever options you normally do, but add some finite unrolling bound using --unwind and also add --program-only. This will yield as output the equation system generate by symbolic execution. Pipe the output to some text file. We exemplify this on the above example:

   > cbmc loop.c --program-only --unwind 2
   [...]
   Starting Bounded Model Checking
   Unwinding loop main.0 iteration 1 file loop.c line 4 function main thread 0
   Not unwinding loop main.0 iteration 2 file loop.c line 4 function main thread 0
   [...]
   Program constraints:
   [...]
   // 2 file loop.c line 4 function main
   (26) i!0@1#2 == 0
   // 3 file loop.c line 4 function main
   // 4 file loop.c line 4 function main
   (27) i!0@1#3 == step!0@1#1
   // 5 file loop.c line 4 function main
   // 3 file loop.c line 4 function main
   // 3 file loop.c line 4 function main
   (28) \guard#1 == !(i!0@1#3 >= 5)
   // 4 file loop.c line 4 function main
   (29) i!0@1#4 == i!0@1#3 + step!0@1#1
        guard: \guard#1
   [...]
   

   The above output is an excerpt from the equation system generated by symbolic execution. We see assignments to the loop counter i turned into equations over its renamed (in static single assignment (SSA) form) instantiations. The loop guard is found as \guard#1.
2. Search for the source location where you expect the constant to appear in the loop guard. In our example, this is "file loop.c line 4."
3. Once you have found the assignment or equality defining the loop guard that doesn't have the expected constant on the right-hand side (in the example, this could be the equality over \guard#1), work backwards from that right-hand side to see where you last had a constant. That is, backwards-search for the name appearing on the right-hand side, which will eventually appear as a left-hand side. Now repeat this process for the new right-hand side of this equation, until the right-hand side is a constant. In the example, the only time we find a constant as right-hand side is the initial assignment, i!0@1#2 == 0.
4. The expression where you flip from is-a-constant to is-a-symbol is the culprit. For our example, this is i!0@1#3 == step!0@1#1. You will then conclude that either this behavior is as expected, meaning your source program does not permit constant propagation (our example does not permit constant propagation, because step is unconstrained; setting it to some constant value will result in bounded loop unwinding), or a shortcoming in CBMC's simplification process. In the latter case, report an issue or contribute a patch to address this.

How do memory pointers work?

A pointer in C points to a memory location. It is a string of 32 or 64 bits interpreted as an unsigned integer denoting a memory address. CBMC, however, interprets this same string of bits as object id followed by an offset into the object denoted by the object id.

CBMC models the heap as a collection of objects. Each object has an id and a size. A pointer consists of an object id and an offset into the object. CBMC encodes the id and offset into a C pointer by using the top bits for the object id and the bottom bits for the offset into the object. By default, CBMC uses the top 8 bits for the object id and the bottom 56 bits for the offset in 64-bit code (and the bottom 24 bits in 32-bit code).

Object id: The number of bits used to represent the object id is 8 by default. It can be changed to K with the flag --object-bits K that is passed to the compiler goto-cc and to cbmc itself. It is important that the same value K be passed to goto-cc and cbmc. If you are using the CBMC starter kit, you set K in your Makefile with

CBMC_OBJECT_BITS = K

You may see CBMC fail with an error message saying that CBMC tried to allocate "too many objects." One option is to increase the number of object bits and see if the problem goes way. Even if this works, it is worth getting your hands dirty and trying to understand why CBMC needs to allocate so many objects for your code. Remember that CBMC is exploring all paths through your code, and has to model all of the objects allocated in all of these paths. In the best case, you will discover a way to reduce the number of objects produced by your code, and produce better code. In the worst case, you may find it prudent to bound the size of a data structure (maybe the size of an input buffer) to bound the number of objects CBMC has to model.

Object offset: The number of bits used to represent the offset into the object is the number of remaining bits in a pointer. This is 56 by default in 64-bit code and 24 by default in 32-bit code.

• The maximum offset is the maximum size of an object that can be modeled in CBMC. This maximum size is smaller than the maximum size that can (at least theoretically) be used in a C program. This is a proof assumption, and it needs to be made clear to the readers or customers of a proof who need to know exactly what CBMC has proved about the code. If you are using the CBMC starter kit, you can access this maximum size using the preprocessor definition CBMC_MAX_OBJECT_SIZE as in the code fragment

  size_t size;
  char *ptr;
  
  __CPROVER_assume(size <= CBMC_MAX_OBJECT_SIZE);
  ptr = (char *) malloc(size);
  

• The offset is a signed integer. In pointer arithmetic, the difference ptr1 - ptr2 can be negative or positive depending on whether ptr1 points before or after ptr2. This means that the maximum size of an object with a 56- or 24-bit offset is actually the maximum positive number that can be represented in 55 or 23 bits. If you are using the CBMC starter kit, this maximum positive number is CBMC_MAX_OBJECT_SIZE.

CBMC provides a few intrinsics that can be useful in a proof harness:

• __CPROVER_POINTER_OBJECT(ptr) is the id of the object denoted by ptr.
• __CPROVER_POINTER_OFFSET(ptr) is the offset into the object denoted by ptr.
• __CPROVER_OBJECT_SIZE(ptr) is the size of the object denoted by ptr.
• __CPROVER_same_object(ptr1, ptr2) is true if ptr1 and ptr2 point to the same object.
• __CPROVER_is_invalid_pointer(ptr) is true if ptr is a valid pointer.

CBMC provides a few functions that can be useful in a proof harness. These functions havoc an object, which means they set all or some of the object to an arbitrary, unconstrained value. The word "havoc" means "widespread destruction". To "wreak havoc" means "to cause great damage". We havoc an object to search for an object value that will induce an issue in our code like a memory safety error or integer overflow.

• __CPROVER_havoc_object(ptr) havocs the entire object denoted by the object id in ptr.
• __CPROVER_havoc_slice(ptr, length) havocs the portion of the object starting at the offset denoted by the object offset in ptr and extending for length bytes.

For more information, see the CBMC tutorial on memory primitives and CBMC builtin functions.

How does malloc work?

CBMC has several models of malloc.

In one model of malloc (the default model), the function never fails to allocate an object on the heap and always returns a valid pointer to a valid object. In particular, malloc will never return NULL, malloc will never run out of memory, and malloc will never fail.

This is a problem if you are using CBMC to check for memory safety issues, because malloc can fail and return NULL, and trying to dereference a null pointer is one of the issues you want to check for.

In other models of malloc, the function can nondeterministically choose to fail and return NULL, and the function will fail if it is asked to allocate an object that is larger than CBMC can model (see the notion of object bits in the discussion of the CBMC memory model). These models of malloc are used when CBMC is invoked with the flags --malloc-may-fail and --malloc-fail-null.

We recommend that you use --malloc-may-fail and --malloc-fail-null. Do not use the default model of malloc. The CBMC starter kit uses both flags by default.

One last comment about malloc: The invocation malloc(0) can return a valid pointer to nothing. The C standard says that invoking malloc with size 0 should return a pointer that can be passed to free but cannot be dereferenced.

What do I do when CBMC won't stop?

CBMC goes through several stages. CBMC can theoretically get stuck in any stage, but the most commonly slow stages are

• Doing the symbolic execution
• Generating the SAT formula from the symbolic execution
• Solving the SAT formula with the SAT solver

Almost always the problem is just one or two lines of code. For example, under certain circumstances something as simple as

  memcpy(dst, src, length);

can cause CBMC to become stuck generating the SAT formula that results from considering all places dst and src might be pointing.

The first problem is to find the line of code. Most programmers are used to delta debugging in which the programmer performs a kind of binary search on the code to find the problem. Delete more and more from the bottom of the function under test until CBMC no longer hangs. The problem is in the last block of code (the last line) deleted that caused CBMC to terminate.

The second problem is to fix the problem. Usually the solution involves some form of function abstraction. It is a known problem, for example, for the standard library functions memcpy, memmove, and memset to be a problem. It is a common solution to abstract these functions to havoc the entire destination object and not just the portion being updated. This works because functions under test commonly copy data to the output and never look at the data actually copied. A simple stub for memcpy would be

void memcpy(char *dst, char *src, size_t length) {
  __CPROVER_havoc(dst);
}

A better stub would check that src and dst are nonnull pointers to nonoverlapping regions of memory. For a good stub, see memcpy in the AWS C Common repository.

A final tip is that sometimes it is interesting to know which stage of CBMC is taking so long. The output of CBMC can general indicate where the problem is. Running CBMC with

  cbmc --flush

will flush to the terminal log messages saying that a given stage is starting or finishing. This usually gives some hint. The most difficult stage to debug is why CBMC is taking so long to generate the SAT formula. If the problem is the SAT solver is taking too long, you may be able to figure out what is going on by running CBMC with one flag at a time (eg, check --bounds-check and then check --unsigned-overflow-check) until you can identify the check that is taking so much time.

CBMC projects

This is a short tutorial on how to use CBMC on a software project. We discuss:

• Project planning: How organize your proof, estimate the effort involved, and estimate the return on investment
• Writing a good proof: What does a good proof look like?
• Debugging an error trace: How to debug and repair an issue discovered by CBMC
• Coding for verification: How to write code to make it easy to prove with CBMC
• Proof evaluation: A checklist for proof writers and reviewers to know when a proof is done

Project planning

How to select what proofs to attempt, in what order

1. Make a dependency graph of the modules in your program. There are a number of tools that can help with this, including doxygen. In addition, you can manually determine a good approximation to the dependency graph using the .h files. If a module includes the .h file of another module, it likely depends on it.
2. Select the leaves of the graph - those modules which other modules depend upon, but which do not depend on other modules themselves. Typically, these include the basic data-structures and algorithms used by the rest of the codebase. Which one of these you choose is a matter of style: you can use the guidelines for coding for verification to help select modules which are likely to be good verification targets.
3. Inside a given module, select the best initial verification target. This is often, but not always, one of the simpler functions. In particular, you are looking for a function which is both easy to verify, and will give good insight into the data-structure invariants of the data-structures used in the given module. The more a function conforms to our guidelines for coding for verification, the easiest it will be to verify. In our experience, it often makes sense to start with allocation or initialization functions (which often have named that end in _alloc() or _init().
4. The first proof for a given module is typically the hardest. It typically requires the creation of an _is_valid() function and an _ensure_is_allocated() function. However, once these have been written once, the remainder of the module becomes much easier. The amount of time needed to complete a proof can vary significantly, from hours for a simple proof to days for a complex one. If the function has few dependencies, and conforms to the guidelines for coding for verification, we would expect an initial proof to take perhaps a day's work.[TODO I made up this number. We need data] If it is taking longer than this, try a different entry-point.

How to get a sense of the work CBMC will involve

We recommend selecting a few (2-3) modules from the leaves of the dependency graph, and then doing 2-3 proofs from each module. This will give you a sense of

1. How much work the first proof in a new module is
2. How much work subsequent proofs in that module is, once the _is_valid() and _ensure_is_allocated() functions are written.

Predicting precisely how hard a piece of code will be to verify can be difficult. In general, however, the more code conforms to our guidelines for coding for verification, the easier it will be to verify. We recommend trying modules of different verification complexity to get a sense of overall expected effort.

Particular features to look for are:

1. Does the code have loops?
   1. If so, are those loops nested? Since CBMC unrolls loops before verifying them, nested loops can lead to a quadratic (or worse) increase in the amount of work CBMC will need to perform.
   2. Are they over fixed sizes, or do they vary with the size of inputs? If loops are of fixed size, it may be hard to simplify the problem if CBMC is having performance issues as the proof is being developed. On the other hand, once the proof is complete, functions with fixed-sized loops may have higher assurance proofs, since data-structures do not need to be bounded for performance reasons.
2. Does the code use inductive data-structures (e.g. linked lists, trees)? Inductive data-structures are much harder to model and verify than linear structures such as arrays.
3. Does the code have function pointers? Function pointers are hard to model. They can also cause performance problems for CBMC.
4. Does the code have an simple and obvious specification? One of the main challenges in verification is writing the specification. The simpler the specification of the code being verified, the easier it is to verify. Similarly, the better the documentation, the easier it is.

Writing a good proof

Table of Contents

• The components of a CBMC proof
• Running example.
• The Proof harness
  • What does a good proof harness look like?
  • How to write a good proof harness
• The Proof Makefile
• The is_valid() function
  • Example of an is_valid() function
• The ensure_allocated function
• Stubs and abstractions
• How do I add the function contract to the function being verified?
  • Example using function contracts

The components of a CBMC proof

A CBMC proof normally consists of several components:

1. A proof harness which:

   1. Sets up required data-structures
   2. Calls the function being verified
   3. Checks any function post-conditions

2. A proof makefile which:

   1. Defines any necessary preprocessor defines e.g. -DMAX_BUFFER_SIZE=10
   2. Specifies the dependencies of the code under test
   3. Specifies any abstractions or models used by proof

   Much of the work done by these Makefiles is common among proofs. We provide a Makefile.common, which provides useful makefile rules shared by all proofs.

3. A set of _is_valid() functions, one for each datatype used in the proof

   1. Typically go in the code-base itself
   2. Can be used in the codebase as assertions to improve runtime checking.
   3. Can be reused by multiple proofs

4. A set of _allocate() and ensure() functions, one for each datatype used in the proof

   1. Due to limitations of the CBMC tools, not all properties about a datatype can be described declaratively. In particular, allocation of memory must be done imperatively. These functions handle allocation of the data-structure, and any recursive substructures.
   2. Can be put in a library and reused by multiple proofs.

5. A library of helper functions which:

   1. Models any external libraries (e.g. libCrypto)
   2. Provides implementations for abstracted functions

The remainder of this document describes how build one of these components.

Running example

We will use the aws_array_list module from the AWS C Common open-source project as our running example. This module provides a polymorphic array defined as follows:

struct aws_array_list {
    struct aws_allocator *alloc;
    size_t current_size;
    size_t length;
    size_t item_size;
    void *data;
};

• alloc represents the allocator used by the list (to allow consumers of the list to override malloc if desired)
• current_size represents the bytes of memory that the array has allocated
• length is the number of items that it contains
• item_size represents the size of the objects stored in the list (in bytes)
• data points to a byte array in memory that contains the data of the array list.

Users of this data structure are expected to access its fields using getter and setter methods, although C does not offer language support to ensure that they do so. Similarly, since the C type system does not have support for polymorphism, authors of the getters and setters are responsible for ensuring that the list is accessed safely. The getter itself is defined as:

int aws_array_list_get_at_ptr(const struct aws_array_list *AWS_RESTRICT list, void **val, size_t index) {
    if (aws_array_list_length(list) > index) {
        *val = (void *)((uint8_t *)list->data + (list->item_size * index));
        return AWS_OP_SUCCESS;
    }
    return aws_raise_error(AWS_ERROR_INVALID_INDEX);
}

The Proof harness

What does a good proof harness look like?

Syntactically, a proof harness looks quite similar to a unit test. The main difference is that a proof harness calls the target function with a partially-constrained input rather than a concrete value; when symbolically executed by CBMC, this has the effect of exploring the function under all possible inputs that satisfy the constraints.

We have developed a style of writing proofs that we believe is readable, maintainable, and modular. This style was driven by feedback from developers, and addresses the need to communicate exactly what we are proving to developers and users.

Our proofs have the following features:

1. They are structured as harnesses that call into the function being verified, similar to unit tests. This makes them easier to write, because they follow a pattern most developers are familiar with. This style also yields more useful error traces. Most importantly, it makes proofs easier to understand and maintain, since a developer reviewing a proof has an "executable" which they can understand using their existing knowledge and intuition about C code.
2. They state their assumptions declaratively. Rather than creating a fully-initialized data structure in imperative style, we create unconstrained data structures and then constrain them just enough to prove the property of interest. This means the only assumptions on the data structure's values are the ones we state in the harness.
3. They follow a predictable pattern: setting up data structures, assuming preconditions on them, calling into the code being verified, and asserting postconditions.

The following code is an example of a proof harness:

void aws_array_list_get_at_ptr_harness() {
    /* initialization */
    struct aws_array_list* list = can_fail_malloc(sizeof(*list));
    __CPROVER_assume(list != NULL));
    __CPROVER_assume(aws_array_list_is_bounded(list));
    ensure_array_list_has_allocated_data_member(list);

    /* generate unconstrained inputs */
    void **val = can_fail_malloc(sizeof(void *));
    size_t index;

    /* preconditions */
    __CPROVER_assume(aws_array_list_is_valid(list));
    __CPROVER_assume(val != NULL);

    /* call function under verification */
    if(!aws_array_list_get_at_ptr(list, val, index)) {
        /* If aws_array_list_get_at_ptr is successful,
         * i.e. ret==0, we ensure the list isn't
         * empty and index is within bounds */
        assert(list->data != NULL);
        assert(list->length > index);
    }

    /* postconditions */
    assert(aws_array_list_is_valid(list));
    assert(val != NULL);
}

The harness shown above consists of five parts:

1. Initialize the data structure to unconstrained values. We recommend initializers for all verified data structures use a consistent naming scheme: ensure_{data_structure}_has_allocated_data_member().
2. Generate unconstrained inputs to the function.
3. Constrain all inputs to meet the function specification and assume all preconditions using assume statements. If necessary, bound the data structures so that the proof terminates.
4. Call the function under verification with these inputs.
5. Check any function postconditions using assert statements.

How to write a good proof harness

We recommend approaching writing a proof-harness as an iterative process:

1. Write a minimally constrained harness, which simply

   1. declares the necessary variables
   2. and then calls the function under test using them.

   For example, for the harness given above, an initial harness might look like:

void aws_array_list_get_at_ptr_harness() {
    /* initialization */
    struct aws_array_list* list;

    /* generate unconstrained inputs */
    void **val;
    size_t index;

    /* call function under verification */
    aws_array_list_get_at_ptr(list, val, index);
}

Note that we are leaving the inputs to the function completely unconstrained: we are simply declaring them on the stack, and then using them without assigning any values to them. In a normal C compiler, this would be undefined behavior. In CBMC, this is legal, but represents an unconstrained value (you may also hear this called a non-deterministic value). The CBMC tool will use a mathematical solver which considers every possible value of an unconstrained variable. If there exists a value which can cause an assertion failure, the solver will find it. Conversely, if the solver says the assertion cannot be violated, this forms mathematical proof that no such value exists.

Leaving these values unconstrained will almost certainly lead to CBMC detecting violations, because real functions have implicit (or, if you're lucky, explicit) constraints on their inputs. For example, it is typically a precondition of a function that pointers must either reference valid memory, or be null. However, sometimes you may be surprised: if a function doesn't use a given input, or uses it in a defensive way, it may accept totally unconstrained values. What we are attempting to do is find the minimum constraint that will allow the function to succeed with no assertion violations. So we start with unconstrained values, and slowly constrain them just enough to get the function to verify.

1. Run CBMC and observe the output. In the case of our running example, you will see errors that look like this

   Errors
     * In include/aws/common/array_list.inl
       * In aws_array_list_get_at_ptr
         * Line 347:
           * [trace] val != ((void*)0) check failed

We have already seen examples of CBMC error traces like this, and we will soon give more guidance on debugging CBMC error traces.

1. Constrain each input in turn until all warnings are resolved. See the sections on writing _is_valid() and _ensure_is_allocated() functions for details on how to do this

2. Fix any loop-unwinding errors. To fix these errors, you will need to update the Makefile with the correct loop bounds. This may cause CBMC to get quite slow. In this case, we recommend bounding the size of data-structures to allow CBMC to finish quickly. In the harness above, this is accomplished by the line

   __CPROVER_assume(aws_array_list_is_bounded(list))
   

   We recommend starting with very small bounds to ensure a quick debug cycle. Once the proof is finished, you can increase the bounds to give proofs for longer lists.

3. Check the coverage report. Ideally, you will have 100% coverage. In practice, coverage will be less than 100%, for e.g. in defensive code that redundantly checks for errors. In this case, inspect the uncovered code, and ensure that it matches your expectations.

4. Strengthen the proof by adding assertions to the harness that check more properties. There are typically three types of such assertions:

   1. Data structures should remain valid, whether or not the function under test succeeded.
   2. If the function failed, data-structures should remain unchanged.
   3. If the function succeeded, data-structures should be updated according to the function semantics.

   In our example harness, this is handled by the lines

    /* call function under verification */
    if(!aws_array_list_get_at_ptr(list, val, index)) {
        /* If aws_array_list_get_at_ptr is successful,
         * i.e. ret==0, we ensure the list isn't
         * empty and index is within bounds */
        assert(list->data != NULL);
        assert(list->length > index);
    }

    /* postconditions */
    assert(aws_array_list_is_valid(list));
    assert(val != NULL);

The Proof Makefile

The Makefile for our running example looks like this:

# Sufficiently long to get full coverage on the aws_array_list APIs
# short enough that all proofs complete quickly
MAX_ITEM_SIZE ?= 2
DEFINES += -DMAX_ITEM_SIZE=$(MAX_ITEM_SIZE)

# Necessary to get full coverage when using functions from math.h
MAX_INITIAL_ITEM_ALLOCATION ?= 9223372036854775808ULL
DEFINES += -DMAX_INITIAL_ITEM_ALLOCATION=$(MAX_INITIAL_ITEM_ALLOCATION)

# This bound allows us to reach 100% coverage rate
UNWINDSET += memcpy_impl.0:$(shell echo $$(($(MAX_ITEM_SIZE) + 1)))

CBMCFLAGS +=

DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
DEPENDENCIES += $(HELPERDIR)/source/utils.c
DEPENDENCIES += $(HELPERDIR)/stubs/error.c
DEPENDENCIES += $(HELPERDIR)/stubs/memcpy_override.c
DEPENDENCIES += $(SRCDIR)/source/array_list.c
DEPENDENCIES += $(SRCDIR)/source/common.c

ENTRY = aws_array_list_get_at_ptr_harness
###########

include ../Makefile.common

1. It defines a set of variables that can be used as bounds in the proof. As discussed above, we recommend starting with small bounds to enable quick iteration on the proof and increasing them once the proof is complete. These variables are created both as Makefile variables, which can be used later (e.g. in the UNWINDSET, and also passed as -D defines, which allow
2. It creates an UNWINDSET which tells CBMC how many times to unroll loops in the program. As shown here, loop bounds typically depend on variables within the Makefile. Its a good idea to make this explicit, as we do here, to avoid the need to change magic constants as you experiment with the proof.
3. A list of CBMCFLAGS if any are needed. Typically, all the required flags are set in the Makefile.common, and this can be left empty
4. A list of DEPENDENCIES, which are the
   1. Project source files
   2. Proof stubs/models [TODO, this really belongs in ABSTRACTIONS]
5. The ENTRY, which is the name of the function being verified
6. include ../Makefile.common to take advantage of the standard templates declared in that file.

Most makefiles should like exactly like this. [TODO discuss wellspring, litani]

The is_valid() function

The is_valid() functions used in preconditions are developed using an iterative process. For each data-structure module, start by specifying the simplest predicates that you can think of for the data structure --- usually, that the data of the data structure is correctly allocated. Then, gradually refine these predicates, until you have a set of reasonable invariants for the data structure.

You can verify that invariants are reasonable by:

1. Having an explicit code-review in which subject matter experts on the development team confirm that the invariants represent the design intent of the code

2. Adding these invariants as pre/post-conditions to the code being verified, and ensuring that all unit and regression tests pass. Note that unit-test failures do not necessarily reflect problems with your invariants. They may also reflect either

   1. Bugs in the code itself
   2. Bugs in the unit-tests

   In both these cases, fix the bug in the code, then make sure the invariant now succeeds during the tests.

Example of an is_valid() function

For instance, in the case of the array_list, we started with the invariant that data points to current_size allocated bytes. After several iterations, the validity invariant for array_list ended up looking like this:

bool aws_array_list_is_valid(const struct aws_array_list *list) {
  if (!list) return false;
  size_t required_size = 0;
  bool required_size_is_valid = (aws_mul_size_checked(list->length, list->item_size, &required_size) == AWS_OP_SUCCESS);
  bool current_size_is_valid = (list->current_size >= required_size);
  bool data_is_valid = ((list->current_size == 0 && list->data == NULL) || AWS_MEM_IS_WRITABLE(list->data, list->current_size));
  bool item_size_is_valid = (list->item_size != 0);

  return required_size_is_valid && current_size_is_valid && data_is_valid && item_size_is_valid;
}

The invariant above describes four conditions satisfied by a valid array_list:

1. the sum of the sizes of the items of the list must fit in an unsigned integer of type size_t, which is checked using the function aws_mul_size_checked
2. the size of the array_list in bytes (current_size) has to be larger than or equal to the sum of the sizes of its items;
3. the data pointer must point to a valid memory location; otherwise it must be NULL if the size of the array_list is zero; This point is actually somewhat subtle: there was debate among the team about whether the pointer must be NULL, or whether any value was legal if the length was zero. Writing an explicit is_valid() function forced the team to come to a precise decision.
4. the item_size must be positive.

The ensure_allocated function

Ideally, all properties in a proof harness would be written in a declarative style. Unfortunately, CBMC currently does not allow to use __CPROVER_assume() statements to assume that memory is correctly allocated for some data structure as a precondition for function verification. Instead, memory must be explicitly allocated in the harness before calling the function under analysis using imperative calls to malloc(). By default, CBMC malloc() never returns null. So it is important that your ensure_allocated function explicitly defines cases where pointers can be null, using adequately placed calls to __CPROVER_assume({some pointer} == null).

It is important to separate the work done in this function from the work done in an is_valid function. This function should only worry about allocating the memory needed by the data-structure. Any other validity constraints should be handled by the is_valid() check.

The ensure function for the running example is:

void ensure_array_list_has_allocated_data_member(struct aws_array_list *const list) {
    if (list->current_size == 0 && list->length == 0) {
        __CPROVER_assume(list->data == NULL);
        list->alloc = can_fail_allocator();
    } else {
        list->data = bounded_malloc(list->current_size);
        list->alloc = nondet_bool() ? NULL : can_fail_allocator();
    }
}

Stubs and abstractions

• TODO

How do I add the function contract to the function being verified?

We strongly recommend adding all checks and assumptions from the proof harness to the function being verified as runtime assertions. This provides value in several ways.

1. It connects the code and the proof. Proofs for all but the most simple functions require environment assumptions. One of the most common ways proof can go wrong is when these assumptions are actually false when the function is called in the real world. Adding the assumptions as runtime assertions in the code allows such mismatches to be detected as the code runs. Some teams choose to enable these assertions only in debug mode; this allows mismatches to be detected during the standard unit and integration testing processes without any performance penalty on production code. Other teams enable these assertions for all builds, providing increased assurance at a small runtime cost.
2. It helps detect bugs in the broader codebase. On a number of occasions, adding function contracts to correct code detected violations of function contracts in other parts of the code base. In several cases, we discovered errors in other projects, which were calling verified APIs with invalid parameters. Even though those projects had never been formally verified, they still benefited from the function contracts developed during the formal verification work.
3. It helps focus the mind. It is easy to let standards slip during code-reviews for test and verification code. "Even if its not perfect, its better than nothing, so might as well just click approve." Adding the proof assumptions and checks to the codebase itself as runtime assertions causes reviewers to take them much more seriously, which leads to both increased proof quality, and improved code quality.

Example using function contracts

In the running example, our verification harness assumed the following preconditions

    __CPROVER_assume(aws_array_list_is_valid(list));
    __CPROVER_assume(val != NULL);

These directly translate into preconditions in the function under test:

    AWS_PRECONDITION(aws_array_list_is_valid(list));
    AWS_PRECONDITION(val != NULL);

Similarly, the key postcondition checked in the verification harness is

    assert(aws_array_list_is_valid(list))

This also directly translates into a postcondition in the function under test:

    AWS_POSTCONDITION(aws_array_list_is_valid(list));

Putting it all together:

int aws_array_list_get_at_ptr(
    const struct aws_array_list* list,
    void **val,
    size_t index)
{
    AWS_PRECONDITION(aws_array_list_is_valid(list));
    AWS_PRECONDITION(val != NULL);
    if (aws_array_list_length(list) > index) {
        *val = (void *)((uint8_t *)list->data +
                        (list->item_size * index));
        AWS_POSTCONDITION(aws_array_list_is_valid(list));
        return AWS_OP_SUCCESS;
    }
    AWS_POSTCONDITION(aws_array_list_is_valid(list));
    return aws_raise_error(AWS_ERROR_INVALID_INDEX);
}

Debugging an error trace

• I see 12 proof failures. How do I select which one to debug?
• How do I debug a proof failure?
  • Read the trace
  • Add additional information to the trace
  • Delta debugging
  • Add assertions to check your hypotheses.
  • Use assert(0) to dump program state leading to a checkpoint
  • Use assume(...) to block uninteresting paths
  • Consider the possibility it is a fault in the code itself
• How do I improve proofs with low coverage?
  • Fix any CBMC errors
  • Check for truly unreachable code.
  • Check for over-constrained inputs
• How can I tell if my proof is over-constrained?
• What should I do if CBMC crashes?

I see 12 proof failures. How do I select which one to debug?

CBMC proof failures seem to come in batches: you run the proof, and see a dozen different errors reported In many cases, these failures are related: instead of stressing about the number of failures, pick one, debug it, and see if fixing it removes (many of) the others. Some good heuristics for deciding which failure to investigate:

1. Look for a failure that occurs early on in the proof. This will often be the one with the shortest trace [TODO viewer should output this information]. The shorter the trace leading to the issue, the easier it is to debug.
2. Look for a failure in code you understand. Some functions are simpler than others: a failure in a simple function is often easier to analyze that one in a complicated function. And a failure in a function you understand is easier than one in a function you are not familiar with.
3. Look for a simple type of failure. For example, the trace from a null dereference is often easier to follow than the traces from other uses of bad pointers. But they're normally exactly the same bug! Since null dereference bugs normally give the simplest traces, start with them first. Often, resolving the null dereference also fixes the other related bugs.

How do I debug a proof failure?

There are a number of techniques that have proven useful in debugging proof failures.

Read the trace

[TODO link to a guide to viewer] CBMC viewer generates a step-by-step trace that leads to the assertion violation. This trace details

• Every line of code executed
• Every function call made
• Every time a variable is assigned

Essentially, this trace contains everything you would get from attaching a debugger to the program, and single stepping until the violation occurred. Take a look at the values of the relevant variables right before the assertion violation. Do they make sense? If not, figure out where they were assigned. I often find that Ctrl-F is my friend here: I search for either the variable name, or the value it was assigned, and see where it appears in the trace.

Similarly, look at the set of function calls that led to the error. Do they make sense? Are there functions you expect to see there, but don't? Are there functions you didn't expect to see there, but do?

Add additional information to the trace

The trace has all the information you need to understand the state of program memory at every point during the execution. But its not always that easy to reconstruct. In particular, the trace records the value of a variable when it is written to. But it doesn't record the value of a variable that is only read, or passed along to another function.

You can solve this by adding "dummy writes" to the program. For example, let's say you were debugging an error that involved the following function

int foo(struct bar* b, int x) {
    baz(b->data, x);
}

Figuring out the value of b->data and x are possible given a complete trace, but its difficult. Any it might harder to figure out the value of b->size. Instead, annotate the code to track those values:

int foo(struct bar* b, int x) {
        struct bar debug_foo_b = *b;
        int debug_foo_x = x;
    baz(b->data, x);
}

the trace will now contain an assignment to debug_foo_b, which will let you see what values each member of the struct had.

Delta debugging

Delta debugging is a powerful technique for localizing faults and creating minimal reproducing test-cases. Essentially, you modify the program in some way, typically either by removing (commenting out) or modifying code. You then rerun the verification tool, and see if the results changed. The goal is to either:

1. produce a small program which still displays the bug or
2. produce a small change between two programs, one of which has the bug, and the other doesn't.

In case 1, you now have a small program which is hopefully easy to understand; In case 2, you have a small change which induces the bug, and hopefully leads you toward the root cause.

Add assertions to check your hypotheses.

For example, consider the case of a null pointer dereference of a pointer p. It is important to distinguish the case where the pointer must be null, vs the case where it may be null, vs the case where it is never null. You can test for these cases by adding assert(p) to the function. If the can be null, the assertion will trigger. If it cannot be null, the assertion will succeed.

Now, check assert(!p) instead. If can be non-null, this assertion will fail. If it can only be null, this assertion will succeed.

You now know which one of the three cases is true. And you can use the trace to see why it can be null/non-null.

You can do similar things to determine why a branch is reachable, or unreachable.

Use assert(0) to dump program state leading to a checkpoint

Sometimes, you want to know how/whether a particular line of code is reachable. One easy way to learn that is to put assert(0) right before the line. CBMC will detect the assertion violation, and give a trace explaining how it reached there, and with what values. If the assertion passes without error, you know that the line is unreachable given the current proof harness.

Use assume(...) to block uninteresting paths

There are often many possible execution paths that reach a given line of code / assertion. Some of these may reflect cases you are trying to understand, while others do not help with your current debugging plan. Left to its own devices, CBMC will non-deterministically choose one of those traces, which may not be the one you want. You can guide CBMC to the trace you want by sprinkling __CPROVER_assume() statements within the code. For example, you might __CPROVER_assume() that a function fails with an error code, to test whether the calling function handles that error code correctly. Or you might __CPROVER_assume() that a given variable is null, to simplify you search for the root cause of a null dereference.

Consider the possibility it is a fault in the code being verified

In many cases, the error detected by CBMC represents a true issue within the code being verified. This is particularly common in the case of functions which fail to validate their inputs. In this case, the fix is either to validate the inputs, and return an error if given invalid inputs, or to document the requirements on the inputs, and state that actions on illegal inputs are undefined behavior. Which solution you choose depends on the risk profile of the code.

It is also common that code being verified has integer-overflows and other errors that only occur in unusual circumstances. In these cases, the solution is to either guarantee that inputs are sufficiently small to prevent these issues, or to use overflow-safe built-ins, such as gcc's __builtin_mul_overflow (documented here).

How do I improve proofs with low coverage?

Fix any error detected by CBMC

Make sure that there are no missing function definitions, or property violations. Both of these errors can affect coverage calculations.

Check for truly unreachable code.

In some cases, code may be truly unreachable - for example, redundant defensive checks. Or this may be code which is reachable using particular inputs, but not in the context of your proof. For example:

int size_from_enum(type_enum t) {
        switch (t) {
        case BAR: return 1;
        case BAZ: return 2;
        ...
}

int function_being_tested() {
        return size_from_enum(BAZ);
}

In this case, most of the lines in size_from_enum will appear to be unreachable, even though the proof has full coverage of all truly reachable paths.

Check for over-constrained inputs

Consider the case where one side of a branch is not reached, or where execution does not continue past an assumption. In this case, it is possible that the inputs have been over-constrained in the proof harness. You can try to relax some of the __CPROVER_assume() statements.

How can I tell if my proof is over-constrained?

This will normally appear in coverage - over-constrained proofs will usually have unreachable portions of code. You can also add a "smoke test", but adding assertions that you expect to fail to the code (which can be as simple as assert(0)). If these assertions do not fail, then something is wrong with your proof.

What should I do if CBMC crashes?

1. Make a new branch in your project, containing the exact code that caused cbmc to crash. We recommend giving it a name like cbmc-crashing-bug-1.
2. Push it to a public github repo (if possible)
3. Post a bug report here, linking to the branch that you pushed containing the bug.
4. Post a bug report on this repo, linking to the bug that you posted on the main CBMC repo.

Coding for verification

The basic principles of coding for verification are similar to those of coding for testability, with some modifications due to the nature of the SAT solver underlying CBMC.

Code Organization to Support Verification

• Write small functions. Functions should:
  • Do exactly one thing.
  • Take all their input and outputs through function parameters and rely as little as possible on global state. Where possible, avoid global variables.
• Encapsulate interaction with the environment within a small function. Interaction with the environment includes accessing files, the network, etc. This makes is possible to verify that function independently and then stub it out for the rest of the verification.
• Functions should check their input parameters, and return an error code when they fail to verify. This makes harnesses much simpler, since any value for the parameters is a valid input to the function.
• Avoid unbounded loops as far as possible, and encapsulate the ones that you need. CBMC does bounded model checking, so we need to be able to compute a bound on the number of iterations of any given loop. Loops that iterate a constant number of times are best. Loops whose iteration depends on input will require making some assumptions about the input.
• Consider defining magic numbers that control loop bounds and buffer sizes in your build system, i.e., -DBUFFER_SIZE=1024 and similar. This ensures that you can configure this value at build time, and we can also use those values in our proofs.
• Provide an easy way to access static functions and data structures for testing, if you must have them. For example, use a macro that overrides static.
• Make threads independently verifiable. When writing concurrent programs, reduce interaction to well-defined points. This enables verification of each thread in isolation.

Improving Verification Performance

• Avoid void pointers (void*). There are two reasons people use void pointers:
  • To hide implementation detail. This use of void pointers is unnecessary, because we can replace void *bar with struct foo *bar and declare struct foo later within the implementation.
  • To implement a form of polymorphism. Don't do this for gratuitous reasons (e.g., because it might someday be useful). Void pointers can block constant propagation which can dramatically reduce the size of the formula constructed for the constraint solver.
• Avoid function pointers. When unavoidable, ensure that function pointer types match a minimum number of candidate functions signatures in your code base (ideally just one). They really can make the difference between a proof and no proof. When CBMC encounters a function pointer, it has to consider all possibilities for what that function could be, based on loose signature matching. CBMC has to consider possible any function in the entire program whose address is taken with a signature matching the function pointer. So for each function invocation, the symbolic execution of a single function is replaced with the symbolic execution of a collection of functions (including the functions they call), and the combinatorial explosion makes the size of the formula too big for memory. The worst thing you can do is to give your functions the signature void foo(void *arg); see the point above about avoiding void*.
• Large (more than several kB in size) arrays can cause trouble. Again, defining the sizes of arrays in the build system means that we can cleanly re-define them to smaller bounds for our proofs.
• Data-structures should explicitly carry their size, as a parameter (e.g., Pascal strings are better than C strings).
• Stay type safe.
  • Allocate the correct size of objects. Don't allocate less than the correct size for a struct even if you're only using some of its fields.
• Consider encapsulating loops in a function, or even just the loop body. Nested loops can lead to a combinatorial explosion in the size of the formula sent to the constraint solver. Encapsulated loops can be specified and validated in isolation, and the simpler specification can be used in place of the function in the rest of the validation.
• Try to minimize string comparisons
• E.g., instead of making a string->string hash table, consider an enum->string hash-table.

Proof evaluation

This is a check list intended for

• proof writers to use before checking a proof into a repository and
• proof reviewers to use during the code review of a pull request containing a proof.

This check list is intended to ensure clear answers to two questions:

• What properties are being checked by the proof?
• What assumptions are being made by the proof?

and that these answers can be found in one of three places:

• The proof harness,
• The proof makefiles (and, with the starter kit, these makefiles are the proof Makefile, the project Makefile-project-defines, and the project Makefile.common), and perhaps
• The proof readme file.

The best practices for writing a proof are described in Write a good proof. Reviewers should keep these best practices in mind when reading a proof. We recommend that any deviations from best practices be explained in the readme file.

Properties checked

Check the following:

• All of the standard property-checking flags are used:

    * --bounds-check
    * --conversion-check
    * --div-by-zero-check
    * --float-overflow-check
    * --malloc-fail-null
    * --malloc-may-fail
    * --nan-check
    * --pointer-check
    * --pointer-overflow-check
    * --pointer-primitive-check
    * --signed-overflow-check
    * --undefined-shift-check
    * --unsigned-overflow-check
  

  Note that the starter kit uses these flags by default. The properties checked by these flags is documented on the CPROVER website. Note, however, that a developer may disable any one of these flags by editing project Makefile.common or by setting a makefile variable to the empty string (as in CBMC_FLAG_MALLOC_MAY_FAIL = ) in the project Makefile-project-defines or a proof Makefile. These are the places to look for deviations.

• All deviations from the standard property-checking flags are documented.

  There are valid reasons to omit flags either for a project or for an individual proof. But the decision and the reason for the decision must be documented either in a project readme or a proof readme file.

CBMC checks assertions in the code. This is understood and need not be documented.

Assumptions made

Check the following:

• All nontrivial data structures have an ensure_allocated function as described in the training material.

  Feel free to use any naming scheme that makes sense for your project --- some projects use allocate_X in place of ensure_allocated_X --- but be consistent.

• All nontrivial data structures have an is_valid() predicate as described in the training material for every nontrivial data structure.

• All definitions of ensure_allocated functions and is_valid predicates appear in a common location.

  These definitions are most commonly stored in the proofs/sources subdirectory of the starter kit. Definitions are stored here and used consistently in the proofs.

• All pointers passed as input are allocated on the heap with malloc.

  One common mistake is to allocate a buffer buf on the stack and to pass &buf to the function under test in the proof harness. This prevents the proof from considering the case of a NULL pointer.

• All instances of __CPROVER_assume appear in a proof harness.

  Note that some exceptions are required. For example, it may be necessary in an ensure_allocated to assume length < CBMC_MAX_OBJECT_SIZE before invoking malloc(length) to avoid a false positive about malloc'ing a too-big object. But every instance of __CPROVER_assume in supporting code should be copied into the proof harness. The goal is for all proof assumptions to be documented in one place.

• All preprocessor definitions related to bounds on input size or otherwise related to proof assumptions appear in the proof Makefile.

  In particular, do not embed definitions in the supporting code or header files. The goal is for all proof assumptions to be documented in one place.

• Confirm that all stubs used in the proof are acceptable abstractions of the actual code.

  Acceptable could mean simply that every behavior of the original code is a behavior of the abstraction.

Results checked

Look at the report in the checks attached to the pull request.

• Confirm that the coverage is acceptable and confirm that the readme file explains the reason for any lines not covered.

• Confirm that the list of missing functions is acceptable.

• Confirm that there are no errors reported.

Other things to consider

• Consider writing function contracts for the function under test as described in Write a good proof. The check list above ensures that the properties (including the assumptions about the input) that must be true before function invocation are clearly stated in the proof harness. Consider adding a statement of what properties must be true after function invocation as assertions at the end of the proof harness.

• Consider adding the assumptions made by the proof harness for a function under test to the source code for the function in the form of assertions in the code. This will validate that the assumptions made by the proof of a function are satisfied by each invocation of the function (at least during testing).

CBMC projects

Here is a list of software projects that contain some CBMC verification work.

• AWS C Common (cbmc)
• AWS Encryption SDK for C (cbmc)
• AWS IoT Device Defender Library (cbmc)
• AWS IoT Device Shadow Library (cbmc)
• AWS IoT Fleet Provisioning Library (cbmc)
• AWS IoT Jobs Library (cbmc) (cbmc)
• AWS IoT Over-the-air Update Library (cbmc)
• AWS SigV4 Library (cbmc)
• AWS s2n (cbmc)
• Amazon FreeRTOS (cbmc)
• FreeRTOS (cbmc)
• FreeRTOS Cellular Interface (cbmc)
• FreeRTOS coreHTTP Client Library (cbmc)
• FreeRTOS coreJSON Library (cbmc)
• FreeRTOS coreMQTT Agent Library (cbmc)
• FreeRTOS coreMQTT Client Library (cbmc)
• FreeRTOS corePCKS11 Library (cbmc)
• FreeRTOS coreSNTP Library (cbmc)
• FreeRTOS TCP (cbmc)

CBMC resources

• CBMC home page
• CBMC github repository
• Papers
• Blog posts
• Talks

Papers

CBMC technology

• Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking. Daniel Kroening, Edmund Clarke, and Karen Yorav. In Proceedings of Design Automation Conference (DAC), pages 368-371, 2003.
  • This is the original paper on CBMC that was later expanded into the following CMU technical report, which includes a good description of CBMC's internal architecture:
  • Behavioral Consistency of C and Verilog Programs. Edmund Clarke, Daniel Kroening, Karen Yorav. CMU-CS-03-126, May 2003.
• A number of further applications of CBMC can be found online.

CBMC applications

• Model checking boot code from AWS data centers. Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle. Formal Methods in System Design, volume 57, number 1, pages 34-52, July 2021.

  • This paper originally appeared in the following paper at CAV 2018:
  • Model Checking Boot Code from AWS Data Centers. Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle: In Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018), pages 267-486, July 2018.

• Code-level model checking in the software development workflow at Amazon Web Services. Nathan Chong, Byron Cook, Jonathan Eidelman, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle. Journal of Software: Practice and Experience --- Special Issue: Introduction to the Special Issue on Software Engineering in Practice, volume 51, issue 4, pages 772-797, April 2021.

  • This paper originally appears in the following paper at ICSE 2020:
  • Code-Level Model Checking in the Software Development Workflow. Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP 2020), pages 11–20, June 2020.

Blog posts

• Daniel Schwartz-Narbonne shares how automated reasoning is helping achieve the provable security of AWS boot code in the AWS Security Blog. Supriya Anand. October 2, 2018.

• Ensuring the Memory Safety of FreeRTOS Part 1 and Part 2 in the FreeRTOS Blog. Nathan Chong, February and May 2020.

Talks

• Code-level model checking in the software development workflow, Daniel Schwartz-Narbonne, ICSE 2020 conference talk.