Documentation

• A set of slides about the detection of software vulnerabilities using ESBMC:
  • Part I
  • Part II
  • Part III
• This software security course describes further implementation details about ESBMC.

ESBMC Features

• User specified assertion failures;
• Out of bounds array access;
• Illegal pointer dereferences, such as:
  • Dereferencing null;
  • Performing an out-of-bounds dereference;
  • Double-free of malloc'd memory;
  • Misaligned memory access;
• Integer overflows;
• NaN (Floating-point);
• Divide by zero;
• Memory leak.

Concurrent software (using the pthread API) is verified by explicitly exploring interleavings, thus producing one symbolic execution per interleaving. By default, pointer-safety, array-out-of-bounds, division-by-zero, and user-specified assertions will be checked for; one can also specify options to check multi-threaded programs for:

• Deadlock (only on pthread mutexes and conditional variables);
• Data races (i.e., competing writes);
• Atomicity violations at visible assignments;
• Lock acquisition ordering.

By default, ESBMC performs a "lazy" depth-first search of interleavings but can also encode (explicitly) all interleavings into a single SMT formula. Currently, many SMT solvers are supported:

• Z3 4.9+;
• Boolector 3.2+;
• MathSAT 5.6+;
• CVC4 1.8;
• Yices 2.6+;
• Bitwuzla 0.3+;

In addition, ESBMC can be configured to use the SMTLIB interactive text format to write the formula to a file or interactively with a pipe to communicate with an arbitrary solver process, although insignificant overheads are involved. See the section on supported SMT backends for details.

ESBMC uses clang as its front-end, which brings several advantages:

• We address the problem of maintaining a frontend for C and C++ simply and elegantly: by using clangs API to access and traverse the program AST, without having details of the input program compiled away.
• ESBMC provides compilation error messages as expected from a compiler.
• ESBMC leverages clang’s powerful static analyzer to provide meaningful warnings when parsing the program.
• Clang can simplify some expressions, e.g., calculate sizeof/alignof expressions, evaluate static asserts, evaluate if a dynamic cast is always null, etc., which eases the analysis of the input program.

A limited subset of C++98 is supported too -- a library modeling the STL is also available.

To check all available options of the ESBMC tool, type:

esbmc --help

Modeling with non-determinism

ESBMC extends C with three modeling features:

__ESBMC_assert(e): aborts execution when e is false.

void __ESBMC_assert (e, "some message here");

nondet_X(): returns non-deterministic X-value, with X in {bool, char, int, float, double, loff_t, long, pchar, pthread_t, sector_t, short, size_t, u32, uchar, uint, ulong, unsigned, ushort} (no side effects, pointer for void *, etc.). ESBMC assumes that the functions are implemented according to the following template:

X nondet_X () { X val; return val; }

__ESBMC_assume(e): “ignores” execution when e is false, no-op otherwise.

void __ESBMC_assume(e);

__ESBMC_atomic_begin(), __ESBMC_atomic_end(): For modeling an atomic execution of a sequence of statements in a multi-threaded run-time environment, those statements can be placed between two function calls.

__ESBMC_atomic_begin();
//shared memory
__ESBMC_atomic_end();

__ESBMC_init_object(): Initialize a memory object. This can be used to mark any pointer or symbol as non-determnistic.

my_complex_type T = {0,0,0};
__ESBMC_init_object(T);

As an illustrative example to show some of the ESBMC features to model non-determinism, consider the following C code:

int main() {
  int x=nondet_int(),y=nondet_int(),z=nondet_int();
  __ESBMC_assume(x > 0 && y > 0 && z > 0);
  __ESBMC_assume(x < 16384 && y < 16384 && z < 16384);
  assert(x*x + y*y != z*z);
  return 0;
}

Here, ESBMC is invoked as follows:

esbmc file.c

For this particular C program, ESBMC produces the following counterexample:

Counterexample:

State 1 file file.c line 2 function main thread 0
----------------------------------------------------
x = 252 (00000000 00000000 00000000 11111100)

State 2 file file.c line 2 function main thread 0
----------------------------------------------------
y = 561 (00000000 00000000 00000010 00110001)

State 3 file file.c line 2 function main thread 0
----------------------------------------------------
z = 615 (00000000 00000000 00000010 01100111)

