[CPP'25] Formally verified hardening of C programs against hardware fault injection скачать в хорошем качестве

[CPP'25] Formally verified hardening of C programs against hardware fault injection

Formally Verified Hardening of C Programs against Hardware Fault Injection (Video, CPP 2025) Basile Pesin, Sylvain Boulmé, David Monniaux, and Marie-Laure Potet (Ecole Nationale de l'Aviation Civile, France; University Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France; University Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France; University Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France) Abstract: 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, and measured the effect of optimizations on security and performance. Article: https://doi.org/10.1145/3703595.3705880 ORCID: https://orcid.org/0000-0002-3575-7770, https://orcid.org/0000-0002-9501-9606, https://orcid.org/0000-0001-7671-6126, https://orcid.org/0000-0002-7070-6290 Video Tags: Formally Verified Compiler, Software Counter-Measure, Control Flow Integrity, Coq Proof Assistant, poplws25cppmain-p52-p, doi:10.1145/3703595.3705880, orcid:0000-0002-3575-7770, orcid:0000-0002-9501-9606, orcid:0000-0001-7671-6126, orcid:0000-0002-7070-6290 Presentation at the CPP 2025 conference, January 20-21, 2025, https://popl25.sigplan.org/home/CPP-2025 Sponsored by ACM SIGPLAN and ACM SIGLOG