Skip to content

ESBMC

Jump to bottom Edit New page
Yiannis Charalambous edited this page Sep 18, 2024 · 1 revision

ESBMC (the Efficient SMT-based Context-Bounded Model Checker) is a mature, permissively licensed open-source context-bounded model checker for verifying single and multithreaded C/C++, CUDA, CHERI, Kotlin, Python, and Solidity programs. It can automatically verify predefined safety properties (e.g., bounds check, pointer safety, overflow) and user-defined program assertions.

What inputs are supported?

ESBMC supports source code files from various programming languages.

For which programming languages has it support?

  • C/C++
  • CUDA
  • CHERI
  • Java/Kotlin
  • Python
  • Solidity programs

What properties can be verified?

ESBMC can automatically analyze source code and verify the following properties:

  • 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
  • Undefined behavior on shift operations
  • Floating-point for NaN
  • Divide by zero
  • Memory leaks

Concurrent software (using the pthread API) is verified by explicitly exploring interleavings, 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 concurrent programs for:

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

What are the tool’s main techniques for the supported (input, property) pairs?

ESBMC implements state-of-the-art incremental BMC and k-induction proof-rule algorithms based on Satisfiability Modulo Theories (SMT) and Constraint Programming (CP) solvers for all of its supported languages.

What external tools are used? (e.g., compilers, SMT solvers)

Many SMT solvers are currently supported:

  • Z3 4.8+
  • Bitwuzla
  • Boolector 3.0+
  • MathSAT
  • CVC4
  • CVC5
  • Yices 2.2+
  • Arbitrary solvers (through SMTLIB's interactive text format and pipes)

Additional Libraries:

  • The Clang compiler as its C/C++/CHERI/CUDA frontend;
  • The Soot framework via Jimple as its Java/Kotlin frontend;
  • The ast2json package as its Python frontend;
  • Implements the Solidity grammar production rules as its Solidity frontend;

What is the tool’s URL?

Example(s)

To verify the following program:

#include <math.h>
int main() {
  unsigned int N = nondet_uint();
  double x = nondet_double();
  if(x <= 0 || isnan(x))
    return 0;
  unsigned int i = 0;
  while(i < N) {
    x = (2*x);
    assert(x>0);
    ++i;
  }
  assert(x>0);
  return 0;
}

Invoke ESBMC with the following command:

esbmc file.c --k-induction

Where file.c is the source code program to be verified and --k-induction is a flag to use K-Induction proof for the verification.

Other relevant information

Acknowledgements:

ESBMC is a joint project of the Federal University of Amazonas (Brazil), the University of Manchester (UK), the University of Southampton (UK), and the University of Stellenbosch (South Africa).

The ESBMC development was supported by various research funding agencies, including CNPq (Brazil), CAPES (Brazil), FAPEAM (Brazil), EPSRC (UK), Royal Society (UK), British Council (UK), European Commission (Horizon 2020), and companies including ARM, Intel, Motorola Mobility, Nokia Institute of Technology and Samsung. The ESBMC development is currently funded by ARM, EPSRC grants EP/T026995/1 and EP/V000497/1, Ethereum Foundation, EU H2020 ELEGANT 957286, Intel, Motorola Mobility (through Agreement N° 4/2021), and Soteria project awarded by the UK Research and Innovation for the Digital Security by Design (DSbD) Programme.

References

Add a custom footer

list of tools

list of challenges

Clone this wiki locally