Cerberus：一种安全高效 enclave 内存共享的形式化方法

硬件 enclave 依赖于不相交内存模型，该模型将每个物理地址映射到一个 enclave 以实现强内存隔离。然而，这严重限制了 enclave 程序的性能和可编程性。尽管一些先前工作提出了 enclave 内存共享，但其并未提供对其设计的形式化模型或验证。本文提出 Cerberus，一种安全高效 enclave 内存共享的形式化方法。为减轻形式化验证的负担，我们比较了不同的共享模型并选择了一个简单而强大的共享模型。基于该共享模型，Cerberus 扩展了一个 enclave 平台，使得 enclave 内存可通过附加操作变为不可变且可在多个 enclave 之间共享。我们使用增量验证，从称为可信抽象平台（Trusted Abstract Platform，TAP）的现有形式化模型开始。利用我们扩展的 TAP 模型，我们形式化验证了尽管允许内存共享，Cerberus 不会破坏或削弱 enclave 的安全保证。更具体地，我们在我们的形式化模型上证明了安全远程执行（Secure Remote Execution，SRE）属性。最后，本文通过在现有 enclave 平台 RISC-V Keystone 中实现 Cerberus 展示了其可行性。