International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Paper: FIVER – Robust Verification of Countermeasures against Fault Injections

Authors:
Jan Richter-Brockmann , Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany
Aein Rezaei Shahmirzadi , Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany
Pascal Sasdrich , Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany
Amir Moradi , Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany
Tim Güneysu , Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum, Germany; DFKI, Bremen, Germany
Download:
DOI: 10.46586/tches.v2021.i4.447-473
URL: https://tches.iacr.org/index.php/TCHES/article/view/9072
Search ePrint
Search Google
Abstract: Fault Injection Analysis is seen as a powerful attack against implementations of cryptographic algorithms. Over the last two decades, researchers proposed a plethora of countermeasures to secure such implementations. However, the design process and implementation are still error-prone, complex, and manual tasks which require long-standing experience in hardware design and physical security. Moreover, the validation of the claimed security is often only done by empirical testing in a very late stage of the design process. To prevent such empirical testing strategies, approaches based on formal verification are applied instead providing the designer early feedback.In this work, we present a fault verification framework to validate the security of countermeasures against fault-injection attacks designed for ICs. The verification framework works on netlist-level, parses the given digital circuit into a model based on Binary Decision Diagrams, and performs symbolic fault injections. This verification approach constitutes a novel strategy to evaluate protected hardware designs against fault injections offering new opportunities as performing full analyses under a given fault models.Eventually, we apply the proposed verification framework to real-world implementations of well-established countermeasures against fault-injection attacks. Here, we consider protected designs of the lightweight ciphers CRAFT and LED-64 as well as AES. Due to several optimization strategies, our tool is able to perform more than 90 million fault injections in a single-round CRAFT design and evaluate the security in under 50 min while the symbolic simulation approach considers all 2128 primary inputs.
Video from TCHES 2021
BibTeX
@article{tches-2021-31323,
  title={FIVER – Robust Verification of Countermeasures against Fault Injections},
  journal={IACR Transactions on Cryptographic Hardware and Embedded Systems},
  publisher={Ruhr-Universität Bochum},
  volume={2021, Issue 4},
  pages={447-473},
  url={https://tches.iacr.org/index.php/TCHES/article/view/9072},
  doi={10.46586/tches.v2021.i4.447-473},
  author={Jan Richter-Brockmann and Aein Rezaei Shahmirzadi and Pascal Sasdrich and Amir Moradi and Tim Güneysu},
  year=2021
}