Compositional synthesis of leakage resilient programs

Arthur Blot, Masaki Yamamoto, Tachio Terauchi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

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. [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.

Original languageEnglish
Title of host publicationPrinciples of Security and Trust - 6th International Conference, POST 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
PublisherSpringer Verlag
Pages277-297
Number of pages21
Volume10204 LNCS
ISBN (Print)9783662544549
DOIs
Publication statusPublished - 2017
Externally publishedYes
Event6th Conference on Principles of Security and Trust, POST 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017 - Uppsala, Sweden
Duration: 2017 Apr 222017 Apr 29

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10204 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other6th Conference on Principles of Security and Trust, POST 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
CountrySweden
CityUppsala
Period17/4/2217/4/29

Fingerprint

Leakage
Synthesis
Threshold Model
Resilience
Compositionality
Side Channel Attacks
Prototype
Benchmark
Demonstrate
Side channel attack

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Blot, A., Yamamoto, M., & Terauchi, T. (2017). Compositional synthesis of leakage resilient programs. In Principles of Security and Trust - 6th International Conference, POST 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings (Vol. 10204 LNCS, pp. 277-297). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10204 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-662-54455-6_13

Compositional synthesis of leakage resilient programs. / Blot, Arthur; Yamamoto, Masaki; Terauchi, Tachio.

Principles of Security and Trust - 6th International Conference, POST 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings. Vol. 10204 LNCS Springer Verlag, 2017. p. 277-297 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10204 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Blot, A, Yamamoto, M & Terauchi, T 2017, Compositional synthesis of leakage resilient programs. in Principles of Security and Trust - 6th International Conference, POST 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings. vol. 10204 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10204 LNCS, Springer Verlag, pp. 277-297, 6th Conference on Principles of Security and Trust, POST 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, 17/4/22. https://doi.org/10.1007/978-3-662-54455-6_13
Blot A, Yamamoto M, Terauchi T. Compositional synthesis of leakage resilient programs. In Principles of Security and Trust - 6th International Conference, POST 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings. Vol. 10204 LNCS. Springer Verlag. 2017. p. 277-297. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-54455-6_13
Blot, Arthur ; Yamamoto, Masaki ; Terauchi, Tachio. / Compositional synthesis of leakage resilient programs. Principles of Security and Trust - 6th International Conference, POST 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings. Vol. 10204 LNCS Springer Verlag, 2017. pp. 277-297 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{9f4d6a0505544ce8b6a213e39939ac48,
title = "Compositional synthesis of leakage resilient programs",
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. [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.",
author = "Arthur Blot and Masaki Yamamoto and Tachio Terauchi",
year = "2017",
doi = "10.1007/978-3-662-54455-6_13",
language = "English",
isbn = "9783662544549",
volume = "10204 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "277--297",
booktitle = "Principles of Security and Trust - 6th International Conference, POST 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Compositional synthesis of leakage resilient programs

AU - Blot, Arthur

AU - Yamamoto, Masaki

AU - Terauchi, Tachio

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85018636405&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85018636405&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-54455-6_13

DO - 10.1007/978-3-662-54455-6_13

M3 - Conference contribution

AN - SCOPUS:85018636405

SN - 9783662544549

VL - 10204 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 277

EP - 297

BT - Principles of Security and Trust - 6th International Conference, POST 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings

PB - Springer Verlag

ER -