Paper 2017/401

Synthesis of Adaptive Side-Channel Attacks

Quoc-Sang Phan, Lucas Bang, Corina S. Păsăreanu, Pasquale Malacaria, and Tevfik Bultan

Abstract

We present symbolic analysis techniques for detecting vulnerabilities that are due to adaptive side-channel attacks, and synthesizing inputs that exploit the identified vulnerabilities. We start with a symbolic attack model that encodes succinctly all the side-channel attacks that an adversary can make. Using symbolic execution over this model, we generate a set of mathematical constraints, where each constraint characterizes the set of secret values that lead to the same sequence of side-channel measurements. We then compute the optimal attack, i.e, the attack that yields maximum leakage over the secret, by solving an optimization problem over the computed constraints. We use information-theoretic concepts such as channel capacity and Shannon entropy to quantify the leakage over multiple runs in the attack, where the measurements over the side channels form the observations that an adversary can use to try to infer the secret. We also propose greedy heuristics that generate the attack by exploring a portion of the symbolic attack model in each step. We implemented the techniques in Symbolic PathFinder and applied them to Java programs encoding web services, string manipulations and cryptographic functions, demonstrating how to synthesize optimal side-channel attacks.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Published elsewhere. Major revision. 30th IEEE Computer Security Foundations Symposium
Keywords
Side-Channel AttacksQuantitative Information FlowCryptographyMulti-run SecuritySymbolic ExecutionSatisfiability Modulo TheoriesMaxSMTModel Counting
Contact author(s)
sang phan @ sv cmu edu
History
2017-05-11: received
Short URL
https://ia.cr/2017/401
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2017/401,
      author = {Quoc-Sang Phan and Lucas Bang and Corina S.  Păsăreanu and Pasquale Malacaria and Tevfik Bultan},
      title = {Synthesis of Adaptive Side-Channel Attacks},
      howpublished = {Cryptology ePrint Archive, Paper 2017/401},
      year = {2017},
      note = {\url{https://eprint.iacr.org/2017/401}},
      url = {https://eprint.iacr.org/2017/401}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.