Compositional Synthesis of Leakage Resilient Programs

TL;DR

This paper introduces a compositional synthesis method for creating leakage-resilient programs based on the n-threshold-probing model, enabling efficient construction of secure programs for higher thresholds.

Contribution

It demonstrates the compositionality of the n-threshold-probing model and leverages this property to develop an efficient synthesis approach for general n values.

Findings

Successfully synthesized leakage-resilient programs for various benchmarks.

The method is effective and scalable for higher threshold values.

Prototype implementation confirms practical applicability.

Abstract

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.