Compositional Synthesis of Leakage Resilient Programs

  • Arthur Blot
  • Masaki Yamamoto
  • Tachio TerauchiEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10204)


A promising approach to defend against side channel attacks is to build programs that are leakage resilient, in a formal sense. One such formal notion of leakage resilience is the n-threshold-probing model proposed in the seminal work by Ishai et al. [16]. In a recent work [9], Eldib and Wang have proposed a method for automatically synthesizing programs that are leakage resilient according to this model, for the case \(n=1\). In this paper, we show that the n-threshold-probing model of leakage resilience enjoys a certain compositionality property that can be exploited for synthesis. We use the property to design a synthesis method that efficiently synthesizes leakage-resilient programs in a compositional manner, for the general case of \(n > 1\). We have implemented a prototype of the synthesis algorithm, and we demonstrate its effectiveness by synthesizing leakage-resilient versions of benchmarks taken from the literature.


Compositionality Property Prototype Implementation Satisfying Assignment Synthesis Algorithm Public Input 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



We thank the anonymous reviewers for useful comments. This work was supported by MEXT Kakenhi 26330082 and 25280023, and JSPS Core-to-Core Program, A.Advanced Research Networks.


  1. 1.
    Alvim, M.S., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: CSF 2012, pp. 265–279 (2012)Google Scholar
  2. 2.
    Balasch, J., Faust, S., Gierlichs, B., Verbauwhede, I.: Theory and practice of a leakage resilient masking scheme. In: Wang, X., Sako, K. (eds.) ASIACRYPT 2012. LNCS, vol. 7658, pp. 758–775. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-34961-4_45 CrossRefGoogle Scholar
  3. 3.
    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
  4. 4.
    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). doi: 10.1007/978-3-662-46800-5_18 Google Scholar
  5. 5.
    Blot, A., Yamamoto, M., Terauchi, T.: Compositional synthesis of leakage resilient programs. CoRR, abs/1610.05603 (2016)Google Scholar
  6. 6.
    Coron, J.-S., Prouff, E., Rivain, M., Roche, T.: Higher-order side channel security and mask refreshing. In: Moriai, S. (ed.) FSE 2013. LNCS, vol. 8424, pp. 410–424. Springer, Heidelberg (2014). doi: 10.1007/978-3-662-43933-3_21 Google Scholar
  7. 7.
    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). doi: 10.1007/978-3-540-78800-3_24 CrossRefGoogle Scholar
  8. 8.
    Duc, A., Dziembowski, S., Faust, S.: Unifying leakage models: from probing attacks to noisy leakage. In: Nguyen, P.Q., Oswald, E. (eds.) EUROCRYPT 2014. LNCS, vol. 8441, pp. 423–440. Springer, Heidelberg (2014). doi: 10.1007/978-3-642-55220-5_24 CrossRefGoogle Scholar
  9. 9.
    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). doi: 10.1007/978-3-319-08867-9_8 Google Scholar
  10. 10.
    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). doi: 10.1007/978-3-642-54862-8_5 CrossRefGoogle Scholar
  11. 11.
    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). doi: 10.1007/978-3-642-13190-5_7 CrossRefGoogle Scholar
  12. 12.
    Goldwasser, S., Rothblum, G.N.: Securing computation against continuous leakage. In: Rabin, T. (ed.) CRYPTO 2010. LNCS, vol. 6223, pp. 59–79. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-14623-7_4 CrossRefGoogle Scholar
  13. 13.
    Goldwasser, S., Rothblum, G.N.: How to compute in the presence of leakage. In: FOCS 2012, pp. 31–40 (2012)Google Scholar
  14. 14.
    Gray III, J.W.: Toward a mathematical foundation for information flow security. In: 1999 IEEE Symposium on Security and Privacy, pp. 21–35 (1991)Google Scholar
  15. 15.
    Ishai, Y., Prabhakaran, M., Sahai, A., Wagner, D.: Private circuits II: keeping secrets in tamperable circuits. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol. 4004, pp. 308–327. Springer, Heidelberg (2006). doi: 10.1007/11761679_19 CrossRefGoogle Scholar
  16. 16.
    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). doi: 10.1007/978-3-540-45146-4_27 CrossRefGoogle Scholar
  17. 17.
    Köpf, B., Basin, D.A.: Automatically deriving information-theoretic bounds for adaptive side-channel attacks. J. Comput. Secur. 19(1), 1–31 (2011)CrossRefGoogle Scholar
  18. 18.
    Köpf, B., Mauborgne, L., Ochoa, M.: Automatic quantification of cache side-channels. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 564–580. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-31424-7_40 CrossRefGoogle Scholar
  19. 19.
    Malacaria, P.: Assessing security threats of looping constructs. In: POPL 2007, pp. 225–235 (2007)Google Scholar
  20. 20.
    Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213–228. Springer, Heidelberg (2002). doi: 10.1007/3-540-45937-5_16 CrossRefGoogle Scholar
  21. 21.
    Prouff, E., Rivain, M.: Masking against side-channel attacks: a formal security proof. In: Johansson, T., Nguyen, P.Q. (eds.) EUROCRYPT 2013. LNCS, vol. 7881, pp. 142–159. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-38348-9_9 CrossRefGoogle Scholar
  22. 22.
    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). doi: 10.1007/978-3-642-15031-9_28 CrossRefGoogle Scholar
  23. 23.
    Smith, G.: On the foundations of quantitative information flow. In: Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 288–302. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-00596-1_21 CrossRefGoogle Scholar
  24. 24.
    Yasuoka, H., Terauchi, T.: Quantitative information flow - verification hardness and possibilities. In: CSF 2010, pp. 15–27 (2010)Google Scholar

Copyright information

© Springer-Verlag GmbH Germany 2017

Authors and Affiliations

  1. 1.ENS LyonLyonFrance
  2. 2.Nagoya UniversityNagoyaJapan
  3. 3.JAISTNomiJapan

Personalised recommendations