论文标题
验证计算机架构的抽象侧通道模型
Validation of Abstract Side-Channel Models for Computer Architectures
论文作者
论文摘要
观察模型通过提供侧通道的抽象来使信息流属性的分析。我们介绍了一种方法论和一种工具Scam-V，以验证现代计算机体系结构的观察模型。我们结合了符号执行，关系分析和不同的程序生成技术，以生成实验并验证模型。一个实验由一个随机生成的程序以及两个输入组成，根据测试的模型，它们在观察上等效。验证是通过通过执行程序并分析侧渠道来检查实际硬件上两个输入的不可区分性来完成验证。我们通过验证模型通过实现ARMV8-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.
