Skip to Main content Skip to Navigation
Conference papers

PROSECCO: Formally-proven secure compiled code

Nicolas Belleville 1 Damien Courousse 1 Emmanuelle Encrenaz 2 Karine Heydemann 2 Quentin Meunier 2 
1 LFIM - Laboratoire Fonctions Innovantes pour circuits Mixtes
UGA - Université Grenoble Alpes, DSCIN - Département Systèmes et Circuits Intégrés Numériques : DRT/LIST/DSCIN
Abstract : The application and the verification of countermeasures against physical attacks still remain long, error-prone and expertise-demanding tasks. We propose a toolchain to help the expert in these tasks. Our toolchain is composed of two components: a compiler that automatically applies a set of countermeasures, and a formal verification tool that automatically verifies binary code for various leakage models and fault models. We describe different scenarios of usage of our toolchain, and then illustrate the flexibility of our toolchain in one of them.
Complete list of metadata
Contributor : Contributeur MAP CEA Connect in order to contact the contributor
Submitted on : Thursday, March 10, 2022 - 6:00:21 PM
Last modification on : Monday, March 14, 2022 - 10:27:09 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution - NonCommercial - NoDerivatives 4.0 International License


  • HAL Id : cea-03605070, version 1


Nicolas Belleville, Damien Courousse, Emmanuelle Encrenaz, Karine Heydemann, Quentin Meunier. PROSECCO: Formally-proven secure compiled code. C&ESAR 2021 : 28th Computer Electronics Security Application Rendezvous, Nov 2021, Rennes, France. pp.13-25. ⟨cea-03605070⟩



Record views


Files downloads