Historia: Refuting Callback Reachability with Message-History Logics (Extended Version)

TL;DR

This paper introduces Historia, a static analysis tool that refines callback control flow reasoning in event-driven frameworks using message histories, enabling verification of callback-related assertions in Android apps.

Contribution

It presents message-history logics and a verification approach that decouples callback control flow specification from app analysis, improving precision and tractability.

Findings

Successfully verified absence of multi-callback bugs in real-world Android apps.

Developed a prototype verifier called Historia with practical effectiveness.

Introduced a novel logic-based framework for reasoning about callback control flow.

Abstract

This paper determines if a callback can be called by an event-driven framework in an unexpected state.Event-driven programming frameworks are pervasive for creating user-interactive apps on just about every modern platform.Control flow between callbacks is determined by the framework and largely opaque to the programmer.This opacity of the callback control flow not only causes difficulty for the programmer but is also difficult for those developing static analysis.Previous static analysis techniques address this opacity either by assuming an arbitrary framework implementation or attempting to eagerly specify all possible callback control flow, but this is either too coarse or too burdensome and tricky to get right.Instead, we present a middle way where the callback control flow can be gradually refined in a targeted manner to prove assertions of interest.The key insight to get this middle way is by reasoning about the history of method invocations at the boundary between app and framework code - enabling a decoupling of the specification of callback control flow from the analysis of app code.We call the sequence of such boundary-method invocations message histories and develop message-history logics to do this reasoning.In particular, we define the notion of an application-only transition system with boundary transitions, a message-history program logic for programs with such transitions, and a temporal specification logic for capturing callback control flow in a targeted and compositional manner.Then to utilize the logics in a goal-directed verifier, we define a way to combine after-the-fact an assertion about message histories with a specification of callback control flow.We implemented a prototype message history-based verifier called Historia that enables proving the absence of multi-callback bug patterns in real-world open-source Android apps.