Building and running instructions for Cerberus-CHERI
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
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#f319aad
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