Overview

This development contains the SECOMP formally secure compiler for compartmentalized C programs and its machine-checked security proofs in Coq. Both of these are based on the CompCert formally verified C compiler. The Coq development contains the proofs, theorems, and testing described in the accompanying paper below.

This README file contains detailed instructions on how to build, run, and check the development. These can be done on most modern hardware, and depend only on OCaml, Coq, and some libraries that are available via the OCaml package manager OPAM. Additionally, some tests rely on the GCC RISC-V cross-compiler.

The permanently archived artifact associated with the paper below contains not only the sources but also a virtual machine (VM) that has all these dependencies already installed. The sudo password of the VM is secomp. Instead of branches, the artifact is split into sub-folders that can be compiled and checked independently from the others.

Accompanying paper

• Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, Cătălin Hrițcu, and Andrew Tolmach. SECOMP: Formally Secure Compilation of Compartmentalized C Programs. In 25th ACM Conference on Computer and Communications Security (CCS). October 2024. Extended version available as arXiv:2401.16277.

Requirements

This development is built and tested with Coq 8.15.2. It is based on CompCert 3.12 and its 64-bit RISC-V backend.

General requirements:

• OCaml version 4.5.0 or greater (OCaml 5 is not supported).
  • systematic testing needs OCaml version 4.14.0 or later (see below)
• Coq version 8.15.2 (OPAM package: coq)
• Menhir version 20190626 or greater (OPAM package: menhir).

Extended requirements for systematic testing:

• OCaml version 4.14.0 or later.
• QCheck (OPAM package: qcheck).
• MenhirLib (OPAM package: menhirLib).

Here are the OPAM commands one can use to install all OCaml dependencies above:

$ opam switch create 4.14.2
$ eval $(opam env --switch=4.14.2)
$ opam install coq.8.15.2 menhir qcheck menhirLib

In addition to the above, some of the toolchain relies on the riscv64 architecture version of the GCC compiler, available for example from the gcc-riscv64-linux-gnu package on Debian-based systems.

System requirements can be verified through CompCert's configure script (see Building below).

Structure

The development is currently split into 3 branches:

• ccs-main: compiler correctness proof, recomposition proof, and testing infrastructure
• ccs-backtranslation: proof of back-translation
• ccs-blame: proof of blame

Building

Each branch can be built after installing its dependencies by first configuring the CompCert build process, by running:

$ ./configure -toolprefix "riscv64-linux-gnu-" rv64-linux

where riscv64-linux–gnu- stands for the prefix used by the local GCC RISC-V compilation chain.

One can then compile CompCert and check the proofs on that branch by running make, optionally with the -j command line option, where an optional argument number N can limit the number of parallel jobs:

$ make -jN

After building once, or after running make depend, the alternative command make proof can be used to only check the proofs.

Installing the GCC RISC-V compiler is not strictly necessary to build CompCert and run make proof, for which the simpler ./configure rv64-linux command is enough. But this will result in errors if running make as CompCert won't be able to compile its runtime, resulting in errors resembling:

error: unsupported argument 'rv64imafd' to option '-march='

Installing and using the GCC RISC-V compiler is necessary in order to compile the tests and examples in the ccs-main branch (see Examples below).

How one can inspect the Coq theorems and proofs

The file table.html contains a mapping from claims in the paper to definitions and proofs.

For those using the provided virtual machine, we recommend using the built-in CoqIDE environment to explore the Coq development. Users of the virtual machine can install other editors, like Proof General, if they prefer.

To start CoqIDE, simply run the coqide command and navigate to the files you wish to inspect. The simplest way to evaluate a file is by using the buttons "Run to end" and "Run to cursor". Keyboard shortcuts for those commands can be found on the Navigation menu.

To inspect a particular theorem, locate that theorem, and process the file up to the start of the theorem. Then, you may step through the proof one step at a time using the button "Forward one step". The state of the proof (with goals and assumptions) is displayed in one of the side window. Messages are displayed in the other side window.

