一句话：提出 Agora 框架，通过可委托验证、区块链悬赏和开放断言语言，为机密计算构建可信且开放的验证平台。
机密计算通过远程认证保证云服务器代码完整性，但无法证明无数据泄漏等高层安全属性。本文提出 Agora，一个可信且开放的机密计算验证平台。为缩减可信计算基（TCB），Agora 将部分验证任务委托给不可信实体，仅在 TCB 内保留小型验证器，并用区块链悬赏管理器通过众包消除对复杂定理证明器的信任，从而减轻二进制分析与定理证明的 TCB 负担。为提升开放性，Agora 提供通用断言语言以验证多种安全策略，并允许不可信方参与 TCB 外流程。作者实现软件故障隔离、信息流控制和侧信道缓解策略的验证工作流，评估表明 Agora 有效。
Confidential computing (CC), designed for security-critical scenarios, uses remote attestation to guarantee code integrity on cloud servers. However, CC alone cannot provide assurance of high-level security properties (e.g., no data leak) on the code. In this paper, we introduce a novel framework, Agora , scrupulously designed to provide a trustworthy and open verification platform for CC. To prompt trustworthiness, we observe that certain verification tasks can be delegated to untrusted entities, while the corresponding (smaller) validators are securely housed within the trusted computing base (TCB). Moreover, through a novel blockchain-based bounty task manager, it also utilizes crowdsourcing to remove trust in complex theorem provers. These synergistic techniques successfully ameliorate the TCB size burden associated with two procedures: binary analysis and theorem proving. To prompt openness, Agora supports a versatile assertion language that allows verification of various security policies. Moreover, the design of Agora enables untrusted parties to participate in any complex processes out of Agora ’s TCB. By implementing verification workflows for software-based fault isolation, information flow control, and side-channel mitigation policies, our evaluation demonstrates the efficacy of Agora .
@article{paperbot2972,
title = {Agora: Trust Less and Open More in Verification for Confidential Computing},
author = {Hongbo Chen and Quan Zhou and Sen Yang and Sixuan Dang and Xing Han and Danfeng Zhang and Fan Zhang and XiaoFeng Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763099}
}