Multi-run Side-Channel Analysis Using Symbolic Execution and Max-SMT
Multi-run Side-Channel Analysis Using Symbolic Execution and Max-SMT
复制标题
DOI：
10.1109/csf.2016.34
复制
发表时间：
2016-08
期刊：
影响因子：
--
通讯作者：
C. Păsăreanu;Quoc-Sang Phan;P. Malacaria
中科院分区：
文献类型：
--
作者：
C. Păsăreanu;Quoc-Sang Phan;P. Malacaria
侧信道攻击从计算的非功能特征（如时间或内存消耗）中恢复机密信息。我们描述了一个程序分析，它使用符号执行来量化泄露给攻击者的信息，攻击者进行了多个侧信道测量。该分析还综合了导致最大泄漏的具体公共输入（“攻击”），通过对符号执行收集的约束进行新颖的Max-SMT还原。此外，利用模型计数和信息论度量来计算攻击者在进行一定数量的侧信道测量后对秘密的剩余不确定性。我们在Symbolic PathFinder工具中实现了分析，并将其应用于密码检查和加密函数的环境中，展示了如何在少量攻击步骤下获得信息泄漏的紧密边界。
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.