SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Thu 16 Oct 2025 16:45 - 17:00 at Orchid East - Compilation 2 Chair(s): Karine Even-Mendoza

To protect security-critical applications, secure compilers have to preserve security policies, such as non-interference, during compilation. The preservation of security policies goes beyond the classical notion of compiler correctness which only enforces the preservation of the semantics of the source program. Therefore, several standard compiler optimisations are prone to break standard security policies like non-interference. Existing approaches to secure compilation are very restrictive with respect to the compiler optimisations that they permit or to the security policies they support because of conceptual limitations in their formal setup. In this paper, we present \emph{hyperproperty simulations}, a novel framework to secure compilation that models the preservation of arbitrary $k$-hyperproperties during compilation and overcomes several limitations of existing approaches, in particular it is more expressive and more flexible. We demonstrate this by designing and proving a generic non-interference preserving code transformation that can be applied on different optimisations and leakage models. This approach reduces the proof burden per optimisation to a minimum. We instantiate this code transformation on different leakage models with various standard compiler optimisations that could be handled in a very limited and less modular way (if at all) by existing approaches. Our results are formally verified in the Rocq theorem prover.

Thu 16 Oct

Displayed time zone: Perth change

16:00 - 17:30
Compilation 2OOPSLA at Orchid East
Chair(s): Karine Even-Mendoza King’s College London
16:00
15m
Talk
An Empirical Study of Bugs in the rustc Compiler
OOPSLA
Zixi Liu Nanjing University, Yang Feng Nanjing University, Yunbo Ni The Chinese University of Hong Kong, Shaohua Li The Chinese University of Hong Kong, Xizhe Yin Nanjing University, Qingkai Shi Nanjing University, Baowen Xu Nanjing University, Zhendong Su ETH Zurich
16:15
15m
Talk
DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
OOPSLA
Chenyao Suo Tianjin University, Jianrong Wang Tianjin University, Yongjia Wang College of Intelligence and Computing, Tianjin University, Jiajun Jiang Tianjin University, Qingchao Shen Tianjin University, Junjie Chen Tianjin University
16:30
15m
Talk
GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
OOPSLA
Damitha Lenadora University of Illinois at Urbana-Champaign, Nikhil Jayakumar University of Texas at Austin, Chamika Sudusinghe University of Illinois at Urbana-Champaign, Charith Mendis University of Illinois at Urbana-Champaign
16:45
15m
Talk
Non-interference Preserving Optimising Compilation
OOPSLA
Julian Rosemann Saarland University, Saarland Informatics Campus, Sebastian Hack Saarland University, Saarland Informatics Campus, Deepak Garg MPI-SWS
Link to publication DOI
17:00
15m
Talk
Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
OOPSLA
Yi Zhang Nanjing University, Yu Wang Nanjing University, Linzhang Wang Nanjing University, Ke Wang Peking University
17:15
15m
Talk
Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
OOPSLA
Junrui Liu University of California, Santa Barbara, Jiaxin Song University of Illinois at Urbana-Champaign, Yanning Chen University of Toronto, Hanzhi Liu University of California, Santa Barbara & Riema Labs, Hongbo Wen University of California, Santa Barbara & Riema Labs, Luke Pearson Polychain Capital, Yanju Chen University of California, San Diego, Yu Feng University of California at Santa Barbara