一句话：提出以完全抽象作为处理器扩展安全性的形式化准则，设计、证明并实现可中断 enclave，评估其性能与硬件开销。
硬件隔离机制（如特权级、虚拟内存和 enclave 执行）常遭受软件侧信道攻击，而为处理器添加新架构或微架构特性可能进一步削弱隔离并引入新侧信道。本文研究在扩展处理器时不破坏隔离机制安全性的问题。作者从程序语言研究中引入完全抽象（full abstraction）概念，将其作为处理器扩展安全性的一般形式化准则，并实例化到支持 enclave 执行的小型微处理器上，用于安全可中断 enclave 的设计。文章提出一种可中断 enclave 设计，证明其满足该安全准则，并在一个开源且支持 enclave 的微处理器上实现，从性能和硬件面积两方面评估开销。该工作表明可在不削弱隔离安全性的前提下支持 enclave 中断。
Computer systems often provide hardware support for isolation mechanisms such as 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 software-based side-channel attacks. This article studies the problem of extending a processor with new features without weakening the security of the isolation mechanisms that the processor offers. Our solution is heavily based on techniques from research on programming languages. More specifically, we propose to use the programming language concept of full abstraction as a general formal criterion for the security of a processor extension. We instantiate the proposed criterion to the concrete case of extending a microprocessor that supports enclaved execution with secure interruptibility. 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.
@article{paperbot1215,
title = {Securing Interruptible Enclaved Execution on Small Microprocessors},
author = {Matteo Busi and Job Noorman and Jo Van Bulck and Letterio Galletta and Pierpaolo Degano and Jan Tobias Mühlberg and Frank Piessens},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {43},
number = {3},
year = {2021},
doi = {10.1145/3470534}
}