Towards Understanding and Reasoning About Android Interoperations
Towards Understanding and Reasoning About Android Interoperations
复制标题
关于 Android 互操作的理解和推理
DOI：
10.1109/icse.2019.00038
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Sukyoung Ryu
中科院分区：
文献类型：
--
作者：
Sora Bae;Sungho Lee;Sukyoung Ryu
由于混合应用程序对可移植性和特定于设备的功能的支持，它已成为移动应用程序开发人员最有吸引力的选择之一。例如，Android 混合应用程序通过 JavaScript 支持可移植性，通过 Android Java 支持特定于设备的功能，以及它们之间的无缝交互。然而，它们的互操作语义通常记录不足且不直观，这使得混合应用程序容易出错。虽然最近的研究已经解决了这些漏洞，但它们都没有任何正式依据。在本文中，我们提出了 Android 互操作性的第一个正式规范，为理解和推理互操作性奠定了坚实的基础。我们通过广泛的测试和对 Android 源代码的彻底检查来识别其语义。我们扩展了现有的多语言语义来正式表达混合机制、动态和不可区分的互操作性的关键特征。基于扩展，我们逐步定义了正式的互操作语义，并揭示了其众多不直观和不一致的行为。此外，在形式语义之上，我们设计了一个轻量级类型系统，可以检测由于不直观的语言间通信而导致的错误。我们证明，在现实的 Android 混合应用程序中，它比 HybriDroid（最先进的 Android 混合应用程序分析器）更有效地检测到更多错误。
Hybrid applications (apps) have become one of the most attractive options for mobile app developers thanks to its support for portability and device-specific features. Android hybrid apps, for example, support portability via JavaScript, device-specific features via Android Java, and seamless interactions between them. However, their interoperation semantics is often under-documented and unintuitive, which makes hybrid apps vulnerable to errors. While recent research has addressed such vulnerabilities, none of them are based on any formal grounds. In this paper, we present the first formal specification of Android interoperability to establish a firm ground for understanding and reasoning about the interoperations. We identify its semantics via extensive testing and thorough inspection of Android source code. We extend an existing multi-language semantics to formally express the key features of hybrid mechanisms, dynamic and indistinguishable interoperability. Based on the extensions, we incrementally define a formal interoperation semantics and disclose its numerous unintuitive and inconsistent behaviors. Moreover, on top of the formal semantics, we devise a lightweight type system that can detect bugs due to the unintuitive inter-language communication. We show that it detects more bugs more efficiently than HybriDroid, the state-of-the-art analyzer of Android hybrid apps, in real-world Android hybrid apps.