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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Throughout this manuscript, we will use the terms countermeasure(s) and protection(s) interchangeably.
- 2.
Seeing as a fault can, however, corrupt flags and/or register contents, control-flow and memory content can be affected indirectly.
References
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
Moro, N.: Sécurisation de programmes assembleur face aux attaques visant lesprocesseurs embarqués.Ph.D. thesis, UPMC, France (2014)
De Keulenaer, R., Maebe, J., De Bosschere, K., De Sutter, B.: Link-time smart card code hardening. Int. J. Inf. Secur. 1–20 (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Goubet, L., Heydemann, K., Encrenaz, E., De Keulenaer, R. (2016). Efficient Design and Evaluation of Countermeasures against Fault Attacks Using Formal Verification. In: Homma, N., Medwed, M. (eds) Smart Card Research and Advanced Applications. CARDIS 2015. Lecture Notes in Computer Science(), vol 9514. Springer, Cham. https://doi.org/10.1007/978-3-319-31271-2_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-31271-2_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-31270-5
Online ISBN: 978-3-319-31271-2
eBook Packages: Computer ScienceComputer Science (R0)