State 6 file file.c line 5 function main thread 0
----------------------------------------------------
Violated property:
file file.c line 5 function main
assertion
(_Bool)(x * x + y * y != z * z)

VERIFICATION FAILED

Quantifiers

ESBMC now supports universal (forall) and existential (exists) quantifiers in SMT-based verification.

New Expressions

The following two expressions have been introduced:

• bool forall(symbol, predicate) - Evaluates if the predicate holds for all possible values of symbol.
• bool exists(symbol, predicate) - Evaluates if the predicate holds for at least one value of symbol.

Function Declarations

extern void __ESBMC_assume(_Bool);
extern _Bool __ESBMC_forall(void *, _Bool);
extern _Bool __ESBMC_exists(void *, _Bool);

Example Usage

int main() {
unsigned n;
int arr[n];
unsigned i;

__ESBMC_assume(__ESBMC_forall(&i, !(i < n) || arr[i] == 2));
__ESBMC_assert(!__ESBMC_exists(&i, (i < n) && arr[i] == 42), "forall init");

arr[n/2] = 42;
__ESBMC_assert(!__ESBMC_exists(&i, (i < n) && arr[i] == 42), "this assertion should fail");
}

Another Example

int zero_array[10];
int main() {
int sym;
__ESBMC_assert(
  __ESBMC_forall(&sym, !(sym >= 0 && sym < 10) || zero_array[sym] == 0),
  "array is zero initialized"
);

const unsigned N = 10;
unsigned i = 0;
char c[N];
for (i = 0; i < N; ++i) c[i] = i;

unsigned j;
__ESBMC_assert(
  __ESBMC_forall(&j, j > 9 || c[j] == j), "array is initialized correctly"
);
}

esbmc file.c --z3

Limitations

• Currently, only Z3 is supported (no SMT-LIB support).
• Only one symbol is supported in quantifiers. Future work will enable multiple symbols.
• Recursive quantifiers (e.g., nested forall statements) are not yet supported.
• There is a known issue where a constant-bounded symbol might cause incorrect simplifications.

Falsification

esbmc file.c --falsification

Our falsification approach (--falsification) uses an iterative technique and verifies the program for each unwind bound up to either a maximum default value of 50 (which can be changed via --max-k-step nr), or indefinitely (until it exhausts the time or memory limits). Intuitively, we aim to find a counterexample with up to k loop unwindings. The algorithm relies on the symbolic execution engine to increasingly unwind the loop after each iteration.

This approach replaces all unwinding assertions (e.g., assertions to check if a loop was completely unrolled) with unwinding assumptions. Normally, this would lead to unsound behaviour but, since the falsification algorithm cannot provide correctness validation, it will not affect the search for bugs. This approach is focused on bug finding and does not care if a loop was not completely unrolled; it only cares if the current number of unwindings will lead to a property violation.

The falsification algorithm also offers the option to change the granularity of the increment; the default value is 1, but can be increased in order to meet any expected behaviour via --k-step nr. Note that changing the value of the increment can lead to slower verification time and might not present the shortest counterexample possible for a property violation.

Incremental BMC

esbmc file.c --incremental-bmc

Our incremental BMC approach (--incremental-bmc) uses an iterative technique and verifies the program for each unwind bound up to either a maximum default value of 50, which can be modified via --max-k-step nr, or indefinitely (until it exhausts the time or memory limits). Intuitively, we aim to either find a counterexample with up to k loop unwinding or to fully unwind all loops so we can provide a correct result. The algorithm relies on the symbolic execution engine to increasingly unwind the loop after each iteration of the algorithm.

The approach is divided in two steps: one that tries to find property violations and one that checks if all the loops were fully unwound. When searching for property violation, the tool replaces all unwinding assertions (e.g., assertions to check if a loop was completely unrolled) with unwinding assumptions. Normally, this would lead to unsound behaviour, however, the first step can only find property violations and reporting an unwinding assertion failure is not a real bug. The next step is to check if all loops in the program were fully unrolled. This is done by checking if all the unwinding assertions are unsatisfiable; note that checking any other assertion in the program, for the current k, is not necessary as they were already verified.

