Provably Secure Isolation for Interruptible Enclaved Execution on Small Microprocessors
Provably Secure Isolation for Interruptible Enclaved Execution on Small Microprocessors
复制标题
小型微处理器上可中断封闭执行的可证明安全隔离
DOI：
10.1109/csf49147.2020.00026
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Frank Piessens
中科院分区：
文献类型：
--
作者：
Matteo Busi;Job Noorman;Jo Van Bulck;Letterio Galletta;P. Degano;Jan Tobias Muhlberg;Frank Piessens
计算机系统通常为隔离机制（如特权级别、虚拟内存或飞地执行）提供硬件支持。在过去的几年中，已经开发出几种成功的基于软件的旁道攻击，这些攻击破坏或至少显着削弱了这些机制提供的隔离性。使用新的架构或微架构功能扩展处理器会带来引入新的此类侧信道攻击的风险。本文研究了在不削弱处理器提供的隔离机制的安全性的情况下扩展处理器新功能的问题。我们建议使用完全抽象作为处理器扩展安全性的正式标准，并将该标准实例化为扩展微处理器的具体情况，该微处理器支持飞地执行以及这些飞地的安全中断性。这是一个非常相关的实例，因为最近的几篇论文表明，飞地的可中断性会导致各种基于软件的旁道攻击。我们提出了可中断飞地的设计，并证明它满足我们的安全标准。我们还在启用 enclave 的开源微处理器上实现了该设计，并根据性能和硬件尺寸评估了我们设计的成本。
Computer systems often provide hardware support for isolation mechanisms like privilege levels, virtual memory, or enclaved execution. Over the past years, several successful software-based side-channel attacks have been developed that break, or at least significantly weaken the isolation that these mechanisms offer. Extending a processor with new architectural or micro-architectural features, brings a risk of introducing new such side-channel attacks. This paper studies the problem of extending a processor with new features without weakening the security of the isolation mechanisms that the processor offers. We propose to use full abstraction as a formal criterion for the security of a processor extension, and we instantiate that criterion to the concrete case of extending a microprocessor that supports enclaved execution with secure interruptibility of these enclaves. This is a very relevant instantiation as several recent papers have shown that interruptibility of enclaves leads to a variety of software-based side-channel attacks. We propose a design for interruptible enclaves, and prove that it satisfies our security criterion. We also implement the design on an open-source enclave-enabled microprocessor, and evaluate the cost of our design in terms of performance and hardware size.