An Automated and Scalable Formal Process for Detecting Fault Injection Vulnerabilities in Binaries

Thomas Given-Wilson 1 Annelie Heuser 1 Nisrine Jafri 1 Jean-Louis Lanet 1 Axel Legay 1
1 TAMIS - Threat Analysis and Mitigation for Information Security
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Fault injection has increasingly been used both to attack software applications, and to test system robustness. Detecting fault injection vulnerabilities has been approached with a variety of different but limited methods. This paper proposes an extension of a recently published general model checking based process to detect fault injection vulnerabilities in binaries. This new extension makes the general process scalable to real-world implementions which is demonstrated by detecting vulnerabilities in different cryptographic implementations.
Keywords : Fault Injection Encryption Vulnerability Model Checking Attack
Type de document :
Pré-publication, Document de travail
2017
Liste complète des métadonnées

Littérature citée [35 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01629135
Contributeur : Thomas Given-Wilson <>
Soumis le : lundi 6 novembre 2017 - 09:59:43
Dernière modification le : mercredi 16 mai 2018 - 11:24:14
Document(s) archivé(s) le : mercredi 7 février 2018 - 13:17:01

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01629135, version 1

Collections

INRIA | IRISA | INRIA2017 | UR1-UFR-ISTIC | UNIV-RENNES | CENTRALESUPELEC | CHAIRE-CYBERSECURITE

Citation

Thomas Given-Wilson, Annelie Heuser, Nisrine Jafri, Jean-Louis Lanet, Axel Legay. An Automated and Scalable Formal Process for Detecting Fault Injection Vulnerabilities in Binaries. 2017. 〈hal-01629135〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

249

Téléchargements de fichiers

940

Contact


archive-ouverte@inria.fr