Design and Analysis of Mobile Operating System Security Architecture using Formal Methods

dc.contributor.authorGunadi, Hendra
dc.date.accessioned2017-11-16T23:53:30Z
dc.date.available2017-11-16T23:53:30Z
dc.date.issued2017
dc.description.abstractThe 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.en_AU
dc.identifier.otherb47392678
dc.identifier.urihttp://hdl.handle.net/1885/133821
dc.language.isoenen_AU
dc.subjectformal methoden_AU
dc.subjectAndroiden_AU
dc.subjectsecurityen_AU
dc.titleDesign and Analysis of Mobile Operating System Security Architecture using Formal Methodsen_AU
dc.typeThesis (PhD)en_AU
dcterms.valid2017en_AU
local.contributor.affiliationCollege of Engineering and Computer Science, The Australian National Universityen_AU
local.contributor.authoremailHendra.Gunadi@hotmail.comen_AU
local.contributor.supervisorTiu, Alwen
local.contributor.supervisorcontactalwen.tiu@anu.edu.auen_AU
local.description.notesthe author deposited 17/11/2017en_AU
local.identifier.doi10.25911/5d70f0303d38e
local.mintdoimint
local.type.degreeDoctor of Philosophy (PhD)en_AU

Downloads

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Gunadi Thesis 2017.pdf
Size:
3.28 MB
Format:
Adobe Portable Document Format
Description:

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
884 B
Format:
Item-specific license agreed upon to submission
Description:
Back to topicon-arrow-up-solid
 
APRU
IARU
 
edX
Group of Eight Member

Acknowledgement of Country

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.


Contact ANUCopyrightDisclaimerPrivacyFreedom of Information

+61 2 6125 5111 The Australian National University, Canberra

TEQSA Provider ID: PRV12002 (Australian University) CRICOS Provider Code: 00120C ABN: 52 234 063 906