Wed 17 Jul 2019 16:40 - 17:00 at Mancy - Program Analysis 1 Chair(s): Yannis Smaragdakis

Static analyses make the increasingly tenuous assumption that all source code is available for analysis; for example, large libraries often call into native code that cannot be analyzed. We propose a points-to analysis that initially makes optimistic assumptions about missing code, and then inserts runtime checks that report counterexamples to these assumptions that occur during execution. Our approach guarantees eventual soundness, which combines two guarantees: (i) the runtime checks are guaranteed to catch the first counterexample that occurs during any execution, in which case execution can be terminated to prevent harm, and (ii) only finitely many counterexamples ever occur, implying that the static analysis eventually becomes statically sound with respect to all remaining executions. We implement Optix, an eventually sound points-to analysis for Android apps, where the Android framework is missing. We show that the runtime checks added by Optix incur low overhead on real programs, and demonstrate how Optix improves a client information flow analysis for detecting Android malware.

Wed 17 Jul
Times are displayed in time zone: Greenwich Mean Time : Belfast change

15:40 - 17:00
Program Analysis 1Research Papers at Mancy
Chair(s): Yannis SmaragdakisUniversity of Athens
15:40
20m
Research paper
Static Analysis for Asynchronous JavaScript Programs
Research Papers
Thodoris SotiropoulosAthens University of Economics and Business, Ben LivshitsImperial College London, UK
DOI
16:00
20m
Research paper
A Program Logic for First-Order Encapsulated WebAssembly
Research Papers
Conrad WattUniversity of Cambridge, Petar MaksimovićImperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Philippa GardnerImperial College London
DOI Media Attached
16:20
20m
Research paper
Garbage-free Abstract Interpretation through Abstract Reference Counting
Research Papers
Noah Van EsSofware Languages Lab, Vrije Universiteit Brussel, Quentin StiévenartVrije Universiteit Brussel, Belgium, Coen De RooverVrije Universiteit Brussel
DOI
16:40
20m
Research paper
Eventually Sound Points-To Analysis with Specifications
Research Papers
Osbert BastaniUniversity of Pennsylvania, Rahul SharmaMicrosoft Research, Lazaro ClappStanford University, Saswat AnandStanford University, Alex AikenStanford University
DOI Media Attached