Compositional Synthesis of Leakage Resilient Programs
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. . In a recent work , 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.
KeywordsCompositionality Property Prototype Implementation Satisfying Assignment Synthesis Algorithm Public Input
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.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
- 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
- 5.Blot, A., Yamamoto, M., Terauchi, T.: Compositional synthesis of leakage resilient programs. CoRR, abs/1610.05603 (2016)Google Scholar
- 13.Goldwasser, S., Rothblum, G.N.: How to compute in the presence of leakage. In: FOCS 2012, pp. 31–40 (2012)Google Scholar
- 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
- 19.Malacaria, P.: Assessing security threats of looping constructs. In: POPL 2007, pp. 225–235 (2007)Google Scholar
- 24.Yasuoka, H., Terauchi, T.: Quantitative information flow - verification hardness and possibilities. In: CSF 2010, pp. 15–27 (2010)Google Scholar