Compositional Synthesis of Leakage Resilient Programs

DOI10.1007/978-3-662-54455-6_13MaRDI QIDQ3304821zbMATH OpenOpenAlexFDO

Authors Arthur Blot, Masaki Yamamoto, Tachio Terauchi

Publication date 3 August 2020

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1610.05603

zbMATH Keywords

compositionality propertyprototype implementationpublic inputsatisfying assignmentsynthesis algorithm

Mathematics Subject Classification ID

Computer security (68M25) Theory of software (68N99)

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.

Recommendations

• Synthesis of masking countermeasures against side channel attacks
• Leakage-resilient circuits without computational assumptions
• How to securely compute with noisy leakage in quasilinear complexity
• Protecting circuits from computationally bounded and noisy leakage
• Securing computation against continuous leakage

Cites work

• Advances in Cryptology - CRYPTO 2003
• Assessing security threats of looping constructs
• Higher-order side channel security and mask refreshing
• scientific article; zbMATH DE number 2087570 (Why is no real title available?)
• Masking against Side-Channel Attacks: A Formal Security Proof
• On the Foundations of Quantitative Information Flow
• Private Circuits II: Keeping Secrets in Tamperable Circuits
• Protecting Circuits from Leakage: the Computationally-Bounded and Noisy Cases
• Provably secure higher-order masking of AES
• Securing computation against continuous leakage
• Synthesis of masking countermeasures against side channel attacks
• Theory and practice of a leakage resilient masking scheme
• Unifying leakage models: from probing attacks to noisy leakage.
• Verified Proofs of Higher-Order Masking

Cited in

(1)

• Synthesis of masking countermeasures against side channel attacks

Describes a project that uses

Uses Software

• z3
• CIL

This page was built for publication: Compositional Synthesis of Leakage Resilient Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3304821)