POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Fri 19 Jan 2024 14:00 - 14:20 at Turing Lecture - Medley Chair(s): Xiaokang Qiu

Characterization of bugs and attack vectors is in many practical scenarios as important as their finding. Recently, Girol et al. have introduced the concept of robust reachability which ensures a perfect reproducibility of the reported violations by distinguishing input which are under the control of the attacker (controlled input) from those which are not (uncontrolled input), and proposed first automated analysis for it. While it is a step toward distinguishing severe bugs from benign ones, it fails to describe violations that are mostly reproducible, i.e., when triggering conditions are likely to happen, meaning that they happen for all uncontrolled input but a few corner cases. To address this issue, we propose to leverage theory-agnostic abduction techniques to generate constraints on the uncontrolled program input that ensure that a target property is robustly satisfied, which is an extension of robust reachability that is generic on the type of trace property and on the technology used to verify the properties. We show that our approach is complete w.r.t. its inference language, and we additionally discuss strategies for the efficient exploration of the inference space. We finally demonstrate the feasibility of the method with an implementation that uses robust reachability oracles to generate constraints on standard benchmarks from software verification and security analysis, and its practical ability to refine the notion of robust reachability. We illustrate the use of our implementation to a vulnerability characterization problem in the context of fault injection attacks. Our method overcomes a major limitation of the initial proposal of robust reachability, without complicating its definition. From a practical view, this is a step toward new verification tools that are able to characterize program violations through high-level feedback.

Fri 19 Jan

Displayed time zone: London change

13:20 - 14:40
MedleyPOPL at Turing Lecture
Chair(s): Xiaokang Qiu Purdue University
13:20
20m
Talk
Guided Equality Saturation
POPL
Thomas Koehler INRIA, Andrés Goens University of Amsterdam, Siddharth Bhat the University of Edinburgh, Tobias Grosser University of Edinburgh, Phil Trinder University of Glasgow, Michel Steuwer TU Berlin; University of Edinburgh
Pre-print
13:40
20m
Talk
Fusing Direct Manipulations into Functional Programs
POPL
Xing Zhang Peking University, Ruifeng Xie Peking University, Guanchen Guo Peking University, Xiao He University of Science and Technology Beijing, Tao Zan Longyan University, Zhenjiang Hu Peking University
Pre-print
14:00
20m
Talk
Inference of Robust Reachability Constraints
POPL
Yanis Sellami CEA, List, Univ. Grenoble Alpes, Guillaume Girol CEA, List, Université Paris Saclay, Frédéric Recoules CEA, List, Damien Couroussé Univ Grenoble Alpes, CEA, List, Sébastien Bardin CEA LIST, University Paris-Saclay
14:20
20m
Talk
Nominal Recursors as Epi-RecursorsDistinguished Paper
POPL
Andrei Popescu University of Sheffield