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.

翻译：本文旨在判断事件驱动框架是否会在意外状态下调用回调函数。事件驱动编程框架几乎在每个现代平台中都被广泛用于创建用户交互式应用程序。回调之间的控制流由框架决定，且对程序员而言大多不透明。这种回调控制流的不透明性不仅给程序员带来困难，也使得静态分析工具的开发者面临挑战。以往的静态分析技术要么假设任意的框架实现，要么试图详尽地预定义所有可能的回调控制流，但这两种方法要么过于粗糙，要么过于繁琐且难以正确实现。为此，我们提出一种折中方案：通过目标导向的方式逐步细化回调控制流，从而证明感兴趣的不变性断言。实现这一折中方案的关键在于：对应用代码与框架代码边界上的方法调用历史进行推理——这使得回调控制流的规格说明与应用代码的分析能够解耦。我们将此类边界方法调用的序列称为消息历史，并开发了消息历史逻辑以进行推理。具体而言，我们定义了带有边界转换的纯应用转换系统、针对此类转换的消息历史程序逻辑，以及用于以目标导向和组合方式捕获回调控制流的时间规格说明逻辑。为了在目标导向的验证器中使用这些逻辑，我们提出了一种事后将关于消息历史的断言与回调控制流的规格说明相结合的方法。我们实现了一个名为Historia的原型消息历史验证器，该工具能够在真实世界的开源Android应用程序中证明不存在多回调错误模式。