今天为大家推荐的论文是由XiaoFeng Wang研究组完成并投稿的，来自USENIX Security 2023的A Verified Confidential Computing as a Service Framework for Privacy Preservation，该工作将在美西时间今天下午为大家带来进一步讲解呀~

这篇论文 A Verified Confidential Computing as a Service Framework for Privacy Preservation 来自 Usenix Security 2023，将在本周的会议上出现。这篇论文介绍了一个经过验证的机密计算框架，可以在云端部署提供隐私保护。

背景

虽然硬件TEE（Trusted Execution Environment，可信执行环境）做到了远程证明（Remote Attestation），强隔离，以及加密，但单纯地使用TEE仍然无法确保隐私保护，更不能向用户(data provider)“证明”隐私得到了保护。远程证明只能保证运行的代码符合预期，却无法证明代码符合安全属性。隔离能够有效阻止外部的攻击者，但是无法阻止来自内部的数据泄漏。加密可以保证数据的机密性， 然而不能确保敏感数据被完全擦除。现在较为流行的CCaaS（Confidential Computing as a Service, 机密计算即为服务）框架如下：

在这一框架下，CCaaS可以接受第三方开发者提交的任务。用户（data provider）首先向CCaaS提交数据，CCaaS接下来完成“解密-执行任务-加密”的流程，最后将输出返回给用户。

本文的目标是向用户证明enclave里运行的代码确实能够保护隐私，防止隐私数据的泄漏和残留。

形式化模型

作者提出了一个安全准则：Proof of Being Forgotten (PoBF)，即证明数据被遗忘。
其包含两个要求：No Leakage 和 No Residue。前者要求所有的敏感数据和被敏感数据污染(taint)的数据都不会泄漏，后者要求所有的敏感数据都会被擦除。首先，本文用Coq建立了一个基于Imp语言的形式化模型，这个模型描述了抽象的enclave以及在enclave里运行的程序。

它对于不同的TEE是普适的。注意这里有一个Zone的概念，类似于传统的沙箱，所有的敏感数据都应该在Zone内被处理。

基于这个模型，作者证明了两个定理，分别是在何种情况下能够满足上述的No Leakage 和 No Residue要求。前者主要是通过限制敏感数据只能在Zone内写入，后者则是通过在函数结束的时候擦除（zero-out）Zone内的所有的敏感数据来满足。

设计和实现

本文设计了一个系统：PoBF-Compliant Framework (PoCF)。

其所提供的Artifact主要包括三个部分：通用的CCaaS库(PoCF Library)，TEE平台具体的enclave(PoCF Enclave)，以及一个在用户端运行的验证程序(PoCF Verifier)。为了达到上述的要求，首先需要确保工作流的完整性。作者设计了一个状态机来规定每一个CCaaS作业的状态转换入下图所示：

借助Rust的强类型，作者通过Rust的类型系统实现了这个状态机，这也是PoCF Library的核心部分。这部分的实现通过Prusti得以形式化验证。

No Resiude

根据形式化模型中得到的定理，本文引入了Zerorize trait，来实现在函数结束时对Zone内的敏感数据进行擦除的机制。对于在堆上分配的数据，作者们修改了内存分配器，使得在释放内存时能够对Zone内的数据进行擦除。对于在栈上和寄存器上的数据，作者们通过插桩以及Zerorize trait来确保擦除。此外，PoCF不允许有可写入的全局变量。

No Leakage

类似地，根据形式化模型中的定理，本文设计了一套数据流追踪 (data flow tracking) 机制。密钥不会被暴露给第三方提交的任务，然而数据会。密钥的追踪基于状态机。作者们使用MIRAI的抽象解释（abstract interpretation）来实现数据流追踪。

评估

PoCF的设计和实现满足了PoBF的要求。在计算为主的任务上，PoCF基本没有引入额外开销。然而在IO为主的任务上，由于缺少优化，PoCF的开销较大。此外，MIRAI的抽象解释的准确性在某些情况下也会有问题。

PoCF代码开源：https://github.com/ya0guang/PoBF
论文下载：https://hiroki-chen.github.io/papers/PoBF_USENIX_SEC_2023.pdf