PROSECCO: Formally-proven secure compiled code - Archive ouverte HAL Access content directly
Conference Papers Year : 2021

PROSECCO: Formally-proven secure compiled code

(1) , (1) , (2) , (2) , (2)
1
2

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.
L’application et la vérification de contre-mesures contre les attaques physiques sont des tâches qui sont longues, qui comportent un important risque d’erreur, et qui demandent une forte expertise. Nous proposons une chaîne d’outils pour aider les experts dans ces tâches. Notre chaîne d’outils se décompose en deux élements : un compilateur capable d’appliquer automatiquement différentes contremesures contre les attaques en fautes ou par canal auxiliaire, et un outil de vérification formelle dont le but est de vérifier automatiquement la robustesse des codes binaires en considérant des modèles de fuites et de fautes variés. Nous décrivons plusieurs scénarios d’utilisation de notre chaîne d’outils, et illustrons la flexibilité de celle-ci sur un de ces scénarios.
Fichier principal
Vignette du fichier
PROSECCO.pdf (841.36 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

cea-03605070 , version 1 (10-03-2022)

Licence

Attribution - NonCommercial - NoDerivatives - CC BY 4.0

Identifiers

  • HAL Id : cea-03605070 , version 1

Cite

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⟩
50 View
35 Download

Share

Gmail Facebook Twitter LinkedIn More