Non-interference Preserving Optimising Compilation
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 OctDisplayed time zone: Perth change
16:00 - 17:30 | |||
16:00 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 |