README-cheri.md

Building and running instructions for Cerberus-CHERI

Docker

Execute test.c using CHERI C semantics:

docker run -v $HOME/tmp:/mnt -it vzaliva/cerberus-cheri cerberus-cheri --exec /mnt/test.c

Execute test.c using ISO C semantics:

docker run -v $HOME/tmp:/mnt -it vzaliva/cerberus-cheri cerberus --exec /mnt/test.c

Print Core elaboration for test.c using CHERI C semantics:

docker run -v $HOME/tmp:/mnt -it vzaliva/cerberus-cheri cerberus-cheri --pp=core --exec /mnt/test.c

Print Core elaboration for test.c using ISO C semantics:

docker run -v $HOME/tmp:/mnt -it vzaliva/cerberus-cheri cerberus --pp=core --exec /mnt/test.c

Local install

To build Cerberus, you need opam (>= 2.0.0, see here to install) and OCaml (>= 4.12.0). Current developement is using Coq 8.16.1.

First set up additional repositories for Coq and Iris packages:

opam repo add --this-switch coq-released https://coq.inria.fr/opam/released
opam pin -ny coq-struct-tact https://github.com/uwplse/StructTact.git
opam repo add --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam pin -ny coq-sail-stdpp https://github.com/rems-project/coq-sail.git
opam pin -ny coq-cheri-capabilities https://github.com/rems-project/coq-cheri-capabilities.git

Install the remaining dependencies using opam:

opam pin add -ny cerberus-lib .
opam pin add -ny cerberus-cheri .
opam install --deps-only ./cerberus-cheri.opam

Then to build Cerberus-CHERI:

make cerberus-with-cheri

To install Cerberus-CHERI:

opam install cerberus-cheri