Formally verified hardening of C programs against hardware fault injection
This program is tentative and subject to change.
A fault attack is a malicious manipulation of the hardware (e.g., electromagnetic or laser pulse) that modifies the behavior of the software. Fault attacks typically target sensitive applications such as cryptography services, authentication, boot-loaders or firmware updaters. They can be defended against by adding countermeasures, that is, control flow checks and redundancies, either in the hardware, or in the software running on it. In particular, software countermeasures may be added automatically during compilation.
In this paper, we describe a formally verified implementation of this approach in the CompCert verified compiler for the C language. We implemented two existing countermeasures protecting the control flow of the program as program transformations over a middle-end intermediate representation of CompCert, RTL. We proved that these countermeasures are correct, that is, they do not change the observable behavior of the program during an execution without fault injection. We then modeled the effect of a fault on the behavior of the program as an extension of the semantic model of RTL. We used this new model to formally prove the efficacy of the countermeasure: all attacks are either caught, or produce no observable effects. In addition to this formal reasoning, we evaluated the protected program using Lazart, a tool for symbolic fault injection.
This program is tentative and subject to change.
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
11:00 - 12:30 | |||
11:00 30mTalk | Leakage-Free Probabilistic Jasmin Programs CPP Denis Firsov Tallinn University of Technology, Tiago Oliveira SandboxAQ, José Bacelar Almeira University of Minho & INESC TEC, Dominique Unruh RWTH Aachen | ||
11:30 30mTalk | Formally verified hardening of C programs against hardware fault injection CPP Basile Pesin Ecole Nationale de l'Aviation Civile (ENAC), Sylvain Boulmé Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, David Monniaux CNRS, Marie-Laure Potet Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG Pre-print | ||
12:00 30mTalk | CertiCoq-Wasm: A verified WebAssembly backend for CertiCoq CPP Wolfgang Meier Aarhus University, Martin Jensen Aarhus University, Jean Pichon-Pharabod Aarhus University, Bas Spitters Aarhus University Pre-print |