The algorithm also offers the option to change the granularity of the increment; the default value is 1, but can be increased in order to meet any expected behaviour via --k-step nr. Note that changing the value of the increment can lead to slower verification time and might not present the shortest counterexample possible for the property violation.

k-Induction proof rule

esbmc file.c --k-induction

The original k-induction algorithm (--k-induction) presented by Sheeran et al. [1] was used to prove safety properties in hardware verification. The algorithm was later refined by Alastair et al. [2] and applied to the verification of general C programs. Our algorithm is a combination of both approaches. It can be summarized as follows:

Here B(k) is the base case, F(k) is the forward condition and I(k) is the inductive step; k is the number of loop unwinding used for each step. For the base case we use the plain BMC technique, hence we can only find property violations here. If the base case error check is satisfiable, then the algorithm presents a counterexample of length k. For the forward condition and inductive step, the base case must be checked for satisfiability before the result is presented. This is a soundness requirement of the technique.

The forward condition attempts to prove that all loops in the program were fully unrolled; this is achieved by adding unwinding assertions after all loops. The forward condition is further optimized to only check the unwinding assertions, as all program assertions are already proven to be unsatisfiable by the base case, for the current value of k. The inductive step attempts to prove that, if the property is valid for k iterations, then it must be valid for the next iteration; this is achieved by assigning nondeterministic values to all variable written inside a loop body, assuming k-1 invariants and checking if the invariant holds at the kth iteration.

The algorithm starts with k = 1. It increases it up to a maximum number of iterations, incrementally analysing the program, until it either finds a bug (i.e., the base case is satisfiable for some k), proves correctness (i.e., the base case is unsatisfiable and either the forward condition or inductive step is unsatisfiable for some k), or exhausts either time or memory constraints.

Loop Invariant Support

esbmc file.c --loop-invariant

ESBMC now supports user-provided loop invariants as an alternative to expensive loop unwinding. This approach is particularly beneficial for programs with large loop bounds or unbounded loops, where traditional k-induction may become computationally prohibitive or hit iteration limits.

Loop invariants are specified using the built-in function __ESBMC_loop_invariant(condition) placed within the loop body. When the --loop-invariant option is enabled, ESBMC transforms the loop using the standard k-induction approach:

1. Base case verification: Check that the invariant holds upon loop entry
2. Inductive step: Assume the invariant holds, execute one loop iteration, and verify the invariant still holds
3. Property verification: After loop exit, use the invariant to prove the target property

Example: Basic Loop Invariant Usage

int main() {
int i = 0;
int sum = 0;

__ESBMC_loop_invariant(i >= 0 && i <= 1000 && sum == i * 10);
while (i < 1000) {
  sum += 10;
  i++;
}

assert(sum == 10000);  // Successfully verified
  return 0;
}

The loop invariant approach has been tested on various benchmark programs from the k-induction test suite, successfully verifying several cases that previously resulted in "VERIFICATION UNKNOWN" verdicts due to unwinding limitations, including check_if, count_down, and count_up_down.

Known Limitations

We can also use additional options together with the k-induction proof rule to produce (inductive) invariants:

1. --interval-analysis: enable interval analysis for integer variables and add assumes to the program.
2. --add-symex-value-sets: enable value set analysis for pointers and add assumes to the program.
3. --loop-invariant: enable user-provided loop invariants to avoid expensive loop unwinding.

The loop invariant feature is completely opt-in and maintains backward compatibility with existing verification workflows. Programs without loop invariant annotations continue to use the standard k-induction unwinding approach.

[1] Mary Sheeran, Satnam Singh, Gunnar Stålmarck: Checking Safety Properties Using Induction and a SAT-Solver. FMCAD 2000: 108-125

[2] Alastair F. Donaldson, Leopold Haller, Daniel Kroening, Philipp Rümmer: Software Verification Using k-Induction. SAS 2011: 351-368

Verification of modules that rely on larger structures

ESBMC can verify code that relies on existing infrastructures and must be compliant with those. Consider the following C program where the verification engineer wants to check whether the assert-statement in line 8 holds.

1 #include "lib.h"
2 // Running with esbmc  --overflow-check main.c lib.c
3 int main() {
4   int64_t a;
5   int64_t b;
6   int64_t r;
7   if (mul(a, b, &r)) {
8   __ESBMC_assert(r == a * b, "Expected result from multiplication");
9   }
10   return 0;
11 }

