Advertisement

Formal Verification of Masked Hardware Implementations in the Presence of Glitches

  • Roderick Bloem
  • Hannes Gross
  • Rinat Iusupov
  • Bettina Könighofer
  • Stefan Mangard
  • Johannes Winter
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10821)

Abstract

Masking provides a high level of resistance against side-channel analysis. However, in practice there are many possible pitfalls when masking schemes are applied, and implementation flaws are easily overlooked. Over the recent years, the formal verification of masked software implementations has made substantial progress. In contrast to software implementations, hardware implementations are inherently susceptible to glitches. Therefore, the same methods tailored for software implementations are not readily applicable.

In this work, we introduce a method to formally verify the security of masked hardware implementations that takes glitches into account. Our approach does not require any intermediate modeling steps of the targeted implementation. The verification is performed directly on the circuit’s netlist in the probing model with glitches and covers also higher-order flaws. For this purpose, a sound but conservative estimation of the Fourier coefficients of each gate in the netlist is calculated, which characterize statistical dependence of the gates on the inputs and thus allow to predict possible leakages. In contrast to existing practical evaluations, like t-tests, this formal verification approach makes security statements beyond specific measurement methods, the number of evaluated leakage traces, and the evaluated devices. Furthermore, flaws detected by the verifier are automatically localized. We have implemented our method on the basis of a SAT solver and demonstrate the suitability on a range of correctly and incorrectly protected circuits of different masking schemes and for different protection orders. Our verifier is efficient enough to prove the security of a full masked first-order AES S-box, and of the Keccak S-box up to the third protection order.

Keywords

Masking Formal verification Threshold implementations Hardware security Side-channel analysis Private circuits 

Notes

Acknowledgements

The work has been supported in part by the Austrian Science Fund (FWF) through project P26494-N15, project S114-06, and project W1255-N23. Furthermore this work has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 681402), and from the European Commission (grant agreement No 644905).

Supplementary material

