Scaling Instruction-Selection Verification against Authoritative ISA Semantics
This program is tentative and subject to change.
Secure, performant execution of untrusted code—as promised by WebAssembly (Wasm)—requires correct compilation to native code that enforces a sandbox. Errors in instruction selection can undermine the sandbox’s guarantees, but prior verification work struggles to scale to the complexity of realistic industrial compilers.
We present Arrival, an instruction-selection verifier for the Cranelift production Wasm-to-native compiler. Arrival enables end-to-end, high-assurance verification while reducing developer effort. Arrival (1) automatically reasons about chains of instruction-selection rules, thereby reducing the need for developer-supplied intermediate specifications, (2) introduces a lightweight, efficient method for reasoning about stateful instruction-selection rules, and (3) automatically derives high-assurance machine code specifications.
Our work verifies nearly all AArch64 instruction-selection rules reachable from Wasm core. Furthermore, Arrival reduces the developer effort required: 60% of all specifications benefit from our automation, thereby requiring 2.6X fewer hand-written specifications than prior approaches. Arrival finds new bugs in Cranelift’s instruction selection, and it is viable for integration into production workflows.
This program is tentative and subject to change.
Sat 18 OctDisplayed time zone: Perth change
10:30 - 12:15 | |||
10:30 15mTalk | FO-Complete Program Verification for Heap Logics OOPSLA Adithya Murali University of Illinois at Urbana-Champaign, Hrishikesh Balakrishnan University of Illinois Urbana-Champaign, Aaron Councilman Univ of Illinois Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign | ||
10:45 15mTalk | Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back OOPSLA Kevin Batz RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University, Francesca Randone Department of Mathematics, Informatics and Geosciences, University of Trieste, Italy, Tobias Winkler RWTH Aachen University | ||
11:00 15mTalk | Guarding the Privacy of Label-Only Access to Neural Network Classifiers via Formal Verification OOPSLA | ||
11:15 15mTalk | KestRel: Relational Verification Using E-Graphs for Program Alignment OOPSLA Robert Dickerson Purdue University, Prasita Mukherjee Purdue University, Benjamin Delaware Purdue University | ||
11:30 15mTalk | Laurel: Unblocking Automated Verification with Large Language Models OOPSLA Eric Mugnier University of California San Diego, Emmanuel Anaya Gonzalez UCSD, Nadia Polikarpova University of California at San Diego, Ranjit Jhala University of California at San Diego, Zhou Yuanyuan UCSD | ||
11:45 15mTalk | Scaling Instruction-Selection Verification against Authoritative ISA Semantics OOPSLA Michael McLoughlin Carnegie Mellon University, Ashley Sheng Wellesley College, Chris Fallin F5, Bryan Parno Carnegie Mellon University, Fraser Brown CMU, Alexa VanHattum Wellesley College | ||
12:00 15mTalk | Verification of Bit-Flip Attacks against Quantized Neural Networks OOPSLA Yedi Zhang National University of Singapore, Lei Huang ShanghaiTech University, Pengfei Gao ByteDance, Fu Song Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences; Nanjing Institute of Software Technology, Jun Sun Singapore Management University, Jin Song Dong National University of Singapore | ||