Compositional Synthesis of Leakage Resilient Programs
This work addresses security vulnerabilities in programs for cryptography and embedded systems by providing an automated synthesis method, though it is incremental as it builds on prior work for n=1.
The paper tackles the problem of synthesizing leakage-resilient programs against side-channel attacks by exploiting a compositionality property in the n-threshold-probing model, enabling efficient synthesis for n > 1 and demonstrating effectiveness on benchmarks.
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.