Evaluating Modern Mobile Security: A Multifaceted Approach Using Formal Methods and Empirical Analysis

Mobile devices, such as smartphones, smartwatches, and tablets, represent a class of portable computing systems characterized by wireless connectivity, compact form factors, and independent power sources. These devices offer local data storage capabilities and intuitive user interfaces while maintaining mobility. Their unprecedented convenience has catalyzed widespread adoption, with billions of users worldwide relying on them for sensitive tasks including financial transactions, authentication, and personal data storage. This massive adoption means vulnerabilities can lead to large-scale privacy breaches, financial losses, and identity theft affecting millions of users simultaneously.

Moreover, as smartphones increasingly bridge our digital and physical lives, modern mobile security becomes more critical. The contemporary mobile ecosystem creates a situation where a single breach can compromise not only our social and financial accounts but also the IoT devices that control our homes and daily routines. The interconnected nature of these mobile devices necessitates new standard specifications, APIs, and policies, which in turn creates new attack surfaces that require thorough security analysis. Studying these three aspects presents several technical challenges, including a shift in responsibility from humans to programs, the need for a more systematic analysis, and the requirement for more scalable approaches.

However, traditional program analysis techniques alone might not be sufficient to address emerging security challenges, making innovative research on modern mobile security a critical concern. To address these challenges, I systematically investigated multiple dimensions of modern mobile security: data protection both on-device and in-transit, application security including apps and libraries, operating system security for APIs and system services, policy correctness and specifications compliance, and measurement of knowledge gaps between user awareness and UI design. My research utilizes a multifaceted methodology that combines static and dynamic program analysis, formal verification of security protocols, and user studies to evaluate security awareness.

More concretely, for modern security APIs, my work delved into the authentication mechanisms of mobile applications, particularly focusing on SMS-based One-Time Passwords (OTPs). This investigation systematically studied the threats posed by local attacks, where an attacker controls an unprivileged app on the victim’s device, employing a combination of reverse engineering, formal verification, user studies, and large-scale automated analysis to uncover design and implementation flaws in both third-party apps and the Android operating system.

Regarding modern security standards, I conducted the first systematic security analysis of Android’s scoped storage mechanism. This involved designing and implementing a novel testing tool that utilizes differential analysis to identify security issues and inconsistencies in Android’s storage handling across different versions and OEM implementations, thereby addressing the complexities and potential vulnerabilities introduced by evolving storage paradigms.

Furthermore, for modern security policies, I performed the first look at the security of the mobile driving license (mDL) standard and its real-world implementations. This research involved formally modeling mDL usage scenarios to identify potential pitfalls in implementing the standard and developing a dynamic analysis tool to evaluate the compliance of mDL reader applications in the market.