References

  1. 1.
    Barthe, G., Belaïd, S., Dupressoir, F., Fouque, P., Grégoire, B.: Compositional verification of higher-order masking: application to a verifying masking compiler. IACR Cryptology ePrint Archive, 2015:506 (2015)Google Scholar
  2. 2.
    Barthe, G., Belaïd, S., Dupressoir, F., Fouque, P.-A., Grégoire, B., Strub, P.-Y.: Verified proofs of higher-order masking. In: Oswald, E., Fischlin, M. (eds.) EUROCRYPT 2015. LNCS, vol. 9056, pp. 457–485. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46800-5_18Google Scholar
  3. 3.
    Barthe, G., Belaïd, S., Dupressoir, F., Fouque, P., Grégoire, B., Strub, P., Zucchini, R.: Strong non-interference and type-directed higher-order masking. In: Proceedings of the 2016 ACM SIGSAC CCS, Vienna, Austria, 24–28 October 2016, pp. 116–129 (2016)Google Scholar
  4. 4.
    Barthe, G., Dupressoir, F., Faust, S., Grégoire, B., Standaert, F., Strub, P.: Parallel implementations of masking schemes and the bounded moment leakage model. IACR Cryptology ePrint Archive, 2016:912 (2016)Google Scholar
  5. 5.
    Barthe, G., Dupressoir, F., Grégoire, B., Stoughton, A., Strub, P.: EasyCrypt: Computer-Aided Cryptographic Proofs (2017). https://github.com/EasyCrypt/easycrypt
  6. 6.
    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).  https://doi.org/10.1007/978-3-642-40349-1_17CrossRefGoogle Scholar
  7. 7.
    Belaïd, S., Benhamouda, F., Passelègue, A., Prouff, E., Thillard, A., Vergnaud, D.: Randomness complexity of private circuits for multiplication. In: Fischlin, M., Coron, J.-S. (eds.) EUROCRYPT 2016. LNCS, vol. 9666, pp. 616–648. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49896-5_22CrossRefGoogle Scholar
  8. 8.
    Belaïd, S., Benhamouda, F., Passelègue, A., Prouff, E., Thillard, A., Vergnaud, D.: Private multiplication over finite fields. In: Katz, J., Shacham, H. (eds.) CRYPTO 2017. LNCS, vol. 10403, pp. 397–426. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63697-9_14CrossRefGoogle Scholar
  9. 9.
    Bertoni, G., Martinoli, M.: A methodology for the characterisation of leakages in combinatorial logic. In: Carlet, C., Hasan, M.A., Saraswat, V. (eds.) SPACE 2016. LNCS, vol. 10076, pp. 363–382. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-49445-6_21CrossRefGoogle Scholar
  10. 10.
    Bhasin, S., Carlet, C., Guilley, S.: Theory of masking with codewords in hardware: low-weight dth-order correlation-immune boolean functions. IACR Cryptology ePrint Archive, 2013:303 (2013)Google Scholar
  11. 11.
    Bilgin, B., Bogdanov, A., Knežević, M., Mendel, F., Wang, Q.: Fides: lightweight authenticated cipher with side-channel resistance for constrained hardware. In: Bertoni, G., Coron, J.-S. (eds.) CHES 2013. LNCS, vol. 8086, pp. 142–158. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-40349-1_9CrossRefGoogle Scholar
  12. 12.
    Bilgin, B., Gierlichs, B., Nikova, S., Nikov, V., Rijmen, V.: Higher-order threshold implementations. In: Sarkar, P., Iwata, T. (eds.) ASIACRYPT 2014. LNCS, vol. 8874, pp. 326–343. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-45608-8_18Google Scholar
  13. 13.
    Chari, S., Jutla, C.S., Rao, J.R., Rohatgi, P.: Towards sound approaches to counteract power-analysis attacks. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 398–412. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48405-1_26Google Scholar
  14. 14.
    Coron, J.-S.: Formal verification of side-channel countermeasures via elementary circuit transformations. Cryptology ePrint Archive, Report 2017/879Google Scholar
  15. 15.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  16. 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, Cham (2014).  https://doi.org/10.1007/978-3-319-08867-9_8Google Scholar
  17. 17.
    Eldib, H., Wang, C., Schaumont, P.: SMT-based verification of software countermeasures against side-channel attacks. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 62–77. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54862-8_5CrossRefGoogle Scholar
  18. 18.
    Eldib, H., Wang, C., Taha, M.M.I., Schaumont, P.: QMS: evaluating the side-channel resistance of masked software from source code. In: DAC 2014, San Francisco, CA, USA, 1–5 June 2014, pp. 209:1–209:6 (2014)Google Scholar
  19. 19.
    Faust, S., Grosso, V., Pozo, S.M.D., Paglialonga, C., Standaert, F.: Composable masking schemes in the presence of physical defaults and the robust probing model. IACR Cryptology ePrint Archive, 2017:711 (2017)Google Scholar
  20. 20.
    Faust, S., Rabin, T., Reyzin, L., Tromer, E., Vaikuntanathan, V.: Protecting circuits from leakage: the computationally-bounded and noisy cases. In: Gilbert, H. (ed.) EUROCRYPT 2010. LNCS, vol. 6110, pp. 135–156. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-13190-5_7CrossRefGoogle Scholar
  21. 21.
    Goodwill, G., Jun, B., Jaffe, J., Rohatgi, P.: A Testing Methodology for Side-Channel Resistance Validation. In: NIST Non-Invasive Attack Testing Workshop (2011)Google Scholar
  22. 22.
    Gross, H.: Collection of protected hardware implementations. https://github.com/hgrosz
  23. 23.
    Gross, H., Mangard, S.: Reconciling d+1 masking in hardware and software. In: CHES 2017 (2017)Google Scholar
  24. 24.
    Gross, H., Mangard, S., Korak, T.: An efficient side-channel protected AES implementation with arbitrary protection order. In: Handschuh, H. (ed.) CT-RSA 2017. LNCS, vol. 10159, pp. 95–112. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-52153-4_6CrossRefGoogle Scholar
  25. 25.
    Gross, H., Schaffenrath, D., Mangard, S.: Higher-order side-channel protected implementations of keccak. Cryptology ePrint Archive, Report 2017/395Google Scholar
  26. 26.
    Ishai, Y., Sahai, A., Wagner, D.: Private circuits: securing hardware against probing attacks. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 463–481. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-45146-4_27CrossRefGoogle Scholar
  27. 27.
    Iusupov, R.: REBECCA - Masking verification tool. https://github.com/riusupov/rebecca
  28. 28.
    Kocher, P., Jaffe, J., Jun, B.: Differential power analysis. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 388–397. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48405-1_25Google Scholar
  29. 29.
    Mangard, S., Schramm, K.: Pinpointing the side-channel leakage of masked AES hardware implementations. In: Goubin, L., Matsui, M. (eds.) CHES 2006. LNCS, vol. 4249, pp. 76–90. Springer, Heidelberg (2006).  https://doi.org/10.1007/11894063_7CrossRefGoogle Scholar
  30. 30.
    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).  https://doi.org/10.1007/978-3-642-33027-8_4CrossRefGoogle Scholar
  31. 31.
    Nikova, S., Rechberger, C., Rijmen, V.: Threshold implementations against side-channel attacks and glitches. In: Ning, P., Qing, S., Li, N. (eds.) ICICS 2006. LNCS, vol. 4307, pp. 529–545. Springer, Heidelberg (2006).  https://doi.org/10.1007/11935308_38CrossRefGoogle Scholar
  32. 32.
    O’Donnell, R.: Analysis of Boolean Functions. Cambridge University Press, Cambridge (2014)CrossRefzbMATHGoogle Scholar
  33. 33.
    Quisquater, J.-J., Samyde, D.: ElectroMagnetic analysis (EMA): measures and counter-measures for smart cards. In: Attali, I., Jensen, T. (eds.) E-smart 2001. LNCS, vol. 2140, pp. 200–210. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45418-7_17CrossRefGoogle Scholar
  34. 34.
    Reparaz, O.: Detecting flawed masking schemes with leakage detection tests. In: Peyrin, T. (ed.) FSE 2016. LNCS, vol. 9783, pp. 204–222. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-52993-5_11CrossRefGoogle Scholar
  35. 35.
    Reparaz, O., Bilgin, B., Nikova, S., Gierlichs, B., Verbauwhede, I.: Consolidating masking schemes. In: Gennaro, R., Robshaw, M. (eds.) CRYPTO 2015. LNCS, vol. 9215, pp. 764–783. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-47989-6_37CrossRefGoogle Scholar
  36. 36.
    Rivain, M., Prouff, E.: Provably secure higher-order masking of AES. In: Mangard, S., Standaert, F.-X. (eds.) CHES 2010. LNCS, vol. 6225, pp. 413–427. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15031-9_28CrossRefGoogle Scholar
  37. 37.
    Trichina, E.: Combinational logic design for AES subbyte transformation on masked data. IACR Cryptology ePrint Archive (2003)Google Scholar
  38. 38.
    Wolf, C., Glaser, J.: Yosys - a free verilog synthesis suite. In: Proceedings of Austrochip 2013 (2013)Google Scholar
  39. 39.
    Xiao, G., Massey, J.L.: A spectral characterization of correlation-immune combining functions. IEEE Trans. Inf. Theory 34(3), 569–571 (1988)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© International Association for Cryptologic Research 2018

Authors and Affiliations

  1. 1.Institute for Applied Information Processing and Communications (IAIK)Graz University of TechnologyGrazAustria

Personalised recommendations