现在：在保密计算中，减少信任，更多依赖验证机制

《Proceedings of the ACM on Programming Languages》：Agora: Trust Less and Open More in Verification for Confidential Computing

可信计算框架Agora通过委托验证任务和区块链赏金机制优化TCB规模，支持多样化安全策略的断言验证，并允许非信任方参与复杂流程。

　　

摘要

保密计算（Confidential Computing, CC）专为安全关键场景设计，利用远程认证机制来保证云服务器上代码的完整性。然而，仅靠保密计算本身无法确保代码具备高级别的安全特性（例如防止数据泄露）。在本文中，我们提出了一个名为Agora的新框架，该框架经过精心设计，旨在为保密计算提供一个可信且开放的验证平台。为了提升可信度，我们发现某些验证任务可以委托给不受信任的实体，而相应的（规模较小的）验证器则安全地部署在受信任的计算基础（Trusted Computing Base, TCB）内部。此外，通过基于区块链的奖励任务管理系统，Agora还利用众包机制来降低对复杂定理证明工具的依赖。这些协同技术有效减轻了与两种流程（二进制分析和定理证明）相关的TCB规模负担。为了实现开放性，Agora支持一种通用的断言语言，能够验证多种安全策略。同时，Agora的设计允许不受信任的第三方参与TCB之外的任何复杂流程。通过实现基于软件的故障隔离、信息流控制以及侧信道防护策略的验证工作流程，我们的评估证明了Agora的有效性。