PROSECCO: Formally-proven secure compiled code
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.
Origin : Files produced by the author(s)
