Multi-run Side-Channel Analysis Using Symbolic Execution and Max-SMT

Citations Over TimeTop 1% of 2016 papers

Abstract

Side-channel attacks recover confidential information from non-functional characteristics of computations, such as time or memory consumption. We describe a program analysis that uses symbolic execution to quantify the information that is leaked to an attacker who makes multiple side-channel measurements. The analysis also synthesizes the concrete public inputs (the "attack") that lead to maximum leakage, via a novel reduction to Max-SMT solving over the constraints collected with symbolic execution. Furthermore model counting and information-theoretic metrics are used to compute an attacker's remaining uncertainty about a secret after a certain number of side-channel measurements are made. We have implemented the analysis in the Symbolic PathFinder tool and applied it in the context of password checking and cryptographic functions, showing how to obtain tight bounds on information leakage under a small number of attack steps.

Related Papers

• → Side Channel Attacks(2011)20 cited
• → The Auspicious Couple: Symbolic Execution and WCET Analysis(2013)12 cited
• → Protecting cryptographic integrated circuits with side-channel information(2017)5 cited
• → Analysis and countermeasures to side-channel attacks: a hardware design perspective(2019)2 cited
• → Symbolic Execution of Network Software Based on Unit Testing(2014)