Cerberus C semantics

Web interfaces, papers, and web page

See https://www.cl.cam.ac.uk/~pes20/cerberus/.

Build instructions for the CLI

To build Cerberus, you need opam (>= 2.0.0, see here to install) and OCaml (>= 4.12.0).

First install the dependencies (including lem and menhir) using opam:

$ opam install --deps-only ./cerberus-lib.opam ./cerberus.opam

Then build the CLI using:

$ make

The CLI can then be used either from the source directory using:

$ dune exec cerberus -- ARG1 .. ARGN

or, after doing $ make install, using the cerberus executable.

---

To fully remove all object and Lem generated files:

$ make distclean

To remove the object files, but keep the Lem generated files (allowing for faster build when only working on .ml files):

$ make clean

Basic usage

Executing some translation units:

$ cerberus --exec file1.c ... fileN.c

This will elaborate to Core, link, look for a main() function, and start executing the Core from there. To see a printout of the return value, and to get a machine-friendly collection of stdout and stderr, add the --batch argument.

Passing command line arguments to the C program

$ cerberus --args="arg1","arg2" file.c

Printing the intermediate representations

• The C abstract syntax (Cabs) and the Ail intermediate representation can be printed with --ast=cabs and --ast=ail.

• The Ail intermediate representation and the Core program can be pretty-printed with --pp=ail and --pp=core.

Running the elaborate-and-link pipeline without executing:

$ cerberus file1.c ... fileN.c

This will elaborate the C translation units to Core programs, and link them, before returning silently.

Include directories can be added with the usual -I, and macros can be forwarded to the preprocessor using -D (and unset with -U).

---

For more, see cerberus --help

---

Various C programs can be found in tests/.

Building Cerberus-BMC

Install the common dependencies and the following extra ones:

• angstrom (0.15.0)

$ opam install angstrom

Then run:

$ make cerberus-bmc

---

To run:

$ cerberus-bmc --help

Building the web server

Install the common dependencies and some backend specific ones (see here for details):

$ opam install --deps-only ./cerberus-web.opam ./cerberus-lib.opam

Then:

$ make web

This copies all the available web instances as webcerb.* and the web server as cerberus-webserver to the source root directory.

Next, build the webapp providing the UI (this requires the node package manager npm):

$ make ui

The first command sets up a deployment directory at public/_deployment containing a default configuration config.json.

To run the server with that default configuration:

$ ./cerberus-webserver -c public/_deployment/config.json

(If you intend to move and run the server binary to another location, you will need the cerberus-lib package to first be installed in with opam)

All targets

You can also compile all the targets with:

$ make all

Docker image

For a local build, run:

$ docker build -t cerberus:release -f Dockerfile.ubuntu .

which creates a Docker image than can be used for example with:

$ docker run --volume `PWD`:/data/ cerberus:release cerberus tests/tcc/00_assignment.c --pp=core

This image contains all the source code.

People

Contributors:

• Kayvan Memarian
• Christopher Pulte
• Thomas Sewell
• Victor B. F. Gomes
• Stella Lau
• Kyndylan Nienhuis
• Dhruv Makwana
• Justus Matthiesen
• James Lingard
• David Chisnall
• Robert N. M. Watson
• Peter Sewell
• Vadim Zaliva

The main Cerberus developer is Kayvan Memarian. Victor Gomes made substantial contributions across the system. Kyndylan Nienhuis worked on the operational semantics for C11 concurrency. Stella Lau is the main developer of Cerberus BMC. The CN backend is by Christopher Pulte and Thomas Sewell. The CHERI memory model is by Vadim Zaliva. Cerberus originated with Justus Matthiesen's 2010-11 Part II project dissertation and his 2011-12 MPhil dissertation. James Lingard's 2013-14 MPhil dissertation developed a certifying translation validator for simple C programs for the Clang front-end, w.r.t. the Cerberus and Vellvm semantics.

Funding

This software was developed largely within the Rigorous Engineering of Mainstream Systems (REMS) project at the University of Cambridge. It has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 789108, ELVER); the EPSRC Programme Grant REMS: Rigorous Engineering of Mainstream Systems (EP/K008528/1); an EPSRC Leadership Fellowship EP/H005633 (Sewell); a Gates Cambridge Scholarship (Nienhuis); an MIT EECS Graduate Alumni Fellowship (Lau); and Google.