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.

翻译：微架构侧信道的严格量化评估面临两大挑战。首先，处理器、攻击手段及防御机制常表现出概率性行为。这些概率性行为源于系统固有噪声（例如来自并发运行进程）、概率性侧信道攻击以及概率性混淆防御。其次，微处理器结构极其复杂。现有评估方法多依赖抽象或简化模型，这些模型必然比真实系统或逐周期模拟器缺乏细节，可能遗漏关键现象。虽然简单模型足以评估性能，但安全问题往往潜藏于细节之中。我们通过将统计模型检验引入微架构侧信道量化评估来应对这一挑战。SMC是一种严格的统计技术，能够处理概率性实验结果并提供统计保证，已广泛应用于高度依赖统计保证的计算领域（如医疗植入设备、车载计算）。借助SMC，我们可以将处理器视为黑箱，无需进行抽象或简化。通过三个案例研究，我们实证展示了SMC的有效性：实验表明SMC能够评估现有安全漏洞与防御机制，在保持更高统计严谨性的同时得出定性相似的结论，且无需任何简化假设或抽象处理。我们还证明SMC可使防御者量化所需噪声强度，以特定置信水平确保攻击者成功率低于预期阈值，从而为通过噪声注入实施混淆防御提供可操作的实施方案。