Abstract
Masking is a popular countermeasure against side-channel attacks, which randomizes secret data with random and uniform variables called masks. At software level, masking is usually added in the source code and its effectiveness needs to be verified. In this paper, we propose a symbolic method to verify side-channel robustness of masked programs. The analysis is performed at the assembly level since compilation and optimizations may alter the added protections. Our proposed method aims to verify that intermediate computations are statistically independent from secret variables using defined distribution inference rules. We verify the first round of a masked AES in 22 s and show that some secure algorithms or source codes are not leakage-free in their assembly implementations.
Similar content being viewed by others
References
Balasch, J., Gierlichs, B., Grosso, V., Reparaz, O., Standaert, F.-X.: On the cost of lazy engineering for masked software implementations. In: International Conference on Smart Card Research and Advanced Applications, pp. 64–81. Springer (2014)
Barthe, G., Belaïd, S., Dupressoir, F., Fouque, P.-A., Grégoire, B., Strub, P.-Y.: Verified proofs of higher-order masking. In: Eurocrypt 2015, number 9056 (2015)
Barthe, G., Dupressoir, F., Faust, S., Grégoire, B., Standaert, F.-X., Strub, P.-Y.: Parallel implementations of masking schemes and the bounded moment leakage model. In: Annual International Conference on the Theory and Applications of Cryptographic Techniques, pp. 535–566. Springer (2017)
Bayrak, A.G., Regazzoni, F., Novo, D., Brisk, P., Standaert, F.-X., Ienne, P.: Automatic application of power analysis countermeasures. IEEE Trans. Comput. 64(2), 329–341 (2015)
Beaulieu, R., Shors, D., Smith, J., Treatman-Clark, S., Weeks, B., Wingers, L.: The SIMON and SPECK families of lightweight block ciphers. IACR Cryptol. 2013, 404 (2013)
Bilgin, B., Gierlichs, B., Nikova, S., Nikov, V., Rijmen, V.: Higher-order threshold implementations. In: Lecture Notes in Computer Science, vol. 8874, pp. 326–343. Springer (2014)
Blömer, J., Guajardo, J., Krummel, V.: Provably secure masking of aes. In: International Workshop on Selected Areas in Cryptography, pp. 69–83. Springer (2004)
Chen, C., Inci, M.S., Taha, M., Eisenbarth, T.: Spectre: a tiny side-channel resistant speck core for fpgas. IACR Cryptol. 2015, 691 (2015)
Coron, J.-S.: Higher order masking of look-up tables. In: Annual International Conference on the Theory and Applications of Cryptographic Techniques, pp. 441–458. Springer (2014)
Coron, J.-S., Großschädl, J., Tibouchi, M., Vadnala, P. K.: Conversion from arithmetic to boolean masking with logarithmic complexity. In: International Workshop on Fast Software Encryption, pp. 130–149. Springer (2015)
Coron, J.-S., Prouff, E., Rivain, M.: Side channel cryptanalysis of a higher order masking scheme. In: International Workshop on Cryptographic Hardware and Embedded Systems, pp. 28–44. Springer (2007)
Eldib, H., Wang, C.: Synthesis of masking countermeasures against side channel attacks. CAV 8559, 114–130 (2014)
Eldib, H., Wang, C., Schaumont, P.: Formal verification of software countermeasures against side-channel attacks. ACM Trans. Softw. Eng. Methodol. 24(2), 11 (2014)
Eldib, H., Wang, C., Taha, M., Schaumont, P.: Quantitative masking strength: quantifying the power side-channel resistance of software code. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 34(10), 1558–1568 (2015)
Goodwill, G., Jun, B., Jaffe, J., Rohatgi, P.: A testing methodology for side-channel resistance validation. In: NIST Non-invasive Attack Testing Workshop (2011)
Goubin, L.: A sound method for switching between boolean and arithmetic masking. In: Cryptographic Hardware and Embedded SystemsCHES 2001, pp. 3–15. Springer (2001)
Herbst, C., Oswald, E., Mangard, S.: An aes smart card implementation resistant to power analysis attacks. In: ACNS, vol. 3989, pp. 239–252. Springer (2006)
Kocher, P.C.: Timing attacks on implementations of Diffie-Hellman, rsa, dss, and other systems. In: Annual International Cryptology Conference, pp. 104–113. Springer (1996)
Microsoft Research. Z3py-python interface for the z3 theorem prover (2012)
Papagiannopoulos, K., Veshchikov, N.: Mind the gap: towards secure 1st-order masking in software. IACR Cryptol. 2017, 345 (2017)
Prouff, E., Rivain, M.: Masking against side-channel attacks: a formal security proof. In: Annual International Conference on the Theory and Applications of Cryptographic Techniques, pp. 142–159. Springer (2013)
Reparaz, O.: Detecting flawed masking schemes with leakage detection tests. In: Lecture Notes in Computer Science. Springer (2016)
Reparaz, O., Gierlichs, B., Verbauwhede, I.: Fast leakage assessment. In: International Conference on Cryptographic Hardware and Embedded Systems. Springer (2017)
Ronen, E., OFlynn, C., Shamir, A., Weingarten, A.-O.: IoT Goes Nuclear: Creating a ZigBee Chain Reaction. Technical Report 1047 (2016)
Shahverdi, A., Taha, M., Eisenbarth, T.: Lightweight side channel resistance: threshold implementations of simon. IEEE Trans. Comput. 66(4), 661–671 (2017)
Standaert, F.-X.: How (not) to use Welch’s t-test in side-channel security evaluations. IACR Cryptol. 2017, 138 (2017)
Strobel, D., Oswald, D., Richter, B., Schellenberg, F., Paar, C.: Microcontrollers as (in)security devices for pervasive computing applications. Proc. IEEE 102(8), 1157–1173 (2014)
Veshchikov, N.: Silk: high level of abstraction leakage simulator for side channel analysis. In: Proceedings of the 4th Program Protection and Reverse Engineering Workshop. ACM (2014)
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Ben El Ouahma, I., Meunier, Q.L., Heydemann, K. et al. Side-channel robustness analysis of masked assembly codes using a symbolic approach. J Cryptogr Eng 9, 231–242 (2019). https://doi.org/10.1007/s13389-019-00205-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s13389-019-00205-7