The function mul is implemented in the library “lib.h”, which is located under “/lib”. Here, ESBMC is invoked as follows:

esbmc main.c --overflow-check -I lib/ lib/lib.c

where main.c is the C program to be checked, --overflow-check enables arithmetic over- and underflow check, and -I path sets the include path. For this particular C program, ESBMC produces the following counterexample:

Counterexample:

State 1 file lib.c line 14 function mul thread 0
----------------------------------------------------
Violated property:
file lib.c line 14 function mul
arithmetic overflow on mul
!overflow("*", a, b)

VERIFICATION FAILED

The library header and implementation files located under /lib are:

1 #include <stdint.h>
2 _Bool mul(const int64_t a, const int64_t b, int64_t *res);

1 #include "lib.h"
2 _Bool mul(int64_t a, int64_t b, int64_t *res) {
3   // Trivial cases
4   if((a == 0) || (b == 0)) {
5   *res = 0;
6   return 1;
7   } else if(a == 1) {
8   *res = b;
9   return 1;
10   } else if(b == 1) {
11   *res = a;
12   return 1;
13   }
14   *res = a * b; // there exists an overflow
15   return 1;
16 }

Verification of Python Programs

To enable the verification of Python programs, build ESBMC with the option:
'-DENABLE_PYTHON_FRONTEND=On'.

Users can specify the Python interpreter binary using a flag.

Python frontend:
--python path             Python interpreter binary to use 
                  (searched in $PATH; default: python)

esbmc main.py --python python2.7

ESBMC version 7.6.1 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing main.py
Python version: 2.7.18
ERROR: Please ensure Python 3 is available in your environment.

esbmc main.py --python python3

