论文标题
可证明安全的隔离,用于在小微处理器上可中断的环境执行:扩展版本
Provably Secure Isolation for Interruptible Enclaved Execution on Small Microprocessors: Extended Version
论文作者
论文摘要
计算机系统通常为隔离机制提供硬件支持,例如特权级别,虚拟内存或乡村执行。在过去的几年中,已经开发出了一些成功的基于软件的侧通道攻击,它们破裂了,或者至少显着削弱了这些机制所提供的隔离。扩展具有新的建筑或微构造特征的处理器,带来了引入新的此类侧向通道攻击的风险。 本文研究了扩展具有新功能的处理器的问题,而不会削弱处理器提供的隔离机制的安全性。我们建议将完全抽象作为处理器扩展安全性的正式标准,并将该标准实例化,以扩展微处理器的具体案例,该案例扩展了支持封闭执行的微处理器,并具有这些飞地的安全中断性。这是一个非常相关的实例化,因为最近的几篇论文表明,飞地的中断性会导致各种基于软件的侧向通道攻击。我们为可中断的飞地提供了设计,并证明它满足我们的安全标准。我们还在开源飞地的微处理器上实现了设计,并在性能和硬件尺寸方面评估了我们的设计成本。
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.