POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

Runtime errors that can be triggered by an attacker are sensibly more dangerous than others, as they not only result in program failure, but can also be exploited and lead to security breaches such as Denial-of-Service attacks or remote code execution. Proving the absence of exploitable runtime errors is challenging, as it involves combining classic techniques for safety with novel security analyses. While numerous approaches to statically detect runtime errors have been proposed, they lack the ability to classify program failures as potentially exploitable or not. In this paper, we bridge the gap between traditional safety properties and security hyperproperties by putting forward a novel definition of nonexploitability, which we leverage to propose a sound static analysis by abstract interpretation to prove the absence of exploitable runtime errors. While false alarms can occur, if our analysis determines that a program is nonexploitable, then there is a strong mathematical guarantee that it is impossible for an attacker to trigger a runtime error. Furthermore, our analysis reduces the noise generated from false positives by classifying each warning as security-critical or not. We implemented the first nonexploitability analyzer for a subset of C, and we evaluated it on a set of 77 real-world programs taken from the GNU Coreutils package that are long up to 4,188 lines of code. Our analysis was able to prove that more than 70% of the runtime errors previously reported (3,498 over 4,715) cannot be triggered by an attacker.

Mon 15 Jan

Displayed time zone: London change

14:00 - 15:30
Session 3: Security and Privacy, Model Checking and SynthesisVMCAI at Marconi Room
Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL
14:00
20m
Talk
Automatic and Incremental Repair for Speculative Information Leaks
VMCAI
Joachim Bard CISPA Helmholtz Center for Information Security, Swen Jacobs CISPA, Yakir Vizel Technion—Israel Institute of Technology
14:20
20m
Talk
Sound Abstract Nonexploitability Analysis
VMCAI
Francesco Parolini Sorbonne Université, Antoine Miné Sorbonne Université
Pre-print
14:40
20m
Talk
Solving Two-Player Games under Progress Assumptions
VMCAI
Anne-Kathrin Schmuck MPI-SWS, K. S. Thejaswini The University of Warwick, Irmak Saglam Max Planck Institute for Software Systems (MPI-SWS), Satya Prakash Nayak Max Planck Institute for Software Systems (MPI-SWS)
Pre-print
15:00
20m
Talk
Model-Guided Synthesis for LTL over Finite Traces
VMCAI
Shengping Xiao East China Normal University, Yongkang Li East China Normal University, Xinyue Huang East China Normal University, Yicong Xu East China Normal University, Jianwen Li East China Normal University, China, Geguang Pu East China Normal University, Ofer Strichman Technion, Moshe Vardi Rice University
15:20
10m
Talk
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
VMCAI
Daniel Hausmann University of Gothenburg, Merlin Humml Friedrich-Alexander Universität Erlangen-Nürnberg, Simon Prucker Friedrich-Alexander Universität Erlangen-Nürnberg, Lutz Schröder University of Erlangen-Nuremberg, Aaron Strahlberger Friedrich-Alexander-Universität Erlangen-Nürnberg
Pre-print