Design and Analysis of Mobile Operating System Security Architecture using Formal Methods
Creators: name: Gunadi, Hendra
Publisher: name: The Australian National University
Year: 2017
Subjects: formal method
Android
security

description: The Android operating system (OS) is now used in the majority of mobile devices. Hence, Android security is an important issue to handle. In this work, we tackle the problem using two separate approaches: directly modifying Android OS and developed a framework to provide a guarantee of non-interference. Firstly, we present a design and an implementation of a security policy specifi- cation language based on metric linear-time temporal logic (MTL) to specify timing- dependent security policies. The design of the language is driven by the problem of runtime monitoring of applications in mobile devices. A main case of the study is the privilege escalation attack in the Android OS, where an unprivileged app gains ac- cess to privileged resource or functionalities through indirect flow. To capture these attacks, we extend MTL with recursive definitions to express call chains between apps. We then show how our language design can be used to specify policies to detect privilege escalation under various fine-grained constraints. We present a new algorithm for monitoring safety policies written in our specification language. The monitor does not need to store the entire history of events generated by the apps. We modified the Android OS kernel to allow us to insert our generated monitors mod- ularly. We have tested the modified OS (LogicDroid) on an actual device, and show that it is effective in detecting policy violations. Furthermore, LogicDroid is able to prevent a previously unknown exploit to breach Android security which allows an unprivileged application to access certain critical and privileged functionalities of an Android phone, such as making phone calls, terminating phone calls, and sending SMS, without having to ask any permissions to do so. Subsequently, we provided a framework to ensure non-interference properties of DEX bytecode. Each application in Android runs in an instance of the Dalvik virtual machine, which is a register-based virtual machine (VM). Most applications for Android are developed using Java, compiled to Java bytecode and further into DEX bytecode. Following a methodology that has been developed for Java byte- code certification by Barthe et al., we developed a type-based method for certifying non-interference property of a DEX program. To this end, we develop a formal oper- ational semantics of the Dalvik VM, a type system for DEX bytecode, and prove the soundness of the type system with respect to a notion of non-interference. We have also formalized the proof of a subset of DEX in Coq for an additional guarantee that our proof is correct. We then study the translation process from Java bytecode to DEX bytecode, as implemented in the dx tool in the Android SDK. We show that an abstracted version of the translation from Java bytecode to DEX bytecode preserves the non-interference property. More precisely, we show that if the Java bytecode is typable in Barthe et al.’s type system, then its translation is typable in our type system. This result opens up the possibility to leverage existing bytecode verifiers for Java to certify non-interference properties of Android bytecode.