Agora: Trust Less and Open More in Verification for Confidential Computing
This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Sat 18 OctDisplayed time zone: Perth change
16:00 - 17:30 | |||
16:00 15mTalk | (TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs OOPSLA DOI | ||
16:15 15mTalk | (TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging OOPSLA Yaozhu Sun National Institute of Informatics, Xuejing Huang IRIF, Bruno C. d. S. Oliveira University of Hong Kong | ||
16:30 15mTalk | Detecting and explaining (in-)equivalence of context-free grammars OOPSLA Marko Schmellenkamp Ruhr University Bochum, Thomas Zeume Ruhr University Bochum, Sven Argo Ruhr University Bochum, Sandra Kiefer University of Oxford, Cedric Siems Ruhr University Bochum, Fynn Stebel Ruhr University Bochum | ||
16:45 15mTalk | Modal Abstractions for Virtualizing Memory Addresses OOPSLA | ||
17:00 15mTalk | Agora: Trust Less and Open More in Verification for Confidential Computing OOPSLA Hongbo Chen Indiana University Bloomington, Quan Zhou Penn State University, Sen Yang Yale University, Dang Sixuan Duke University, Xing Han The Hong Kong University of Science and Technology, Danfeng Zhang Duke University, Fan Zhang Yale University, XiaoFeng Wang Nanyang Technological University | ||
17:15 15mTalk | QED in Context: An Observation Study of Proof Assistant Users OOPSLA Jessica Shi University of Pennsylvania, Cassia Torczon University of Pennsylvania, Harrison Goldstein University at Buffalo, the State University of New York at Buffalo, Benjamin C. Pierce University of Pennsylvania, Andrew Head University of Pennsylvania |