A proved theorem ends with Qed.. When running Qed, the interactive prover will check the validity of the proof; if the command succeeds, then the proof is accepted by Coq. After a theorem is proved, you can use the following command (write it inside the file and then "Forward one step"): Print Assumptions theorem. to display all the assumptions and axioms theorem depends on.

At any point, you can use the commands on the Query menu to Print the definition of and identifier and Check the type of an identifier, among others.

Main branch: ccs-main

The ccs-main branch contains the extension of CompCert to compartments, which involved updating the languages, passes, and correctness proofs. This extension can be built into a compiler binary that can be used to compile compartmentalized C programs that can be executed. This branch also includes the recomposition proof and the systematic testing infrastructure employed to validate the assumptions and expected behavior of the back-translation function.

The updated complier correctness proof is generally complete and can be found in file driver/Compiler.v, theorems transf_c_program_correct and separate_transf_c_program_correct, and only depends on CompCert's existing axioms, or small adaptions thereof to account for the addition of compartments to the compiler, as well as a few admits in file Stackingproof.v, which still has to be fully adapted to some recent changes.

If one wants to verify this, uncomment and execute Print Assumptions transf_c_program_correct and Print Assumptions separate_transf_c_program_correct. This will load and print the list of axiomatized results used in the proofs. This can be compared to the output of these commands for standard CompCert on branch master.

The following files include the most interesting changes:

• Compartment model: file common/AST.v, modules COMPTYPE and COMP.
• The notion of interface can be found in common/Globalenvs.v and is named Policy. The same file describes how we check for allowed calls.
• Events: file common/Events.v, inductive event. The same file contains the buffer-based IO development and the detailed models for the read and write system calls.

This branch also contains the recomposition proof, which is complete:

File common/Smallstep.v contains the definition of the three-way simulation relation (tsim_properties), and the proof that it implies preservation of finite prefixes (tsimulation_star). The same file also contains the simulation diagrams depicted in Section 6 (Section THREEWAY_SIMU_DIAGRAM).

File security/Recomposition.v contains the proof of recomposition: lemma simulation, as well as the three cores lemmas used to instantiate the diagrams: step_E0_strong, step_E0_weak, and step_t. The simulation invariants can be found at strong_equivalence, weak_equivalence, stack_rel.

Finally, the top-level secure compilation result (Theorem 8.1) is formalized in file security/RSC.v, but this is not yet integrated with the proofs of recomposition, back-translation, and blame. These steps are also generally complete, but they are not yet integrated, and the back-translation and blame proofs are still on separate branches described below.

Examples

Compartmentalized program examples can be found under test/compartments and can be run in a custom version of the CompCert source-level interpreter, which we extended to support compartments, for instance by running:

[compartments]$ ../../ccomp -interp ccs1.c

These programs can be compiled by running make in test/compartments:

[compartments]$ make

You can inspect the examples' source code by opening the C files like ccs1.c, and can test the functioning of the compiler on such individual files using:

[compartments]$ make ccs1.s

Then, you can inspect the content of the generated assembly in ccs1.s, which includes the compartment information in comments.

Alternatively, one can use the -interp-asm flag to both compile a file like ccs1.c and run it in a prototype interpreter for ASM programs with compartments:

[compartments]$ ../../ccomp -interp-asm ccs1.c

Running compartment-stripped binaries in vanilla RISC-V emulator

Running make in test/compartments also generates .compcert binaries using CompCert's standard RISC-V backend, which are stripped from the compartment information and which one should be able to run on a standard RISC-V machine.

If you wish to also run the compiled binaries, we suggest using Fabrice Bellard's TinyEmu, which is included in the virtual image.

On the virtual image, you can use the following to run compiled programs:

Start the emulator with temu root_9p-riscv64.cfg then mount -t 9p /dev/root /mnt in the guest to be able to access the content of the folder /tmp on the host.

Then, compile a file and copy it to the /tmp directory:

[compartments]$ make fib.compcert
[compartments]$ cp fib.compcert /tmp/fib.compcert

Then, on the guest, run /mnt/fib.compcert.

The make invocation above passes the -static flag to CompCert to statically link the libraries to avoid issues arising from version discrepancies between the system's libc and the emulator's libc.

