TY - GEN
T1 - Verifying Redundant-Check Based Countermeasures
T2 - 37th ACM/SIGAPP Symposium on Applied Computing, SAC 2022
AU - Martin, Thibault
AU - Kosmatov, Nikolai
AU - Prevosto, Virgile
N1 - Publisher Copyright:
© 2022 Owner/Author.
PY - 2022/4/25
Y1 - 2022/4/25
N2 - 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.
AB - 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.
KW - deductive verification
KW - fault injection attacks
KW - frama-C verification platform
KW - software countermeasures
UR - https://www.scopus.com/pages/publications/85130417162
U2 - 10.1145/3477314.3507341
DO - 10.1145/3477314.3507341
M3 - Conference contribution
AN - SCOPUS:85130417162
T3 - Proceedings of the ACM Symposium on Applied Computing
SP - 1849
EP - 1852
BT - Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, SAC 2022
PB - Association for Computing Machinery
Y2 - 25 April 2022 through 29 April 2022
ER -