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 JulDisplayed time zone: Belfast change
15:40 - 17:00 | |||
15:40 20mResearch paper | Static Analysis for Asynchronous JavaScript Programs Research Papers Thodoris Sotiropoulos Athens University of Economics and Business, Ben Livshits Imperial College London, UK DOI | ||
16:00 20mResearch paper | A Program Logic for First-Order Encapsulated WebAssembly Research Papers Conrad Watt University of Cambridge, Petar Maksimović Imperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Neel Krishnaswami Computer Laboratory, University of Cambridge, Philippa Gardner Imperial College London DOI Media Attached | ||
16:20 20mResearch paper | Garbage-free Abstract Interpretation through Abstract Reference Counting Research Papers Noah Van Es Sofware Languages Lab, Vrije Universiteit Brussel, Quentin Stiévenart Vrije Universiteit Brussel, Belgium, Coen De Roover Vrije Universiteit Brussel DOI | ||
16:40 20mResearch paper | Eventually Sound Points-To Analysis with Specifications Research Papers Osbert Bastani University of Pennsylvania, Rahul Sharma Microsoft Research, Lazaro Clapp Stanford University, Saswat Anand Stanford University, Alex Aiken Stanford University DOI Media Attached |