RockSalt: better, faster, stronger SFI for the x86
RockSalt: better, faster, stronger SFI for the x86
复制标题
RockSalt：针对 x86 的更好、更快、更强的 SFI
DOI：
10.1145/2254064.2254111
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Edward Gan
中科院分区：
文献类型：
--
作者：
Greg Morrisett;Gang Tan;Joseph Tassarotti;Jean;Edward Gan
Google本地客户端（NACL）中使用的基于软件的故障隔离（SFI）依赖于概念上简单的机器代码分析来执行安全策略。但是，对于X86等复杂的体系结构，很容易获得分析的细节。与Google的原始分析相比，我们已经建立了一个新的检查器，该检查器较小，更快，可信赖的计算基础却大大减少。我们方法的关键是自动从声明性描述中生成大部分分析，我们与x86指令集架构子集的正式模型相关。 COQ中开发的X86模型具有独立的兴趣，应适用于广泛的机器级验证任务。
Software-based fault isolation (SFI), as used in Google's Native Client (NaCl), relies upon a conceptually simple machine-code analysis to enforce a security policy. But for complicated architectures such as the x86, it is all too easy to get the details of the analysis wrong. We have built a new checker that is smaller, faster, and has a much reduced trusted computing base when compared to Google's original analysis. The key to our approach is automatically generating the bulk of the analysis from a declarative description which we relate to a formal model of a subset of the x86 instruction set architecture. The x86 model, developed in Coq, is of independent interest and should be usable for a wide range of machine-level verification tasks.