CVM

The Copland Virtual Machine (CVM) is a Rocq library that formalizes a virtual machine for the Copland Domain Specific Language for layered remote attestation.

NOTE: The CVM expects to communicate with ASP's via a fork/exec style where the ASP is launched, reads input from stdin, and writes output to stdout. Utilizing the rust-am-lib version 0.3.0 and greater should be sufficient to meet these requirements. The CVM does not currently support any other style of communication with ASP's, but support for additional styles may be added in the future.

Meta

• Author(s):
  • Will Thomas
• License: Creative Commons Attribution Share Alike 4.0 International
• Compatible Rocq/Coq versions: 9.0.1
• Compatible OCaml versions: 4.12 or later
• Additional dependencies:
  • RocqCandy
  • Copland Spec
  • CoplandManifestTools
  • EasyBakeCakeML
  • Bake
  • RocqLogging
  • conf-zmq
  • Dune 3.17 or later
• Related publication(s): none

Building and installation instructions

The easiest way to install the latest released version of CVM is via OPAM:

opam repo add -a --set-default ku-sldg/opam-repo https://github.com/ku-sldg/opam-repo.git
opam repo add coq-released https://coq.inria.fr/opam/released
opam install rocq-cvm

To instead build and install manually, do:

git clone https://github.com/ku-sldg/cvm.git
cd cvm
dune build
dune install