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 16:30 - 16:45 at Orchid Plenary Ballroom - Rust

Fine-grained information flow control (IFC) ensures confidentiality and integrity at the programming language level by ensuring that high-secrecy values do not affect low-secrecy values and that low-integrity values do not affect high-integrity values. However, prior support for fine-grained IFC is impractical: It either analyzes programs using whole-program static analysis, detecting false IFC violations; or it extends the language and compiler, thwarting adoption. Recent work called Cocoon demonstrates how to provide fine-grained IFC for Rust programs without modifying the language or compiler, but it is limited to static secrecy labels, and its case studies are limited. This paper introduces an approach called Carapace that employs Cocoon’s core approach and supports both static and dynamic IFC and supports both secrecy and integrity. We demonstrate Carapace using three case studies involving real applications and comprehensive security policies. An evaluation shows that applications can be retrofitted to use Carapace with relatively few changes, while incurring negligible run-time overhead in most cases. Carapace advances the state of the art by being the the first hybrid static–dynamic IFC that works with an off-the-shelf language—Rust—and its unmodified compiler.

This program is tentative and subject to change.

Sat 18 Oct

Displayed time zone: Perth change

16:00 - 17:30
16:00
15m
Talk
A Refinement Methodology for Distributed Programs in Rust
OOPSLA
Aurel Bílý ETH Zurich, João Pereira ETH Zurich, Peter Müller ETH Zurich
16:15
15m
Talk
AutoVerus: Automated Proof Generation for Rust Code
OOPSLA
Chenyuan Yang University of Illinois Urbana-Champaign, Xuheng Li Columbia University, Md Rakib Hossain Misu University of California Irvine, Jianan Yao University of Toronto, Weidong Cui Microsoft Research, Yeyun Gong Microsoft Research, Chris Hawblitzel Microsoft Research, Shuvendu K. Lahiri Microsoft Research, Jacob R. Lorch Microsoft Research, n.n., Shuai Lu Microsoft Research, Fan Yang Microsoft Research Asia, Ziqiao Zhou Microsoft Research, Shan Lu Microsoft; University of Chicago
16:30
15m
Talk
Carapace: Static–Dynamic Information Flow Control in Rust
OOPSLA
Vincent James Beardsley , Chris Xiong Ohio State University, Ada Lamba Ohio State University, Michael D. Bond Ohio State University
16:45
15m
Talk
From Linearity to Borrowing
OOPSLA
Andrew Wagner Northeastern University, Olek Gierczak Northeastern University, Brianna Marshall Northeastern University, John Li Northeastern University, Amal Ahmed Northeastern University, USA
17:00
15m
Talk
Garbage Collection for Rust: The Finalizer Frontier
OOPSLA
Jacob Hughes King's College London, Laurence Tratt King's College London
17:15
15m
Talk
Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
OOPSLA
Zachary Grannan University of British Columbia, Aurel Bílý ETH Zurich, Jonas Fiala ETH Zürich, Jasper Geer University of British Columbia, Markus de Medeiros New York University, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia