The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.

Verifying redundant-check based countermeasures: a case study

The work

AuthorsThibault Martin; Nikolaï Kosmatov; Virgile Prévosto
Editors
Typemisc
Year2022
Citekeymartin2022verifying

Where it appeared

Published inACM Symposium on Applied Computing
Pages1849--1852

Identifiers

DOI10.1145/3477314.3507341
OpenAlexW4229041820

From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.

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.

How it got here

How it got hereagent via openalex
Added2026-10-27 05:45 UTC
Not denied bya person 2026-10-29 17:12 UTC

Cite it as

@misc{martin2022verifying,
  title        = {Verifying redundant-check based countermeasures: a case study},
  author       = {Thibault Martin and Nikolaï Kosmatov and Virgile Prévosto},
  year         = {2022},
  journal      = {ACM Symposium on Applied Computing},
  pages        = {1849--1852},
  doi          = {10.1145/3477314.3507341},
}

This record lives at https://refs.drheap.org/martin2022verifying/ and will keep doing so.