Skip to Main content Skip to Navigation
Conference papers

Verifying redundant-check based countermeasures: a case study

Thibault Martin 1 Nikolai Kosmatov 2 Virgile Prevosto 1 
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : To thwart fault injection based attacks on critical embedded systems, designers of sensitive software use redundancy based countermeasure schemes. In some of these schemes, critical checks (i.e. conditionals) in the code are duplicated to ensure that an attacker cannot bypass such a check by flipping its result in order to get to a protected point (corresponding e.g. to a successful authentication or code integrity verification). This short paper presents a source-code-level verification technique of the correct implementation of such countermeasures. It is based on code instrumentation and deductive verification. The proposed technique was implemented in a tool prototype and evaluated on a real-life case study: the bootloader module of a secure USB storage device called WooKey, supposed to be resistant to fault injection attacks. We were able to prove the correctness of almost all redundant-check countermeasures in the module except two, and found an error in one of the unproven ones.
Complete list of metadata
Contributor : Contributeur MAP CEA Connect in order to contact the contributor
Submitted on : Tuesday, July 5, 2022 - 2:56:36 PM
Last modification on : Friday, July 8, 2022 - 4:15:29 AM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2022-12-14

Please log in to resquest access to the document



Thibault Martin, Nikolai Kosmatov, Virgile Prevosto. Verifying redundant-check based countermeasures: a case study. SAC' 2022 - The 37th ACM Symposium on Applied Computing, Apr 2022, Brno (virtual event), Czech Republic. pp.1849-1852, ⟨10.1145/3477314.3507341⟩. ⟨cea-03714409⟩



Record views