Compiling compartmentalized programs with the capabilities backend

For this part, build the compiler on branch ccs-main following the general invocations of configure and make. One does not need to worry about linking, as only the compilation procedure is needed for this part.

To compile a compartmentalized program, invoke CompCert as follows, for instance for a simple compartmentalized addition example available at test/compartments/add.c, run from the test/compartments folder:

[compartments]$ ../../ccomp -c -dcapasm add.c

The compiler automatically produces an additional file, add.cap_asm, with the capability assembly code for the given program.

Note that not all instructions are fully supported by the pretty-printer at the moment, and programs with unsupported instructions will emit invalid placeholders including the special placeholder __Inst_Name__ in them.

Our prototype implementation of the capability-based backend and secure calling convention is found under cheririscV/.

Simple compilation examples (in Coq) are in file cheririscV/CapAsmgen.v, section Examples.

The compiler binary is instrumented to produce capability assembly in addition to regular compartmentalized CompCert assembly, as described above.

Back-translation

Systematic testing the compilation of the back-translation (Assumption 1)

For this part, build the compiler on branch ccs-main following the general invocations of configure and make. One does not need to worry about linking, as only the compilation procedure is needed for this part.

The property-based testing infrastructure for Assumption 1 can be found under test/backtranslation. After compiling CompCert, from this folder, run:

[backtranslation]$ touch .depend
[backtranslation]$ make clean
[backtranslation]$ make depend
[backtranslation]$ make test_backtranslation

Running the test_backtranslation binary performs the testing:

[backtranslation]$ ./test_backtranslation

In more detail, you can run the tests in two modes: test mode and reproduction mode. The test mode is the default mode and designed to run random tests. In case of any failures, all intermediate seeds are printed, otherwise a statistic of the generated values is shown. Note that the number of tests grows multiplicatively so choose the parameters accordingly. In reproduction mode the specified seeds allow you to reproduce a very specific run. The commands below exemplarily show how to run the tests in test and reproduction mode respectively.

[backtranslation]$ ./test_backtranslation -num_asm_progs 5 -num_traces 20
[backtranslation]$ ./test_backtranslation -root_seed 4 -asm_seed 3 -trace_seed 8

If one is interested in reproduction, we have run the large-scale testing experiments for the CCS'24 paper using QCheck 0.21.3.

A few more details are provided in test/backtranslation/README.md.

Back-translation proof branch: ccs-backtranslation

This branch contains the back-translation proof. Use make depend && make proof to replay the proof.

The proof is complete. This proof is done in a slightly more complex setting where system calls can belong to particular compartments. Also some recent changes to the ccs-main branch are not yet integrated.

The memory deltas are defined in the file security/MemoryDelta.v.

The informative events (called bundled_events), and the intermediate language characterizing the well-formedness of informative traces (ir_step) are defined in security/BtAsm.v. The proof going from RISC-V assembly to the intermediate language is called asm_to_ir.

The file security/Backtranslation.v contains the implementation of the back-translation function, gen_program.

The file security/BacktranslationProof.v contains the proof of correctness of the back-translation, starting from the intermediate language: ir_to_clight.

The file security/BacktranslationProof2.v contains the complete proof from assembly to Clight: backtranslation_proof.

Blame proof branch: ccs-blame

This branch contains the blame proof. Use make depend && make proof to replay the proof.

The proof is complete, but some recent changes to the ccs-main branch are not yet integrated.

The main blame theorem can be found in file security/Blame.v, theorem does_prefix_star.

Definition 6 (Blame) can be found in file security/Blame.v, theorem blame_program.

• This follows directly from does_prefix_star and uses a simple technical lemma that is to be proved after integration on the ccs-main branch.

• Theorem blame is a simple corollary that matches the one used in the top-level security proof.

Full program run lemmas: file security/Blame.v, theorems parallel_exec and parallel_exec'.

Synchronized execution lemmas: file security/Blame.v, theorems parallel_star_E0 and parallel_exec1.

Stepwise lemmas: file security/Blame.v, theorems parallel_concrete and parallel_abstract_t.