Abstract
Security analysis is a crucial concern in the design of hardware and software systems, yet there is a distinct lack of automated methodologies. In this paper, we remedy this situation for the verification of software countermeasure implementations. In this context, verifying the security of a protected implementation against side-channel attacks corresponds to assessing whether any particular leakage in any particular computational phase is statistically dependent on the secret data and statistically independent of any random information used to protect the implementation. We present a novel methodology to reduce this verification problem into a set of Boolean satisfiability problems, which can be efficiently solved by leveraging recent advances in SAT solving. To show the effectiveness of our methodology, we have implemented an automatic verification tool, named Sleuth, as an advanced analysis pass in the back-end of the LLVM compiler. Our results show that one can automatically detect several examples of classic pitfalls in the implementation of countermeasures with reasonable runtimes.
Chapter PDF
Similar content being viewed by others
Keywords
References
The KLEE symbolic virtual machine, http://klee.llvm.org
The LLVM compiler infrastructure, http://llvm.org
SAT competitions, http://www.satcompetition.org
Agosta, G., Barenghi, A., Pelosi, G.: A code morphing methodology to automate power analysis countermeasures. In: Design Automation Conference, DAC 2012, pp. 77–82 (2012)
Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers – Principles, Techniques, & Tools. Pearson (2006)
Badel, S., Guleyupoglu, E., Inac, O., Martinez, A.P., Vietti, P., Grkaynak, F.K., Leblebici, Y.: A generic standard cell design methodology for differential circuit styles. In: Design, Automation and Test in Europe, DATE 2008, pp. 843–848 (2008)
Bayrak, A.G., Regazzoni, F., Brisk, P., Standaert, F.X., Ienne, P.: A first step towards automatic application of power analysis countermeasures. In: Design Automation Conference, DAC 2011, pp. 230–235 (June 2011)
Blömer, J., Guajardo, J., Krummel, V.: Provably secure masking of AES. In: Handschuh, H., Hasan, M.A. (eds.) SAC 2004. LNCS, vol. 3357, pp. 69–83. Springer, Heidelberg (2004)
Bohn, R.E., Short, J.E.: How much information? 2009 Report on American consumers (December 2009)
Cleemput, J.V., Coppens, B., de Sutter, B.: Compiler mitigations for time attacks on modern x86 processors. ACM Transactions on Architecture and Code Optimization 8(4), 23:1–23:20 (2012)
Computer Aided Cryptography Engineering (CACE European Project), http://www.cace-project.eu
Coron, J.-S., Goubin, L.: On Boolean and arithmetic masking against differential power analysis. In: Paar, C., Koç, Ç.K. (eds.) CHES 2000. LNCS, vol. 1965, pp. 231–237. Springer, Heidelberg (2000)
Enck, W., Gilbert, P., Chun, B.G., Cox, L.P., Jung, J., McDaniel, P., Sheth, A.N.: TaintDroid: An information-flow tracking system for realtime privacy monitoring on smartphones. In: USENIX Conference on Operating Systems Design and Implementation, pp. 1–6 (2010)
Ford, B.: Plugging side-channel leaks with timing information flow control. arXiv preprint arXiv:1203.3428 (2012)
Fumaroli, G., Martinelli, A., Prouff, E., Rivain, M.: Affine masking against higher-order side channel analysis. Cryptology ePrint Archive, Report 2010/523 (2010), http://eprint.iacr.org/
Gandolfi, K., Mourtel, C., Olivier, F.: Electromagnetic analysis: Concrete results. In: Koç, Ç.K., Naccache, D., Paar, C. (eds.) CHES 2001. LNCS, vol. 2162, pp. 251–261. Springer, Heidelberg (2001)
Gierlichs, B., Batina, L., Preneel, B., Verbauwhede, I.: Revisiting higher-order DPA attacks. In: Pieprzyk, J. (ed.) CT-RSA 2010. LNCS, vol. 5985, pp. 221–234. Springer, Heidelberg (2010)
Goubin, L.: A sound method for switching between Boolean and arithmetic masking. In: Koç, Ç.K., Naccache, D., Paar, C. (eds.) CHES 2001. LNCS, vol. 2162, pp. 3–15. Springer, Heidelberg (2001)
Herbst, C., Oswald, E., Mangard, S.: An AES smart card implementation resistant to power analysis attacks. In: Zhou, J., Yung, M., Bao, F. (eds.) ACNS 2006. LNCS, vol. 3989, pp. 239–252. Springer, Heidelberg (2006)
Gray III, J.W.: Toward a mathematical foundation for information flow security. Journal of Computer Security 1(3), 255–294 (1992)
Kocher, P., Jaffe, J., Jun, B.: Differential power analysis. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 398–412. Springer, Heidelberg (1999)
Mangard, S., Oswald, E., Popp, T.: Power Analysis Attacks - Revealing the Secrets of Smart Cards. Springer (2007)
Messerges, T.S.: Securing the AES finalists against power analysis attacks. In: Schneier, B. (ed.) FSE 2000. LNCS, vol. 1978, pp. 150–164. Springer, Heidelberg (2001)
Mishchenko, A., Brayton, R.K.: SAT-based complete don’t-care computation for network optimization. In: Design, Automation and Test in Europe, DATE 2005, pp. 412–417 (2005)
Moss, A., Oswald, E., Page, D., Tunstall, M.: Compiler assisted masking. In: Prouff, E., Schaumont, P. (eds.) CHES 2012. LNCS, vol. 7428, pp. 58–75. Springer, Heidelberg (2012)
Osvik, D.A., Shamir, A., Tromer, E.: Cache attacks and countermeasures: The case of AES. In: Pointcheval, D. (ed.) CT-RSA 2006. LNCS, vol. 3860, pp. 1–20. Springer, Heidelberg (2006)
Popp, T., Kirschbaum, M., Zefferer, T., Mangard, S.: Evaluation of the masked logic style MDPL on a prototype chip. In: Paillier, P., Verbauwhede, I. (eds.) CHES 2007. LNCS, vol. 4727, pp. 81–94. Springer, Heidelberg (2007)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Tillich, S., Großschädl, J.: Power analysis resistant AES implementation with instruction set extensions. In: Paillier, P., Verbauwhede, I. (eds.) CHES 2007. LNCS, vol. 4727, pp. 303–319. Springer, Heidelberg (2007)
Tiri, K., Verbauwhede, I.: A logic level design methodology for a secure DPA resistant ASIC or FPGA implementation. In: Design, Automation and Test in Europe, DATE 2004, pp. 246–251 (2004)
Tiri, K., Verbauwhede, I.: A digital design flow for secure integrated circuits. IEEE Transactions on CAD of Integrated Circuits and Systems 25(7), 1197–1208 (2006)
Tiwari, M., Wassel, H.M.G., Mazloom, B., Mysore, S., Chong, F.T., Sherwood, T.: Complete information flow tracking from the gates up. ACM Sigplan Notices 44(3), 109–120 (2009)
Vieira, B.: Formal Verification of Cryptographic Software Implementations. Ph.D. thesis, Universidade do Minho, Portugal (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 International Association for Cryptologic Research
About this paper
Cite this paper
Bayrak, A.G., Regazzoni, F., Novo, D., Ienne, P. (2013). Sleuth: Automated Verification of Software Power Analysis Countermeasures. In: Bertoni, G., Coron, JS. (eds) Cryptographic Hardware and Embedded Systems - CHES 2013. CHES 2013. Lecture Notes in Computer Science, vol 8086. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40349-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-40349-1_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40348-4
Online ISBN: 978-3-642-40349-1
eBook Packages: Computer ScienceComputer Science (R0)