An Efficient SMT-based Bounded Model Checker.
Documentation
News
Publications
SV-COMP
Test-Comp
People
Applications
Download Archive
Third Party Contributions
Index of /benchmarks
Acknowledgments
A demonstration is available here.
A set of slides about the detection of software vulnerabilities using ESBMC: Part I, Part II, and Part III.
This software security course describes further implementation details about ESBMC.
To install ESBMC on your machine, you should download the latest binary for Linux and Windows OSs from GitHub and save and unzip it on your disk.
Once the user unzips the release, they should read the license before running ESBMC. The ESBMC distribution is split into two directories:
bin: contains a static-binary file of ESBMC;license: contains the ESBMC, Z3 and Boolector licenses.If the user wants to use other SMT solvers (e.g., MathSAT, Yices, CVC4), we recommend checking out the ESBMC source code, which is hosted on GitHub, and then follow the instructions in the BUILDING file.
ESBMC aims to support all of C11, and detects errors in software by simulating a finite prefix of the program execution with all possible inputs. Classes of problems that can be detected include:
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:
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:
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:
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
As an illustrative example to show some of the ESBMC features concerning floating-point numbers, consider the following C code:
#include <assert.h>
#include <math.h>
unsigned char nondet_uchar();
double nondet_double();
int main() {
unsigned char N = nondet_char();
double x = nondet_double();
if(x <= 0 || isnan(x))
return 0;
unsigned short i = 0;
__VERIFIER_assume(x < 5);
double x_0 = x; // Store initial value
__VERIFIER_assume(N >= 0 && N < 2);
// Loop invariant: 0 ≤ i ≤ N and x = x_0 * 2^i and x > 0
while(i < N) {
__VERIFIER_assume(x > 0);
__VERIFIER_assume(x == x_0 * pow(2, i));
__VERIFIER_assume(0 <= i && i <= N);
x = (2 * x);
++i;
}
assert(x > 0);
return 0;
}
Here, ESBMC is invoked as follows:
$esbmc file.c --floatbv --k-induction
where file.c is the C program to be checked, --floatbv indicates that ESBMC will use floating-point arithmetic to represent the program's float and double variables, and --k-induction selects the k-induction proof rule. The user can select the SMT solver, property, and verification strategy. For this particular C program, ESBMC provides the following output as the verification result:
*** Checking inductive step Starting Bounded Model Checking Unwinding loop 2 iteration 1 file ex5.c line 8 function main Not unwinding loop 2 iteration 2 file ex5.c line 8 function main Symex completed in: 0.001s (40 assignments) Slicing time: 0.000s (removed 16 assignments) Generated 2 VCC(s), 2 remaining after simplification (24 assignments) No solver specified; defaulting to Boolector Encoding remaining VCC(s) using bit-vector/floating-point arithmetic Encoding to solver time: 0.005s Solving with solver Boolector 3.2.0 Encoding to solver time: 0.005s Runtime decision procedure: 0.427s BMC program time: 0.435s VERIFICATION SUCCESSFUL Solution found by the inductive step (k = 2)
As an illustrative example to show some of the ESBMC features concerning pointer safety, consider the following C code:
#include <stdlib.h>
int *a, *b;
int n;
#define BLOCK_SIZE 128
void foo () {
int i;
for (i = 0; i < n; i++)
a[i] = -1;
for (i = 0; i < BLOCK_SIZE - 1; i++)
b[i] = -1;
}
int main () {
n = BLOCK_SIZE;
a = malloc (n * sizeof(*a));
b = malloc (n * sizeof(*b));
*b++ = 0;
foo ();
if (b[-1])
{ free(a); free(b); }
else
{ free(a); free(b); }
return 0;
}
Here, ESBMC is invoked as follows:
$esbmc file.c --memory-leak-check
where file.c is the C program to be checked and --memory-leak-check indicates that ESBMC will check for memory leaks. For this particular C program, ESBMC produces the following counterexample:
Counterexample: State 1 file ex2.c line 14 function main thread 0 ---------------------------------------------------- a = (signed int *)(&dynamic_1_array[0]) State 2 file ex2.c line 15 function main thread 0 ---------------------------------------------------- b = (signed int *)0 State 3 file ex2.c line 16 function main thread 0 ---------------------------------------------------- b = 0 + 1 State 6 file ex2.c line 16 function main thread 0 ---------------------------------------------------- Violated property: file ex2.c line 16 function main dereference failure: NULL pointer
In the counterexample shown above, State 1 indicates that memory has been allocated, which is identified by 'dynamic_1_array'. State 2 indicates that the call to the malloc function did not succeed, and thus returned NULL, i.e., the memory was not allocated. Note that ESBMC allows the user not to check for malloc/new failure via --force-malloc-success. State 3 represents an assignment to pointer b. Lastly, State 6 reports a failure to dereference pointer b.
As an illustrative example to show some of the ESBMC features concerning concurrency, consider the following C code:
#include <assert.h>
#include <pthread.h>
int n=0; //shared variable
pthread_mutex_t mutex;
void* P(void* arg) {
int tmp, i=1;
while (i<=10) {
pthread_mutex_lock(&mutex);
tmp = n;
n = tmp + 1;
pthread_mutex_unlock(&mutex);
i++;
}
return NULL;
}
int main (void) {
pthread_t id1, id2;
pthread_mutex_init(&mutex, NULL);
pthread_create(&id1, NULL, P, NULL);
pthread_create(&id2, NULL, P, NULL);
pthread_join(id1, NULL);
pthread_join(id2, NULL);
assert(n == 20);
}
Here, we create two threads id1 and id1; both threads will run the same code as implemented in P. Note that these two threads communicate via the shared memory n, which is protected by a mutex via pthread_mutex_lock and pthread_mutex_unlock. Note further that the thread main contains two joining points via pthread_join for id1 and id2.
ESBMC can be invoked as follows:
$esbmc file.c --context-bound 2
where file.c is the C program to be checked and --context-bound nr limits number of context switches for each thread. For this particular C program, ESBMC produces the following verification result:
*** Thread interleavings 612 *** Unwinding loop 1 iteration 10 file test3.c line 6 function P Unwinding loop 1 iteration 1 file test3.c line 6 function P Unwinding loop 1 iteration 2 file test3.c line 6 function P Unwinding loop 1 iteration 3 file test3.c line 6 function P Unwinding loop 1 iteration 4 file test3.c line 6 function P Unwinding loop 1 iteration 5 file test3.c line 6 function P Unwinding loop 1 iteration 6 file test3.c line 6 function P Unwinding loop 1 iteration 7 file test3.c line 6 function P Unwinding loop 1 iteration 8 file test3.c line 6 function P Unwinding loop 1 iteration 9 file test3.c line 6 function P Unwinding loop 1 iteration 10 file test3.c line 6 function P Symex completed in: 0.031s (431 assignments) Slicing time: 0.001s (removed 183 assignments) Generated 149 VCC(s), 7 remaining after simplification (248 assignments) No solver specified; defaulting to Boolector Encoding remaining VCC(s) using bit-vector/floating-point arithmetic Encoding to solver time: 0.004s Solving with solver Boolector 3.2.0 Encoding to solver time: 0.004s Runtime decision procedure: 0.001s BMC program time: 0.040s VERIFICATION SUCCESSFUL
When ESBMC refutes a property, it produces a counterexample that can be used to debug the program to find the root cause of the problem. For this purpose, ESBMC can produce the counterexample in graphml format to make its evaluation easier (e.g., by building a tool that allows graphical visualization).
As an illustrative example, consider the following fragment of C code, where we declare two bit-vectors of size 10 each: x and y, and then check whether x == y.
#include <assert.h>
int main() {
_ExtInt(10) x = nondet_float();
_ExtInt(10) y = nondet_int();
assert(x == y);
return 0;
}
If we call ESBMC as esbmc main.c --witness-output main.graphml, where main.c is the C program we want to verify while main.graphml stores the counterexample in graphml format, then ESBMC will produce the following output:
$esbmc main.c --witness-output main.graphml
<xmp>
<?xml version="1.0" encoding="utf-8"?>
<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
<key id="frontier" attr.name="isFrontierNode" attr.type="boolean" for="node">
<default>false</default>
</key>
<key id="violation" attr.name="isViolationNode" attr.type="boolean" for="node">
<default>false</default>
</key>
<key id="entry" attr.name="isEntryNode" attr.type="boolean" for="node">
<default>false</default>
</key>
<key id="sink" attr.name="isSinkNode" attr.type="boolean" for="node">
<default>false</default>
</key>
<key id="cyclehead" attr.name="cyclehead" attr.type="boolean" for="node">
<default>false</default>
</key>
<key id="sourcecodelang" attr.name="sourcecodeLanguage" attr.type="string" for="graph"/>
<key id="programfile" attr.name="programfile" attr.type="string" for="graph"/>
<key id="programhash" attr.name="programhash" attr.type="string" for="graph"/>
<key id="creationtime" attr.name="creationtime" attr.type="string" for="graph"/>
<key id="specification" attr.name="specification" attr.type="string" for="graph"/>
<key id="architecture" attr.name="architecture" attr.type="string" for="graph"/>
<key id="producer" attr.name="producer" attr.type="string" for="graph"/>
<key id="sourcecode" attr.name="sourcecode" attr.type="string" for="edge"/>
<key id="startline" attr.name="startline" attr.type="int" for="edge"/>
<key id="startoffset" attr.name="startoffset" attr.type="int" for="edge"/>
<key id="control" attr.name="control" attr.type="string" for="edge"/>
<key id="invariant" attr.name="invariant" attr.type="string" for="node"/>
<key id="invariant.scope" attr.name="invariant.scope" attr.type="string" for="node"/>
<key id="assumption" attr.name="assumption" attr.type="string" for="edge"/>
<key id="assumption.scope" attr.name="assumption" attr.type="string" for="edge"/>
<key id="assumption.resultfunction" attr.name="assumption.resultfunction" attr.type="string" for="edge"/>
<key id="enterFunction" attr.name="enterFunction" attr.type="string" for="edge"/>
<key id="returnFromFunction" attr.name="returnFromFunction" attr.type="string" for="edge"/>
<key id="endline" attr.name="endline" attr.type="int" for="edge"/>
<key id="endoffset" attr.name="endoffset" attr.type="int" for="edge"/>
<key id="threadId" attr.name="threadId" attr.type="string" for="edge"/>
<key id="createThread" attr.name="createThread" attr.type="string" for="edge"/>
<key id="witness-type" attr.name="witness-type" attr.type="string" for="graph"/>
<graph edgedefault="directed">
<data key="producer">ESBMC 6.7.0</data>
<data key="sourcecodelang">C</data>
<data key="architecture">64bit</data>
<data key="programfile">main.c</data>
<data key="programhash">7ba149c407ef7ae9e971bbc937b37a624575d6a5</data>
<data key="specification">CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )</data>
<data key="creationtime">2021-06-07T13:37:38</data>
<data key="witness-type">violation_witness</data>
<node id="N0">
<data key="entry">true</data>
</node>
<node id="N1"/>
<edge id="E0" source="N0" target="N1">
<data key="enterFunction">main</data>
<data key="createThread">0</data>
</edge>
<node id="N2"/>
<edge id="E1" source="N1" target="N2">
<data key="startline">4</data>
<data key="assumption">x = -512;</data>
<data key="threadId">0</data>
</edge>
<node id="N3"/>
<edge id="E2" source="N2" target="N3">
<data key="startline">5</data>
<data key="assumption">y = -166;</data>
<data key="threadId">0</data>
</edge>
<node id="N4">
<data key="violation">true</data>
</node>
<edge id="E3" source="N3" target="N4">
<data key="startline">93</data>
<data key="threadId">0</data>
</edge>
</graph>
</graphml>
</xmp>
We recommend reading Exchange Format for Violation Witnesses and Correctness Witnesses to obtain further information about violation and correctness witnesses in graphml format.
In ESBMC, all loops are "unwound", i.e., replaced by several guarded copies of the loop body; the same happens for backward "gotos" and recursive functions. Soundness requires that ESBMC insert a so-called unwinding assertion at the end of the loop. As an example, consider the simple C code fragment illustrated below:
1 unsigned int x=∗; 2 while ( x>0) x−−; 3 assert ( x==0);
Note that the loop in line 2 runs an unknown number of times, depending on the initial non-deterministic value assigned to x in line 1. The assertion in line 3 holds independent of x's initial value. BMC tools typically fail to verify programs that contain such loops. In particular, BMC tools introduce an unwinding assertion at the end of the loop, as illustrated in line 5 of this C code fragment.
1 unsigned int x=∗; 2 if(x>0) 3 x−−; // k copies 4 ... 5 assert (!(x>0)); 6 assert(x==0);
This unwinding assertion in line 5 causes the BMC tool to fail if k is too small as follows:
1 #include <assert.h>
2 unsigned int nondet_uint();
3 int main() {
4 unsigned int x=nondet_uint();
5 while(x>0) x--;
6 assert(x==0);
7 return 0;
8 }
$esbmc file.c --unwind 3
Counterexample: State 1 file file.c line 4 function main thread 0 ---------------------------------------------------- x = 3170305 (00000000 00110000 01100000 00000001) State 2 file file.c line 5 function main thread 0 ---------------------------------------------------- x = 3170304 (00000000 00110000 01100000 00000000) State 3 file file.c line 5 function main thread 0 ---------------------------------------------------- x = 3170303 (00000000 00110000 01011111 11111111) State 4 file file.c line 5 function main thread 0 ---------------------------------------------------- Violated property: file file.c line 5 function main unwinding assertion loop
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:
1 int main() {
2 int x=nondet_int(),y=nondet_int(),z=nondet_int();
3 __ESBMC_assume(x > 0 && y > 0 && z > 0);
4 __ESBMC_assume(x < 16384 && y < 16384 && z < 16384);
5 assert(x*x + y*y != z*z);
6 return 0;
7 }
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
ESBMC now supports universal (forall) and existential (exists) quantifiers in SMT-based verification.
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.extern void __ESBMC_assume(_Bool);
extern _Bool __ESBMC_forall(void *, _Bool);
extern _Bool __ESBMC_exists(void *, _Bool);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");
}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
forall statements) are not yet supported.$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.
$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.
$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:
\begin{equation} \begin{array}{rcrrl} & \neg & B(k) & \rightarrow & \text{program contains bug} \\ B(k) & \wedge & F(k) & \rightarrow & \text{program is correct} \\ B(k) & \wedge & I(k) & \rightarrow & \text{program is correct} \end{array} \end{equation}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 and 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.
We can also use two additional options together with the k-induction proof rule to produce (inductive) invariants:
[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
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 }
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.
$esbmc --help
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 main.py --incremental-bmc 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:
$ esbmc <python-file> --function <function-name>This command instructs ESBMC to focus only on the specified function, making the verification process more efficient when you are only interested in a particular part of the code.
ESBMC has a frontend to process Solidity source code and hence can verify simple Solidity smart contracts. In order to verify Solidity smart contract, ESBMC should be built with the option '-DENABLE_SOLIDITY_FRONTEND=On'.
There are three relevant options, which are:
As an illustrative example, consider the following Solidity code:
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 }
As declared in line 7, a is an static array of the size 2. The loop in line 10 will try to write 10 in a[2] in the third iteration, which is out-of-bound access. This error can be detected by ESBMC using the command lines as follows:
$esbmc --sol example.sol example.solast --contract MyContract --function func_array_loop --incremental-bmc
where MyContract.solast is the JSON AST of the Solidity source code generated using the command line below:
$solc --ast-compact-json example.sol > example.solast
Since there is no ambiguous function name, the --contract option can be omitted. Note that the solidity compiler version should be greater or equal than 0.4.26. For this example, ESBMC produces the following counterexample:
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)
Like other state-of-art verifiers, ESBMC can also verify state properties. A common type of properties in smart contracts are properties that involve the state of the contract. Multiple transactions might be needed to make an assertion fail for such a property. Consider a a 2D grid:
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 prove that the assertion(Invariant) could be violated throughout the funtion calls, via command:
$esbmc --sol example.sol example.solast --contract Robot --k-induction
The counterexample shows the path that leads to the assertion failure:
[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
We provide a technical report about the verification of Solidity programs here.
We also provide a Github action for security verification of solidity contracts using ESBMC-solidity here.
$esbmc file.c --multi-property
ESBMC can verify the satisfiability of all the claims of a given bound. During this multi-property verification, ESBMC does not terminate when a counterexample is found; instead, it continues to run until all bugs have been discovered. There are three relevant options, which are:
An example of multi-property verification can be found in the Code Coverage Metric section below.
ESBMC provides a set of coverage metrics to help you measure how much of the state space you've visited. The supported coverage metrics can be listed as follows:
As an illustrative example, consider the following C code:
1 int main()
2 {
3 int x = 0;
4 while (nondet_int())
5 {
6 if (!x)
7 {
8 assert(x == 0);
9 x = 1;
11 }
12 else if (x == 1)
13 {
14 assert(x > 0);
15 x = 2;
16 }
17 else if (x == 2)
18 {
19 assert(x >= 2);
20 x = 3;
21 }
22 }
23 assert(x == 3);
24 }
For assertion coverage, ESBMC is invoked as follows:
$esbmc example.c --k-induction --assertion-coverage
For this particular C program, ESBMC produces the following counterexample and coverage information, reflecting that two branches in the program leave unexplored during verification:
[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)
For condition coverage, ESBMC is invoked as follows:
$esbmc example.c --k-induction --condition-coverage-claims
The output coverage result can be illustrated as follows:
[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
Note that the --condition-coverage-claims option provides verbose output of claim information, including its condition and location. If only the coverage number is needed, we recommend using the --condition-coverage option instead.
ESBMC integrates a number of SMT solvers directly via their respective API, but on Unix can also be instructed to communicate with an external SMT solver process by a pipe. The following table lists ESBMC's options enabling the use of the particular solver.
| Backend | Option |
| Boolector | --boolector (this is the default) |
| Z3 | --z3 |
| MathSAT | --mathsat |
| CVC4 | --cvc |
| Yices | --yices |
| Bitwuzla | --bitwuzla |
| SMTLIB | --smtlib --smtlib-solver-prog CMD
(see below for details about the placeholder CMD) |
While Boolector is the default, an alternative default solver can also
be specified with the --default-solver SOLVER option, where
SOLVER corresponds to one of the above options without the
--. This option is particular suited for a shell alias or the
ESBMC_OPTS environment variable, which is parsed every time
ESBMC runs.
The CMD parameter for the SMTLIB backend is a string that is
interpreted by the shell, therefore it can contain additional options
to a particular command separated by whitespace, or even chain together
multiple commands. Here are some examples for CMD that work with ESBMC.
Note that the tools in these commands are assumed to be available
through the PATH environment variable:
boolector --incrementalz3 -intee formula.smt2 | z3 -in | tee output.txtyices-smt2 --incrementalcvc5 -L smt2 -mRemember to quote the CMD string when executing ESBMC.
We are still increasing the robustness of ESBMC and also continuously implementing new features, more optimizations and experiencing new encodings. For any question about ESBMC, please contact us via https://github.com/esbmc/esbmc.