Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download

https://hal.inria.fr/hal-01629135
Contributor : Thomas Given-Wilson Connect in order to contact the contributor
Submitted on : Monday, November 6, 2017 - 9:59:43 AM
Last modification on : Monday, April 4, 2022 - 9:28:22 AM
Long-term archiving on: : Wednesday, February 7, 2018 - 1:17:01 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01629135, version 1

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⟩

Share

Metrics

Record views

407

Files downloads

2653