Home

Awesome

Introduction

Crucible is a language-agnostic library for performing forward symbolic execution of imperative programs. It provides a collection of data-structures and APIs for expressing programs as control-flow graphs. Programs expressed as CFGs in this way can be automatically explored by the symbolic execution engine. In addition, new data types and operations can be added to the symbolic simulator by implementing fresh primitives directly in Haskell. Crucible relies on an underlying library called What4 that provides formula representations, and connections to a variety of SAT and SMT solvers that can be used to perform verification and find counterexamples to logical conditions computed from program simulation.

Crucible has been designed as a set of Haskell packages organized so that Crucible itself has a minimal number of external dependencies, and functionality independent of crucible can be separated into sub-libraries.

Currently, the repository consists of the following Haskell packages:

In addition, there are the following library/executable packages:

Finally, the following packages are intended primarily for use by Crucible developers:

The development of major features and additions to crucible is done in separate branches of the repository, all of which are based off master and merge back into it when completed. Minor features and bug fixes are done in the master branch. Naming of feature branches is free-form.

Each library is BSD-licensed (see the LICENSE file in a project directory for details).

Quick start

Clone this repository and checkout the immediate submodules to supply the needed dependencies (git submodule update --init).

Crucible can be built with the cabal tool:

cabal update
cabal new-configure
cabal new-build all

Alternately, you can target a more specific sub-package instead of all.

Testing and Coverage

Testing is done via cabal test.

To run the tests for crux-mir, you need to have built and installed the mir-json tool such that it can be found on your $PATH. You also need translated Rust libraries for the machine you're testing on. See the crux-mir README for further information.

Testing with coverage tracking is done via cabal test --enable-coverage ... or cabal configure --enable-coverage, although additional workarounds will be needed as noted in https://github.com/galoisinc/crucible/issues/884 and https://github.com/haskell/cabal/issues/6440.

Notes on Freeze Files

We use the cabal.GHC-*.config files to constrain dependency versions in CI. We recommand using the following command for best results before building locally:

ln -s cabal.GHC-<VER>.config cabal.project.freeze

These configuration files were generated using cabal freeze --enable-tests --enable-benchmarks. Note that at present, these configuration files assume a Unix-like operating system, as we do not currently test Windows on CI. If you would like to use these configuration files on Windows, you will need to make some manual changes to remove certain packages and flags:

regex-posix
tasty +unix
unix
unix-compat

Acknowledgements

Crucible is partly based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Contract No. N66001-18-C-4011. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Defense Advanced Research Projects Agency (DARPA).