/esbmc

The efficient SMT-based bounded model checker

Primary LanguageCOtherNOASSERTION

The ESBMC model checker

Codacy Badge Lint Code Base Health Checks Build All Solvers codecov

ESBMC (the Efficient SMT-based Bounded Model Checker) is a mature, permissively licensed open-source context-bounded model checker for verifying single- and multithreaded C/C++ programs. It can verify both predefined safety properties (e.g., bounds check, pointer safety, overflow) and user-defined program assertions automatically. ESBMC supports the Clang compiler as its C/C++ frontend, IEEE floating-point arithmetic for various SMT solvers, implements the Solidity grammar production rules as its Solidity frontend and state-of-the-art incremental BMC and k-induction algorithms.

To build ESBMC, please see the BUILDING file. For getting started, we recommend first reading some of the background material / publications, to understand exactly what this technique can provide, for example our SV-COMP papers, which are available online.

We also provide a short video that explains ESBMC:

https://www.youtube.com/watch?v=uJ5Jn0sxm08&t=2182s

This video was delivered as part of a technical talk on exploiting the SAT revolution for automated software verification in a workshop between Arm Research and the University of Manchester.

We offer a post-graduate course in software security that explains the internals of ESBMC.

https://ssvlab.github.io/lucasccordeiro/courses/2020/01/software-security/index.html

This course unit introduces students to basic and advanced approaches to formally build verified trustworthy software systems, where trustworthy comprise five attributes: reliability, availability, safety, resilience and security.

The cannonical public location of ESBMCs source is on github:

https://github.com/esbmc/esbmc

While our main website is esbmc.org

Publications

Features

ESBMC aims to support all of C99/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:

  • 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
  • Divide by zero
  • Memory leaks

Concurrent software (using the pthread api) is verified by explicit exploration of 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

By default ESBMC performs a "lazy" depth first search of interleavings -- it can also encode (explicitly) all interleavings into a single SMT formula.

A number of SMT solvers are currently supported:

  • Z3 4.8+
  • Bitwuzla
  • Boolector 3.0+
  • MathSAT
  • CVC4
  • Yices 2.2+

In addition, ESBMC can be configured to use the SMTLIB interactive text format with a pipe, to communicate with an arbitary solver process, although not-insignificant overheads are involved.

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

Differences from CBMC

ESBMC is a fork of CBMC v2.9 (2008), the C Bounded Model Checker. The primary differences between the two are:

  • CBMC focuses on SAT-based encodings of unrolled programs while ESBMC targets SMT-based encodings.
  • CBMC's concurrency support is an entirely symbolic encoding of a concurrent program in one SAT formulae, while ESBMC explores each interleaving individually.
  • CBMC uses a modified C parser written by James Roskind and a C++ parser based on OpenC++, while ESBMC relies on the Clang front-end.
  • ESBMC implements the Solidity grammar production rules as its Solidity frontend, while CBMC does not implement a Solidity frontend.
  • CBMC implements k-induction, requiring three different calls: to generate the CFG, to annotate the program, and to verify it, whereas ESBMC handles the whole process in a single call. Additionally, CBMC does not have a forward condition to check if all states were reached and relies on a limited loop unwinding.
  • ESBMC adds some additional types to the program's internal representation.

Open source

ESBMC has now been released as open source software -- mainly distributed under the terms of the Apache License 2.0. ESBMC contains a signficant amount of other peoples software, however, please see the COPYING file for an explanation of who-owns-what, and under what terms they are distributed.

We'd be extremely happy to receive contributions to make ESBMC better (under the terms of the Apache License 2.0). If you'd like to submit anything, please file a pull request against the public github repo. General discussion and release announcements will be made via GitHub. To contact us about research or collaboration, please post an issue in GitHub.

Getting started

Currently, we don't have a good guide for getting started with ESBMC, although we hope to improve this in the future. Examining some of the benchmarks in the SV-COMP competition (http://sv-comp.sosy-lab.org/) would be a good start, using the esbmc command line for the relevant competition year.

Contributing to the code base

Here are some steps to contributing to the code base:

  1. Compile and execute esbmc. Building
  2. Fork the repository
  3. Clone the repository git clone git@github.com:YOURNAME/esbmc.git
  4. Create a branch from the master branch (default branch)
  5. Make your changes
  6. Check the formatting with clang-format (use Clang 9)
  7. Push your changes to your branch
  8. Create a Pull Request targeting the master branch

Here is an example to prepare a pull request (PR)

A) Make sure that you are in the master branch and your fork is updated.

git checkout master
git fetch upstream
git pull --rebase upstream master
git push origin HEAD:master

Note that if you have not yet setup the upstream, you need to type the following command:

git remote add upstream https://github.com/esbmc/esbmc

B) Create a local branch (e.g., model-pthread-create) from the master branch:

git checkout -b model-pthread-equal --track master

C) Add your changes via commits to the local branch:

git add path-to-file/file.cpp
git commit -sm "added opertational model for pthread_equal"

Note that you can check your changes via git status. Note also that every PR should contain at least two test cases to check your implementation: one successful and one failed test case.

D) Push your changes in the local branch to the ESBMC repository:

git push origin model-pthread-equal

New contributors can check issues marked with good first issue by clicking here.

Documentation

A limited number of classes have been marked up with doxygen documentation headers. Comments are put in the header files declaring classes and methods. HTML documation can be generated by running:

doxygen .doxygen

Output will be in docs/html, open index.html to get started.

Acknowledgments

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 Intel, Motorola, Nokia Institute of Technology and Samsung. ESBMC is currently funded by Intel, EPSRC grants EP/T026995/1, EP/V000497/1, EU H2020 ELEGANT 957286 and Soteria project awarded by the UK Research and Innovation for the Digital Security by Design (DSbD) Programme.