Cryptology ePrint Archive: Report 2017/401

Synthesis of Adaptive Side-Channel Attacks

Quoc-Sang Phan and Lucas Bang and Corina S. Păsăreanu and 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.

Category / Keywords: implementation / Side-Channel Attacks; Quantitative Information Flow; Cryptography; Multi-run Security; Symbolic Execution; Satisfiability Modulo Theories; MaxSMT; Model Counting

Original Publication (with major differences): 30th IEEE Computer Security Foundations Symposium

Date: received 9 May 2017

Contact author: sang phan at sv cmu edu

Available format(s): PDF | BibTeX Citation

Version: 20170511:023443 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]