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 15:00 - 15:15 at Orchid East - Memory

In untrusted execution environments such as web browsers, code from remote sources is regularly executed. To harden these environments against attacks, constituent programming languages and their implementations must uphold certain safety properties, such as memory safety. These properties must be maintained across the entire compilation stack, which may include intermediate languages that do not provide the same safety guarantees. Any case where properties are not preserved could lead to a serious security vulnerability.

In this work, we identify a specification vulnerability in the WebGPU Shading Language (WGSL) where code with data races can be compiled to intermediate representations in which an optimizing compiler could legitimately remove memory safety guardrails. To address this, we present SafeRace, a collection of threat assessments and specification proposals across the WGSL execution stack. While our threat assessment showed that this vulnerability does not appear to be exploitable on current systems, it creates a “ticking time bomb”, especially as compilers in this area are rapidly evolving. Given this, we introduce the SafeRace Memory Safety Guarantee (SMSG), two components that preserve memory safety in the WGSL execution stack even in the presence of data races. The first component specifies that program slices contributing to memory indexing must be race free and is implemented via a compiler pass for WGSL programs. The second component is a requirement on intermediate representations that limits the effects of data races so that they cannot impact race-free program slices. Our results show that the first component can be implemented with negligible performance overhead on important WebGPU applications, including browser AI implementations. Next, we test the second component by performing a fuzzing campaign of 81 hours across 21 compilation stacks; our results show violations on only one machine, thus providing evidence that lower-level GPU frameworks could relatively straightforwardly support this constraint. Finally, our assessments discovered GPU memory isolation vulnerabilities in Apple and AMD GPUs, as well as a security-critical miscompilation of WGSL in a pre-release version of Firefox.

This program is tentative and subject to change.

Sat 18 Oct

Displayed time zone: Perth change

13:45 - 15:30
13:45
15m
Talk
Compositional Symbolic Execution for the Next 700 Memory Models
OOPSLA
Andreas Lööw Imperial College London, Seung Hoon Park Imperial College London, Daniele Nantes-Sobrinho Imperial College London, Sacha-Élie Ayoun Imperial College London, Opale Sjöstedt Imperial College London, Philippa Gardner Imperial College London
Pre-print
14:00
15m
Talk
Destination calculus: A linear λ-calculus for purely functional memory writes
OOPSLA
Thomas BAGREL Tweag, LORIA/INRIA, Arnaud Spiwack Tweag
14:15
15m
Talk
Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy Through Machine Code-Level Slowdown
OOPSLA
Humphrey Burchell University of Kent, Stefan Marr University of Kent
14:30
15m
Talk
HeapBuffers: Why not just using a binary serialization format for your managed memory?
OOPSLA
Daniele Bonetta VU Amsterdam, Júnior Löff Università della Svizzera italiana, Matteo Basso Università della Svizzera italiana (USI), Walter Binder USI Lugano
14:45
15m
Talk
im2im: Automatically Converting In-Memory Image Representations using A Knowledge Graph Approach
OOPSLA
Fei Chen German Research Center for Artificial Intelligence (DFKI), Saarland University, Sunita Saha German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany, Manuela Schuler German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany; Saarland University, Saarbrücken, Germany, Philipp Slusallek DFKI, Germany, Tim Dahmen Aalen University, Aalen, Germany; German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany
15:00
15m
Talk
SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
OOPSLA
Reese Levine , Ashley Lee University of California, Santa Cruz, Neha Abbas University of California, Santa Cruz, Kyle Little University of Utah, Tyler Sorensen Microsoft Research and University of California at Santa Cruz
15:15
15m
Talk
Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
OOPSLA
Jay Richards University of Kent, Daniel Wright University of Surrey, Simon Cooksey , Mark Batty University of Kent