An automated and scalable formal process for detecting fault injection vulnerabilities in binaries. (14th September 2018)

• Record Type: Journal Article
• Authors: Given‐Wilson, Thomas; Heuser, Annelie; Jafri, Nisrine; Legay, Axel
• Other Names: Chen Jinjun guestEditor.; Zheng Xianghan guestEditor.; Rong Chunming guestEditor.; Badarch Tuyatsetseg guestEditor.; Nanda Priyadarsi guestEditor.; Puthal Deepak guestEditor.; Mohanty Saraju P. guestEditor.
• Is Part Of: Concurrency and computation. Volume 31:Number 23(2019)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2018-09-14
• Subjects: attack -- encryption -- fault injection -- model checking -- vulnerability; Parallel processing (Electronic computers) -- Periodicals; Parallel computers -- Periodicals; 004.35
• DOI: 10.1002/cpe.4794
• Languages: English
• ISSNs: 1532-0626

Abstract

Summary: 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 implementations, which is demonstrated by detecting vulnerabilities in different cryptographic implementations.