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}
}