Goal-Directed Abstract Interpretation and Event-Driven FrameworksKeynote
Static analysis is typically about computing a global over-approxi- mation of a program’s behavior from its source code. But what if most of the program code is missing or unknown to the analyzer? What if even where the program starts is unknown? This fundamentally thorny situation arises when attempting to analyze interactive applications (apps) developed against modern, event-driven software frameworks. Rich event-driven software frameworks enable software engineers to create complex applications on sophisticated computing platforms (e.g., smartphones with a broad range of sensors and rich interactivity) with relatively little code by simply implementing callbacks to respond to events. But developing apps against them is also notoriously difficult. To create apps that behave as expected, devel- opers must follow the complex and opaque asynchronous programming protocols imposed by the framework. So what makes static analysis of apps hard is essen- tially what makes programming them hard: the specification of the programming protocol is unclear and the possible control flow between callbacks is largely un- known. While the typical workaround to perform static analysis with an unknown framework implementation is to either assume it to be arbitrary or attempt to eagerly specify all possible callback control flow, this solution can be too pes- simistic to prove properties of interest or too burdensome and tricky to get right. In this talk, I argue for a rethinking of how to analyze app code in the context of an unknown framework implementation. In particular, I present some benefits from taking a goal-directed or backward-from-error formulation to prove just the assertions of interest and from designing semantics, program logics, specification logics, and abstract domains to reason about the app-framework boundary in a first-class manner. What follows are hopefully lines of work that make ana- lyzing modern interactive applications more targeted, more compositional, and ultimately more trustworthy.
Sun 22 OctDisplayed time zone: Lisbon change
09:00 - 10:30 | Session 1SAS 2023 at Room I Chair(s): Caterina Urban Inria & École Normale Supérieure | Université PSL | ||
09:00 5m | Opening SAS 2023 Manuel Hermenegildo Technical University of Madrid (UPM) and IMDEA Software Institute, José Morales IMDEA Software Institute Pre-print | ||
09:05 60mKeynote | Goal-Directed Abstract Interpretation and Event-Driven FrameworksKeynote SAS 2023 Pre-print | ||
10:05 30mTalk | A Product of Shape and Sequence Abstractions (Radhia Cousot Young Researcher Best Paper Award) SAS 2023 Josselin Giet Ecole Normale Supérieure, Félix Ridoux Univ Rennes / IMDEA Software Institute, Xavier Rival Inria; ENS; CNRS; PSL University Pre-print |