一句话：提出静态工具 SIERRA，通过统一动作序、上下文抽象与按需路径敏感分析精确检测 Android 事件驱动竞态。
Android 应用并发错误主要来自事件驱动竞态，已有可扩展检测方法多为动态，存在覆盖不足与漏报。本文提出静态检测方法与工具 SIERRA：以“concurrency action”统一线程、事件/消息、系统与用户动作，并静态推导动作间 happens-before 序。为处理 Android 外部编排控制流、回调、异步任务和临时同步，作者引入自动生成代码模型、action-sensitivity 事件驱动上下文抽象，以及反向符号执行支持的按需路径敏感以减少误报。在 194 个 Android 应用上评估，其中 20 个与先进动态检测器比较；SIERRA 通常约 960 秒分析一个应用，平均发现 29.5 个真实竞态、3.5 个误报，动态检测器仅发现 4 个。
Event-based races are the main source of concurrency errors in Android apps. Prior approaches for scalable detection of event-based races have been dynamic. Due to their dynamic nature, these approaches suffer from coverage and false negative issues. We introduce a precise and scalable static approach and tool, named SIERRA, for detecting Android event-based races. SIERRA is centered around a new concept of "concurrency action" (that reifies threads, events/messages, system and user actions) and statically-derived order (happens-before relation) between actions. Establishing action order is complicated in Android, and event-based systems in general, because of externally-orchestrated control flow, use of callbacks, asynchronous tasks, and ad-hoc synchronization. We introduce several novel approaches that enable us to infer order relations statically: auto-generated code models which impose order among lifecycle and GUI events; a novel context abstraction for event-driven programs named action-sensitivity and finally, on-demand path sensitivity via backward symbolic execution to further rule out false positives. We have evaluated SIERRA on 194 Android apps. Of these, we chose 20 apps for manual analysis and comparison with a state-of-the-art dynamic race detector. Experimental results show that SIERRA is effective and efficient, typically taking 960 seconds to analyze an app and revealing 43 potential races. Compared with the dynamic race detector, SIERRA discovered an average 29.5 true races with 3.5 false positives, where the dynamic detector only discovered 4 races (hence missing 25.5 races per app) -- this demonstrates the advantage of a precise static approach. We believe that our approach opens the way for precise analysis and static event race detection in other event-driven systems beyond Android.
DOI 原文 ·
@inproceedings{paperbot4294,
title = {Static Detection of Event-based Races in Android Apps},
author = {Yongjian Hu and Iulian Neamtiu},
booktitle = {ASPLOS},
year = {2018},
doi = {10.1145/3173162.3173173}
}