Paper 2017/401

Synthesis of Adaptive Side-Channel Attacks

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


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.

Available format(s)
Publication info
Published elsewhere. Major revision. 30th IEEE Computer Security Foundations Symposium
Side-Channel AttacksQuantitative Information FlowCryptographyMulti-run SecuritySymbolic ExecutionSatisfiability Modulo TheoriesMaxSMTModel Counting
Contact author(s)
sang phan @ sv cmu edu
2017-05-11: received
Short URL
Creative Commons Attribution


      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{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.