nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Efficient Design and Evaluation of Countermeasures against Fault Attacks Using Formal Verification

verfasst von : Lucien Goubet, Karine Heydemann, Emmanuelle Encrenaz, Ronald De Keulenaer

Erschienen in: Smart Card Research and Advanced Applications

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

This paper presents a formal verification framework and tool that evaluates the robustness of software countermeasures against fault-injection attacks. By modeling reference assembly code and its protected variant as automata, the framework can generate a set of equations for an SMT solver, the solutions of which represent possible attack paths. Using the tool we developed, we evaluated the robustness of state-of-the-art countermeasures against fault injection attacks. Based on insights gathered from this evaluation, we analyze any remaining weaknesses and propose applications of these countermeasures that are more robust.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Protecting the Control Flow of Embedded Processors against Fault Attacks

Nächstes Kapitel Precise Laser Fault Injections into 90 nm and 45 nm SRAM-cells

Throughout this manuscript, we will use the terms countermeasure(s) and protection(s) interchangeably.

Seeing as a fault can, however, corrupt flags and/or register contents, control-flow and memory content can be affected indirectly.

Bar-El, H., Choukri, H., Naccache, D., Tunstall, M., Whelan, C.: The sorcerer’s apprentice guide to fault attacks. Proc. IEEE 94(2), 370–382 (2006)CrossRef

Bhasin, S., Maistri, P., Regazzoni, F.: Malicious wave: A survey on actively tampering using electromagnetic glitch. In: International Symposium on Electromagnetic Compatibility, pp. 318–321 (2014)

Boneh, D., DeMillo, R.A., Lipton, R.J.: On the importance of checking cryptographic protocols for faults. In: Fumy, W. (ed.) EUROCRYPT 1997. LNCS, vol. 1233, pp. 37–51. Springer, Heidelberg (1997)CrossRef

Biham, E., Shamir, A.: Differential fault analysis of secret key cryptosystems. In: Kaliski Jr., B.S. (ed.) CRYPTO 1997. LNCS, vol. 1294, pp. 513–525. Springer, Heidelberg (1997)CrossRef

Amiel, F., Villegas, K., Feix, B., Marcel, L.: Passive and active combined attacks: combining fault attacks and side channel analysis. In: Workshop on Fault Diagnosis and Tolerance in Cryptography FDTC, pp. 92–102 (2007)

Rauzy, P., Guilley, S.: A formal proof of countermeasures against fault injection attacks onCRT-RSA. J. Cryptographic Eng. JCEN 4(3), 173–185 (2014)CrossRef

Lalande, J.-F., Heydemann, K., Berthomé, P.: Software countermeasures for control flow integrity of smart card C codes. In: Kutyłowski, M., Vaidya, J. (eds.) ICAIS 2014, Part II. LNCS, vol. 8713, pp. 200–218. Springer, Heidelberg (2014)

Asghari, S., Abdi, A., Taheri, H., Pedram, H., Pourmozaffari, S.: SEDSR: soft error detection using software redundancy. J. Softw. Eng. Appl. 5, 664 (2012)CrossRef

Goloubeva, O., Rebaudengo, M., Reorda, M., Violante, M.: Improved software-based processor control-flow errors detection technique. In: Reliability and Maintainability Symposium, pp. 583–589 (2005)

10.

Barenghi, A., Breveglieri, L., Koren, I., Pelosi, G., Regazzoni, F.: Countermeasures against fault attacks on software implemented AES: effectiveness and cost. In: 5th Workshop on Embedded Systems Security, pp. 7:1–7:10. ACM (2010)

11.

Reis, G., Chang, J., Vachharajani, N., Rangan, R., August, D.: SWIFT: software implemented fault tolerance. In: International Symposium on Code Generation and Optimization, pp. 243–254 (2005)

12.

Moro, N., Heydemann, K., Encrenaz, E., Robisson, B.: Formal verification of a software countermeasure against instruction skip attacks. J. Cryptographic Eng. 4(3), 145–156 (2014)CrossRef

13.

Verbauwhede, I., Karaklajic, D., Schmidt, J.: The fault attack jungle-A classification model to guide you. In: Workshop on Fault Diagnosis and Tolerance in Cryptography (FDTC), pp. 3–8. IEEE (2011)

14.

Goloubeva, O., Rebaudengo, M., Reorda, M., Violante, M.: Soft-error detection using control flow assertions. In: 18th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, pp. 581–588 (2003)

15.

Bayrak, A.G., Regazzoni, F., Novo, D., Ienne, P.: Sleuth: automated verification of software power analysis countermeasures. In: Bertoni, G., Coron, J.-S. (eds.) CHES 2013. LNCS, vol. 8086, pp. 293–310. Springer, Heidelberg (2013)CrossRef

16.

Eldib, H., Wang, C.: Synthesis of masking countermeasures against side channel attacks. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 114–130. Springer, Heidelberg (2014)

17.

Potet, M.L., Mounier, L., Puys, M., Dureuil, L.: Lazart: a symbolic approach for evaluation the robustness of secured codes against control flow fault injection. In: ICST.(2014)

18.

Chetali, B., Nguyen, Q.-H.: Industrial use of formal methods for a high-level security evaluation. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 198–213. Springer, Heidelberg (2008)CrossRef

19.

Moro, N.: Sécurisation de programmes assembleur face aux attaques visant lesprocesseurs embarqués.Ph.D. thesis, UPMC, France (2014)

20.

De Keulenaer, R., Maebe, J., De Bosschere, K., De Sutter, B.: Link-time smart card code hardening. Int. J. Inf. Secur. 1–20 (2015)

Titel: Efficient Design and Evaluation of Countermeasures against Fault Attacks Using Formal Verification
verfasst von: Lucien Goubet
Karine Heydemann
Emmanuelle Encrenaz
Ronald De Keulenaer
Verlag: Springer International Publishing
Buch: Smart Card Research and Advanced Applications
Print ISBN: 978-3-319-31270-5

Electronic ISBN: 978-3-319-31271-2

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-31271-2_11

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner