POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Tue 21 Jan 2025 11:30 - 12:00 at Marco Polo - Session 6 Chair(s): Kathrin Stark

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 Jan

Displayed time zone: Mountain Time (US & Canada) change

11:00 - 12:30
Session 6CPP at Marco Polo
Chair(s): Kathrin Stark Heriot-Watt University
11:00
30m
Talk
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
30m
Talk
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
30m
Talk
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