The CompCert verified compiler

Commented Coq development

Version 3.14, Chamois-Arsene fork, 2024-12-23

The Chamois-Arsene fork

This page is focused on the changes applied to Chamois-CompCert in the context of the Arsene PEPR. General documentation on Chamois-CompCert can be found here. The sources are available on our public gitlab repository.

The people responsible for this version are

Overview

The additions included in this version of CompCert are focused on defending against fault injections, that is hardware attacks that may change the behavior of the software by skipping instructions, changing the content of memory, etc... They are primarily focused on the RiscV (32bits) architecture, although the changes introduced in this version should be back-compatible with all architectures supported by mainline Chamois-CompCert. The work exclusive to this branch focuses on implementing three separate countermeasures against fault injection as program transformations. Inter and intra procedural control flow checking protect the control flow of the program at the level of conditional branching and function calls respectively. Load duplication protects data loaded from memory from mutation.

Paper cross-references

The paper Formally verified hardening of C programs against hardware fault injection (@CPP'25) by Pesin, Boulmé, Monniaux, and Potet gives a high-level overview of our work. All formalized definitions in the paper correspond to a Coq definition or proof, as referenced below.

Usage

Installation

This fork of CompCert 3.15 has been tested with Coq v8.14.1 and v8.19.1 It should work with all versions in between. Its dependencies may be installed by typing

opam install coq.8.19.1 menhir

Chamois-CompCert for RiscV (32bits) can then be compiled with the following commands:

./config_rv32.sh
make
This should generate a ccomp executable for the compiler.

Example usage

After generating the ccomp executable, the compiler can be used to compile the verify_pin example from the article by running:

./ccomp -stdlib runtime -dasm -o verify_pin.exe test/secu/verify_pin.c
This will generate a RiscV executable verify_pin.exe, as well as the corresponding assembly code in verify_pin.s. The executable may then be run, using qemu for instance:
qemu-riscv32 verify_pin.exe

Compiler options

The application of countermeasures is mainly controlled by the following compiler options:

For more details, search for the -fsecu-* options in the full list of options.

Countermeasure annotations

Although intra-procedural control-flow checking and load duplication are activated by default, they are only applied on marked function and memory loads.

Intra-procedural control-flow checking is activated for a given function by adding the harden attribute, as shown below.

__attribute__((harden("control_flow_checking")))
int main() {
  int x = 0;
  while(x < 42) x++;
  return x;
}

Load duplication is activated for a given memory load by encapsulating it with the __builtin_secu_wd_int builtin, as shown below.

int f(int *x) {
  return __builtin_secu_wd_int(x[4]) + 7;
}

Replaying Lazart experiments

This require to install the experimental (unverified) branch btl2llvm of Chamois-Arsene exporting its BTL representation to LLVM-IR backend. This version rather targets RISC-V 64, for technical reasons. Everything is explained on the dedicated btl2llvm branch of chamois-test.

New files and major changes

Our work involved adding and changing a lot of definitions in CompCert. The new files and changes to existing definitions are listed below.

RTL framework

Qualified identifiers

In order to write interprocedural transformations that introduce new functions in the program, we had to generalize the definition of global identifiers into qualified identifiers, made up of a list of identifiers; this allows to check and reason on the absence of some classes of identifiers in a program. This required adding and modifying definitions in numerous files, in particular:

Observe and opaque copies

To prevent countermeasures from being removed by later optimizations, we introduce opaque copies that should not be optimized by the compiler. Concretely, a countermeasure pass may add a call to the observe builtin, with the the registers to observe as a parameter. A subsequent pass then expand all observe into a sequence of opaque copies. These copy instructions already existed in previous versions, but we generalized their typing to facilitate proving the correctness proof of the observe expansion pass.

Currenty, only the interprocedural CFI is protected by observations. They are placed at two different points: between the two test, we observe the condition arguments to prevent constant propagation of the two conditions. After the text, we observe the value of GSR to prevent its constant propagation, which would weaken (but not invalidate) the countermeasure. See cond1.pdf, cond1.cm.pdf and cond1.opaque.pdf for an example.

Assert instruction

The new instruction (Iassert: condition -> list assert_arg -> node -> instruction) added in RTL is used to carry global information about registers/memory from the correctness proof to a robustness proof. It's arguments of type assert_arg represent either reading a register value or loading (successfully) from a memory address. The execution of an assert (see exec_Iassert) does not modify the state, but checks that the condition applied to the argument values evaluates to true.
Currently, Iassert are introduced in two places:

In both cases, it is easy to derive these equalities from the match_states correctness invariant. The robustness proof then inverts the semantic derivation to recover these equalities.
Most RTL source-to-source passes remove Iassert by compiling it to an Inop, to simplify the correctness proof. It would be possible, in most cases, to preserve the Iassert (as it is invariant under register set and memory extension). However, it is not clear if there would be a point, as Iassert are currently useful only in relation with the program produced by the countermeasure pass.

Compilation passes

Pass Source & target Compiler code Correctness proof Robustness proof
Passes introduced in RTL
Intra-procedural SWIFT RTL to RTL CFC CFCproof CFCsecurity
Inter-procedural SWIFT RTL to RTL IPCFC IPCFCproof IPCFCsecurity
Expansion of builtin_observe RTL to RTL ExpandObserve ExpandObserveproof N/A
Passes introduced in BTL
Load Duplication BTL to BTL BTL_SBsecupasses BTL_BlockSimulationproof N/A

basile.pesin@univ-grenoble-alpes.fr