SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

This program is tentative and subject to change.

Sat 18 Oct 2025 17:00 - 17:15 at Orchid Small - TOPLAS and Remote

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 Oct

Displayed time zone: Perth change

16:00 - 17:30
TOPLAS and RemoteOOPSLA at Orchid Small
16:00
15m
Talk
(TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs
OOPSLA
Xusheng Zhi , Thomas Reps University of Wisconsin-Madison
DOI
16:15
15m
Talk
(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
15m
Talk
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
15m
Talk
Modal Abstractions for Virtualizing Memory Addresses
OOPSLA
Ismail Kuru Drexel University, Colin Gordon Drexel University
17:00
15m
Talk
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
15m
Talk
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