基于统计模型检验的微架构侧信道严格评估
Rigorous Evaluation of Microarchitectural Side-Channels with Statistical Model Checking
AI总结：
针对微架构侧信道定量评估受概率行为、处理器复杂度限制的难题，引入统计模型检验SMC技术，以黑盒方式无需简化模型即可完成严谨评估，还能为噪声注入混淆防御提供量化方案。
摘要：
对微架构侧信道进行严格的定量评估颇具挑战性，原因有二。其一，处理器、攻击手段与防御机制通常表现出概率行为。这类概率行为源于系统中的固有噪声（例如来自并行运行进程的噪声）、概率侧信道攻击以及概率混淆防御机制。其二，微处理器的结构极为复杂。以往的评估方法依赖抽象或简化模型，其细节精细度必然不及真实系统或逐周期模拟器，且这类模型可能遗漏重要现象。尽管简单模型或许足以估算性能，但安全问题往往体现在细节之中。\n我们通过将统计模型检验（Statistical Model Checking，SMC）引入微架构侧信道的定量评估，来应对这一挑战。SMC是一种严谨的统计技术，能够处理概率实验的结果并提供统计保证，已被应用于高度依赖统计保证的计算场景（例如医疗植入物、车载计算）。借助SMC，我们可将处理器视为黑盒，无需对其进行抽象或简化处理。我们通过三个案例研究验证了SMC的有效性，实验结果表明：SMC能够评估现有的安全漏洞与防御机制，在不做任何简化假设或抽象的前提下，得出定性相似但统计严谨性更高的结论。我们还证明，SMC可帮助防御者量化所需的噪声量级，使其有信心将攻击者的成功概率降至低于预设阈值，从而为防御者提供通过噪声注入实现混淆的可执行方案。
英文摘要：
Rigorous quantitative evaluation of microarchitectural side channels is challenging for two reasons. First, the processors, attacks, and defenses often exhibit probabilistic behaviors. These probabilistic behaviors arise due to natural noise in systems (e.g., from co-running processes), probabilistic side channel attacks, and probabilistic obfuscation defenses. Second, microprocessors are extremely complex. Previous evaluation methods have relied on abstract or simplified models, which are necessarily less detailed than real systems or cycle-by-cycle simulators, and these models may miss important phenomena. Whereas a simple model may suffice for estimating performance, security issues frequently manifest in the details. We address this challenge by introducing Statistical Model Checking (SMC) to the quantitative evaluation of microarchitectural side channels. SMC is a rigorous statistical technique that can process the results of probabilistic experiments and provide statistical guarantees, and it has been used in computing applications that depend heavily on statistical guarantees (e.g., medical implants, vehicular computing). With SMC, we can treat processors as opaque boxes, and we do not have to abstract or simplify them. We demonstrate the effectiveness of SMC through three case studies, in which we experimentally show that SMC can evaluate existing security vulnerabilities and defenses and provide qualitatively similar conclusions with greater statistical rigor, while making no simplifying assumptions or abstractions. We also show that SMC can enable a defender to quantify the amount of noise necessary to have a desired level of confidence that she has reduced an attacker's probability of success to less than a desired threshold, thus providing the defender with an actionable plan for obfuscation via noise injection.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
