Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Wed 29 May 2019 16:20 - 16:40 at Laurier - Analysis and Verification Chair(s): Domenico Bianculli

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 ground. In this paper, we present the first formal specification of Android interoperability to establish a firm ground for understanding and reasoning 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 sound and efficient 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.

Wed 29 May
Times are displayed in time zone: Eastern Time (US & Canada) change

16:00 - 18:00
Analysis and VerificationPapers / Demonstrations / Technical Track / Journal-First Papers at Laurier
Chair(s): Domenico BianculliUniversity of Luxembourg
16:00
20m
Talk
Easy Modelling and Verification of Unpredictable and Preemptive Interrupt-driven SystemsArtifacts Evaluated ReusableTechnical Track
Technical Track
Minxue PanNanjing University, Shouyu ChenNanjing University, Yu PeiThe Hong Kong Polytechnic University, Tian ZhangNanjing University, Xuandong LiNanjing University
16:20
20m
Talk
Towards Understanding and Reasoning about Android InteroperationsTechnical Track
Technical Track
Sora BaeOracle Labs, Australia, Sungho LeeKAIST, South Korea, Sukyoung RyuKAIST, South Korea
16:40
20m
Talk
ALPACA: A Large Portfolio-based Alternating Conditional AnalysisDemos
Demonstrations
Mitchell GerrardUniversity of Virginia, Matthew B DwyerUniversity of Virginia
17:00
20m
Talk
Mockingbird: A Framework for Enabling Targeted Dynamic Analysis of Java ProgramsDemos
Demonstrations
Derrick LockwoodIowa State University, Benjamin Holland, Suresh KothariIowa State University, USA
17:20
20m
Talk
Zero-Overhead Path Prediction with Progressive Symbolic ExecutionArtifacts AvailableTechnical Track
Technical Track
Richard RutledgeGeorgia Institute of Technology, Sunjae ParkGeorgia Institute of Technology, Haider KhanGeorgia Institute of Technology, Alessandro OrsoGeorgia Tech, Milos PrvulovicGeorgia Institute of Technology, Alenka ZajicGeorgia Institute of Technology
17:40
10m
Talk
Platform-Independent Dynamic Taint Analysis for JavaScriptJournal-First
Journal-First Papers
Rezwana KarimSamsung Research America, Frank TipNortheastern University, Alena SochurkovaAvast, Koushik SenUniversity of California, Berkeley
17:50
10m
Talk
Discussion Period
Papers