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 the following extra ones:

• lwt
• fpath (0.7.3)
• ezgzip (0.2.3)
• cohttp-lwt-unix (5.0.0)

$ opam install lwt fpath ezgzip cohttp-lwt-unix

Then:

$ make web

This installs all the available web instances as webcerb.* and the web server cerberus-webserver.

To build the UI, install node package manager npm (sudo apt install nodejs npm ) and:

$ make ui

Edit the generated config.json.

Run:

$ cerberus-server --help

Building the abstract interpreter

Install the common dependencies and the APRON library (tested with v0.9.12).

$ opam install apron

Then:

$ make absint

All targets

You can also compile all the targets with:

$ make all

Building CN

See https://github.com/rems-project/cerberus/blob/master/backend/cn/README.md

Docker image

A pre-build docker image with cerberus and cn can be downloaded with:

• For the Ubuntu 22.04 based image (recommended):

  $ docker pull ghcr.io/rems-project/cerberus/cn:release

• For Redhat Ubi9 based image:

  $ docker pull ghcr.io/rems-project/cerberus/cn:release-redhat

For a local build, run:

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

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

$ docker run --volume `PWD`:/data/ cerberus:0.1 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.