ESBMC version 7.6.1 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing main.py
Converting
Loading model: range.py
Loading model: int.py
Generating GOTO Program
GOTO program creation time: 0.151s
GOTO program processing time: 0.002s
Starting Bounded Model Checking
Symex completed in: 0.002s (14 assignments)
Slicing time: 0.000s (removed 10 assignments)
Generated 9 VCC(s), 2 remaining after simplification (4 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
Solving with solver Boolector 3.2.3
Runtime decision procedure: 0.000s
BMC program time: 0.003s

VERIFICATION SUCCESSFUL

Consider the following Python file, named main.py:

def factorial(n:int) -> int:
if n == 0 or n == 1:
  return 1
else:
  return n * factorial(n - 1)

n:int = nondet_int()
__ESBMC_assume(n > 0);
__ESBMC_assume(n < 6);

result:int = factorial(n)
assert(result != 120)

Run ESBMC on the Python file using the following command:

ESBMC will analyze the program and detect the assertion violated when 'factorial' is invoked with the value 5. The counterexample generated by the tool will demonstrate this:

[Counterexample]


State 1 file main.py line 7 column 0 thread 0
----------------------------------------------------
n = 5 (00000000 00000000 00000000 00000101)

State 4  thread 0
----------------------------------------------------
Violated property:
assertion
result != 120


VERIFICATION FAILED

Bug found (k = 5)

The --function flag can be used to verify a single function instead of the entire file:

1 // SPDX-License-Identifier: GPL-3.0
2 pragma solidity >=0.4.26;
3
4 contract MyContract {
5
6   function func_array_loop() external pure {
7   uint8[2] memory a;
8
9   a[0] = 100;
10  for (uint8 i = 1; i < 3; ++i)
11  {
12    a[i] = 100;
13    assert(a[i-1] == 100);
14  }
15  }
16 }

esbmc --sol example.sol example.solast --contract MyContract --function func_array_loop --incremental-bmc

solc --ast-compact-json example.sol > example.solast

Counterexample:

State 1 file example.sol line 1 function func_array_loop thread 0
----------------------------------------------------
a[0] = 100 (01100100)

State 2 file example.sol line 1 function func_array_loop thread 0
----------------------------------------------------
a[1] = 100 (01100100)

State 4 file example.sol line 1 function func_array_loop thread 0
----------------------------------------------------
Violated property:
file example.sol line 1 function func_array_loop
array bounds violated: array `a' upper bound
(signed long int)i < 2


VERIFICATION FAILED

Bug found (k = 2)

pragma solidity >=0.8.0;

contract Robot {
int x = 0;
int y = 0;

function moveLeftUp() public {
  --x;
  ++y;
}

function moveLeftDown() public {
  --x;
  --y;
}

function moveRightUp() public {
  ++x;
  ++y;
}

function moveRightDown() public {
  ++x;
  --y;
}

function inv() public view {
  assert((x + y) % 2 != 0);
}
}

esbmc --sol example.sol example.solast --contract Robot --k-induction

[Counterexample]


State 1 file example.sol line 13 function moveLeftDown thread 0
----------------------------------------------------
x = -2 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111110)

State 2 file example.sol line 14 function moveLeftDown thread 0
----------------------------------------------------
y = 0 (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 3 file example.sol line 18 function moveRightUp thread 0
----------------------------------------------------
x = -1 (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)

State 4 file example.sol line 19 function moveRightUp thread 0
----------------------------------------------------
y = 1 (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)

State 5 file example.sol line 23 function moveRightDown thread 0
----------------------------------------------------
x = 0 (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 6 file example.sol line 24 function moveRightDown thread 0
----------------------------------------------------
y = 0 (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 7 file example.sol line 28 function inv thread 0
----------------------------------------------------
Violated property:
file example.sol line 28 function inv
assertion
(x + y) % 2 != 0


VERIFICATION FAILED

esbmc file.c --multi-property

int main()
{
  int x = 0;
  while (nondet_int()) {
    if (!x) {
      assert(x == 0);
      x = 1;
    }
    else if (x == 1) {
      assert(x > 0);
      x = 2;
    }
    else if (x == 2) {
      assert(x >= 2);
      x = 3;
    }
  }
  assert(x == 3);
}

[Counterexample]


State 1 file example.c line 24 column 3 function main thread 0
----------------------------------------------------
Violated property:
file example.c line 24 column 3 function main
x == 3
0

Slicing time: 0.000s (removed 0 assignments)
No solver specified; defaulting to Boolector
Solving claim 'x == 0' with solver Boolector 3.2.2
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.001s
Solving with solver Boolector 3.2.2
Runtime decision procedure: 0.000s

[Counterexample]


State 1 file example.c line 10 column 7 function main thread 0
----------------------------------------------------
Violated property:
file example.c line 10 column 7 function main
x == 0
0


[Coverage]

Total Asserts: 4
Total Assertion Instances: 4
Reached Assertion Instances: 2
Assertion Instances Coverage: 50%

VERIFICATION FAILED

Bug found (k = 1)

[Coverage]

!((_Bool)return_value$_nondet_int$1 != 0)   file example.c line 6 column 3 function main : SATISFIED
(_Bool)return_value$_nondet_int$1 != 0    file example.c line 6 column 3 function main : SATISFIED
!((_Bool)x != 0)    file example.c line 8 column 5 function main : SATISFIED
(_Bool)x != 0 file example.c line 8 column 5 function main : SATISFIED
!(x == 1)   file example.c line 13 column 10 function main : SATISFIED
x == 1    file example.c line 13 column 10 function main : SATISFIED
!(x == 2)   file example.c line 18 column 10 function main : SATISFIED
x == 2    file example.c line 18 column 10 function main : SATISFIED
!(x == 3)   file example.c line 24 column 3 function main : SATISFIED
x == 3    file example.c line 24 column 3 function main : SATISFIED
x == 0    file example.c line 10 column 7 function main : SATISFIED
!(x == 0)   file example.c line 10 column 7 function main : UNSATISFIED
x > 0 file example.c line 15 column 7 function main : SATISFIED
!(x > 0)    file example.c line 15 column 7 function main : UNSATISFIED
x >= 2    file example.c line 20 column 7 function main : SATISFIED
!(x >= 2)   file example.c line 20 column 7 function main : UNSATISFIED
Reached Conditions:  16
Short Circuited Conditions:  0
Total Conditions:  16

Condition Properties - SATISFIED:  13
Condition Properties - UNSATISFIED:  3

Condition Coverage: 81.25%

VERIFICATION FAILED