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
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.
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.
assert
:
exec_Iassert
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 makeThis should generate a
ccomp
executable for the compiler.
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.cThis 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
The application of countermeasures is mainly controlled by the following compiler options:
-fsecu-cfc
intra-procedural control-flow checking [on]-fsecu-cfc-return
intra-procedural control-flow checks before returns [off]-fsecu-ip-cfc
inter-procedural control-flow checking [off]-fsecu-dup-loads
load duplication [on]-fsecu-*
options in the full list of options.
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; }
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.
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:
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.
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:
match_states
correctness invariant.
The robustness proof then inverts the semantic derivation to recover these
equalities.
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 |