计算机体系结构抽象边信道模型的验证
Validation of Abstract Side-Channel Models for Computer Architectures
摘要：
观测模型通过提供边信道的抽象，使信息流特性的分析变得容易处理。我们介绍了一种方法和工具，Scam-V，以验证现代计算机体系结构的观测模型。我们结合符号执行，关系分析，和不同的程序生成技术来生成实验和验证模型。实验由一个随机生成的程序和两个输入组成，根据测试模型，这两个输入在观测上是等价的。验证是通过执行程序和分析侧通道来检查两个输入在实际硬件上的不可重复性来完成的。我们通过验证模型来评估我们的框架，这些模型抽象了Raspberry Pi 3板的数据缓存侧通道，该板具有实现ARMv 8-A架构的处理器。我们的研究结果表明，Scam-V可以识别模型实现中的错误，并生成测试程序，由于隐藏的微体系结构行为使模型无效。
英文摘要：
Observational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware by executing the program and analyzing the side channel. We have evaluated our framework by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture. Our results show that Scam-V can identify bugs in the implementation of the models and generate test programs which invalidate the models due to hidden microarchitectural behavior.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
