Formal Analysis of the Permission Sec Model Androit


of 6
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
2009 Fifth International Conference on Wireless and Mobile Communications Towards Formal Analysis of the Permission-based Security Model for Android Wook Shin, Shinsaku Kiyomoto, Kazuhide Fukushima, and Toshiaki Tanaka KDDI R&D Laboratories, Saitama, Japan Email: {wookshin, kiyomoto, ka-fukushima, toshi} Abstract—Since the source code of Android was released to the public, people have concerned about the security of the Android system. Whereas the insecurity of a system can be easi
  Towards Formal Analysis of the Permission-basedSecurity Model for Android Wook Shin, Shinsaku Kiyomoto, Kazuhide Fukushima, and Toshiaki TanakaKDDI R&D Laboratories, Saitama, JapanEmail: { wookshin, kiyomoto, ka-fukushima, toshi }  Abstract —Since the source code of Android was released tothe public, people have concerned about the security of theAndroid system. Whereas the insecurity of a system can be easilyexaggerated even with few minor vulnerabilities, the security isnot easily demonstrated. Formal methods have been favorablyapplied for the purpose of ensuring security in different contextsto attest whether the system meets the security goals or notby relying on mathematical proofs. In order to commencethe security analysis of Android, we specify the permissionmechanism for the system. We represent the system in terms of a state machine, elucidate the security needs, and show that thespecified system is secure over the specified states and transitions.We expect that this work will provide the basis for assuring thesecurity of the Android system. The specification and verificationwere carried out using the Coq proof assistant.  Keywords -Android; permission; security; formal model; Coq I. I NTRODUCTION Android is an open mobile platform developed by theOpen Handset Alliance (OHA) led by Google, Inc. TheAndroid platform consists of several layers: the Linux kernel,native libraries, the Dalvik virtual machine (VM), and anapplication framework [1]. The Linux kernel provides basicoperating system services and hardware abstraction for theupper software stacks. Native libraries support the miscel-laneous functionalities of web browsing, multimedia dataprocessing, database access, and GPS reception optimized fora resource-limited hardware environment. The register-basedDalvik VM runs Java code with low memory demand. Atthe top of the layers, Android provides a component-basedprogramming framework so that users can easily build theirown applications.An Android application is written with new and reusableapplication building blocks, such as activity , broadcast intent receiver  , service , and content provider  . After an application iswritten, it is deployed in a Zip-compatible archive, .apk file,or the Android package file. An Android package file containscodes, resources, and a special XML file called the AndroidManifest file. The manifest file contains basic informationabout an application such as the package name, componentdescriptions, and permission declarations.The definitions of Android permissions are found in android.Manifest.permissions class. Each permission is defined as astring and conveys the rights to execute a particular operation.In the manifest file, the permissions are sorted into twocategories: permissions required by the application in order Code 1 An example of AndroidManifest.xml. ...<manifest xmlns:android= package= jp.kddilabs. AppMarketClient android:versionCode= 1 android:versionName= 1.0.0 >< uses-permission xmlns:android= android:name= android.permission.INTERNET />< uses-permission xmlns:android= android:name= android.permission.READ_OWNER_DATA />< permission xmlns:android= android:label= @+id/textElement android:name= jp.kddilabs.READ_APPMARKET_DATA android:permissionGroup= @string/app_name android:protectionLevel= normal />< application android:icon= @drawable/icon android:label= @string/app_name >< activity android:name= .AppMarketClientMain ... to execute and permissions required by others in order tointeract with the application components. The permissions thatthe application uses are listed in the  uses-permission  tagand the permissions that the application imposes are in the  permission  tag (see Code 1).Android takes the sandbox approach to prevent an applica-tion from exerting a malicious influence on other applicationsor the system. An Android application basically runs in asecure sandbox; thus, it cannot access other assets unlessexplicitly authorized to do so. The sandbox mechanism issupported by lower level mechanisms. An application is runwithin its own Dalvik VM instance and also runs in a separateLinux process with its own Linux user ID. The system assignsa user ID when an application is installed. In order to interactwith other applications or the system over the isolation,the application needs permission to do that. The permissionauthorization occurs at the application installation time aswell. The application requests the permissions that it needs aswritten in the manifest file, and then the Android system asksthe user for confirmation if allowing the application to have therequested permissions. After authorization for the application,the system will not ask for more permission again.The security mechanisms of Android have apparentlyworked well so far. Several security-related bugs have been re-ported [2][3], but patched without serious security failures. The 2009 Fifth International Conference on Wireless and Mobile Communications 978-0-7695-3750-4/09 $26.00 © 2009 IEEEDOI 10.1109/ICWMC.2009.2187  sandbox mechanism effectively prevents malicious attemptsfrom compromising other parts of the system, as pointed outin [4]. However, it might not be enough to earn customertrust. Moreover, it seems Android faces something bigger thanpractical threats which is the long-standing mistrust of opensource software with regard to security. Contrary to the tradi-tional approach taken by mobile phone service providers andmanufactures, OHA released the Android source code to thepublic and encouraged developers to participate in applicationdevelopment. While the liberation has been applauded by opensource communities, end users and service providers havedoubted the security of the open mobile platform, althoughopen source does not imply easy-to-break and some peopleeven claims the open source approach is stronger in terms of security [5].Applying formal methods is a good way to assure users of the security of a system. Formal methods enable us to clearlystate the elements and behaviors of the system, clarify desiredsecurity properties, and provide the proof that the systemsatisfies the security properties. Besides convincing users of the security of the system, formal methods provide benefits fordevelopers; during the specification and verification processes,developers can grasp inconsistencies and incompleteness in therequirements and implementation and correct the system.This paper mainly presents our specifications and the re-sults of the verification of the permission mechanism of theAndroid system. We represented the system as a state machineaiming to ensure the security of the system in terms of theBasic Security Theorem [6]. The specified state and transitionelements of the system and identified security conditions arebriefly introduced. We also exemplify some lemmas that areused for security proofs. However, we cannot list all of them inthis paper because of space limitations. All specifications andthe verification used the Coq proof assistant. Assuming thatthe reader is already familiar with the basic syntax of Coq andnatural deduction, we did not explain Coq syntax in this paperbecause of space limitations. For further information on Coq,please refer to the Coq Web page [7] and the book by Bertotand Casteran [8].The rest of the paper proceeds as follows. In Section II, wedescribe security requirements and specify system elementsand operations in terms of state-transition system. Then inSection III, the verification of the security properties areintroduced with some exemplified lemmas and proofs. Wediscuss the limitation and expected contribution of our work in Section IV, and conclude in Section V.II. S PECIFICATIONS Although the security of the Android system is enforcedthrough multiple system layers, we only specify the permissionmechanism, which is defined at the Android application frame-work. In other words, we do not specify the sandbox enforce-ment of the VM or the Linux kernel. The security of the Linuxkernel and the VM has been studied separately. Our formalmodel would be too complicated if we specified the securitymechanisms of other layers altogether. Moreover, the notionof permission is to release capabilities, whereas the sandboxis to provide restrictions. Accordingly, we concentrated on thereleasing features, assuming that the sandbox mechanism isworking properly. We only include security-related featuresin our specifications in order to keep the specifications to amanageable size.Modeling the permission mechanism of the Android systemgoes through several steps, which are similar to the Goguen-Meseguer program described by Cristia [9]: ã Step 1: List the security needs. ã Step 2: Take security-related parts of the system (e.g.,data structures, algorithms, input, output, etc.) and de-scribe the system: define states with chosen system el-ements and define transitions based on the operationsthat affect the state elements. The specification resultsare introduced in Section II-A and Section II-C. ã Step 3: Describe security conditions formally in terms of a state. The security conditions are based on the securityneeds of Step 1. ã Step 4: Prove that security conditions are satisfied overstate transitions.The security needs in the permission-based Android systemcan be addressed as follows: applications request permissionsstatically, not dynamically. In other words, permissions thatan application requests must be written in its manifest file.The permissions are granted by the user when the applicationis installed and is maintained for the duration of the lifeof the application. The grant information is removed whenthe application is uninstalled from the system. In addition,running components of the application must have only thepermissions granted to the application. Thus, it would bepossible to carry out the basic idea of the Android securityarchitecture: “no application has permission to perform anyoperation that would adversely impact other applications, theoperating system, or the user” [10]. The needs can be groupedand detailed as follows: ã A user grants an application the permissions that theapplication requested. The requested permissions oughtto be written in the manifest file of the application. Nomore permissions are given to an application than theapplication requested. ã An installed application is distinguishable from others byits identifier. An application has authorized permissionsonly for the duration of its lifetime in the system. Nomore permissions are allowed than have been authorized.Only installed applications can have permissions in thesystem. ã A component is distinguishable from others by its iden-tifier. Every component is a child of an application, andthey both have each others information. A component isallowed to have the permissions granted to the parentapplication. At most, only one foreground componentexists in a certain state. 88   A. System state In this section, we define the primitive elements of thesystem: permissions, applications, components, authorizations,and states.An Android permission is the right to execute a specificoperation. Since permissions are designed to expand the func-tionality of a sandboxed process out of the limitation, theyare generally related to access to particular data or functionsof other applications or the system. In our specifications, wedefine permissions as a set. The elements of the permission setare distinguishable from each other, and it is sufficient for usto reason about the security of the system. We do not introduceindividual definitions of the android.Manifest.permission oruser-defined permissions.The application, AppPackage , is a record type with thefollowing fields: an identifier, a set of application components,and a permission request. A set of application components isidentified by app cmpnnts . The record type PermRequest  isdefined to represent the permission request of an application.Each predicate permreq ineed  and permreq uneed  maps thelisted permissions in the  uses-permission  and  permission  tags, respectively. Record AppPackage : Type := mkAppPackage { app id  : AppID ; app cmpnnts : CmpnntID → Prop ; app permrqst  : PermRequest  } . Record PermRequest  : Type := mkPermRequest  {  permreq ineed  : Permission → Prop ;  permreq uneed  : Permission → Prop } . Cmpnnt  is also a record type for components. It has anidentifier cmpnnt id  and a parent application cmpnnt papp .The Cmpnnt  does not have permission information itself, butit will use the permissions of the parent application. Record Cmpnnt  : Type := mkCmpnnt  { cmpnnt id  : CmpnntID ; cmpnnt papp : AppPackage } . Before an application is installed, the package installer of the system asks whether the user will grant the set of permis-sions the application requests. Based on the user response, thesystem allows the application to have the permission], or not.The allowance is defined as Authorization as follows: Record Authorization : Type := mkAuthorization { auth by user  : AppID → Permission → Prop } . Now we can define a system state as a record type: Record State : Type := mkState { state fgcmpnnt  : optionT Cmpnnt  ; state package tbl : AppPackage → Prop ; state perm tbl : AppID → Permission → Prop } . The state fgcmpnnt  is the foreground component run-ning on top of the handset screen. It is the optionT typethat is an inductive type with two constructors: ExT  : (T:Type) → optionT  and NoneT  : optionT  . ExT  is param-eterized with a a type; therefore, the optionT can repre-sent the optional existence of an object. For example, whenwe have (s:State) and (cmp:Cmpnnt) , state fgcmpnnt s = ExT cmp means that there is a foreground component atthe state s . Conversely, state fgcmpnnt s = NoneT  meansthat there is no foreground component at s . The defini-tion of optionT is borrowed from another user-contributedCoq library, Icharate.Kernel.lambda coq. The package table, state package tbl identifies a set of installed applications atthat state. The permission table, state permission tbl does setsof authorized permissions for applications.  B. Security Property From the security needs mentioned at the beginning of theSection II, we obtain the security conditions and state thoseusing predicates with respect to the state. The predicates areself-explanatory, but it would be better to clarify the meaningof the naming terms here; an “ installed  ” application app atstate s means that the s has information about the app inits package table, that is, ( state package tbl s app ) is true.If an application app “ requested  ” permission p , then the app asked for p using its permission request prqst  . It can be statedas (  permreq ineed prqst p ), when prqst = (app permrqst app) . If permission p is “ granted  ” to an application app atstate s , then s has the information in its permission table.Hence, ( state perm tbl s appid p ) holds, where the appid  is the identifier of the app . Permission p is “ authorized  ” foran application app , if and only if there was a decision thatallows the app to have p . Thus, a predicate ( auth by user auth appid p ) holds for the authorization auth . Furthermore,we say permission p is “  properly ” given to an application app if  p is “ requested  ” by and “ granted  ” to the “ installed  ” app .1) SecureAuth is a predicate that holds, if and only if, anypermission given to any application at a state entailsthat the application requested the permission based onits manifest information.2) SecureCmpnnt  is a combination of three predicates, andall of the predicates specify security conditions forthe foreground component of a given state; a predi-cate fgCmpnntIsAGoodChild  holds when the foregroundcomponent has its parent application and both of them,the component and the parent have each other’s informa-tion. fgCmpnntIsInstalled  is valid when the parent ap-plication is an installed application. cmpnntAppIsProper  is satisfied when the parent application requested a setof permissions, and the permissions were granted.3) SecureApp is valid when all installed applications in agiven state request and are granted the permissions theyneed.Combining those conditions, we define the security prop-erty. The notion of security is defined by that property. In otherwords, if the security property holds at a state, we considerthe state to be secure. In the verification process, the followingproperty will be tested at every transition between states, inorder to confirm whether system operations do not violate thesecurity conditions. 89  Definition SecureState (s:State) : Prop := SecureAuth s ∧ SecureCmpnnt s ∧ SecureApp s . As an example, let us unfold the cmpnntAppIsProper  whichis a part of the SecureCmpnnt  . It tests whether the parent ap-plication of the foreground component has proper permissions: Definition cmpnntAppIsProper  ( s : State ) : Prop := ∀ ( app :  AppPackage ) ( cmp : Cmpnnt  ), state fgcmpnnt s = ExT cmp → app = cmpnnt papp cmp → appIsProper s app . The appIsProper  tests whether the given application isproper using pIsRequested  and pIsGranted  . The two functionsare defined using the previously described primitive predicates,as their names delineate. The following shows the definitionof the pIsGranted  : Definition pIsGranted  ( s : State ) ( appid  :  AppID ) (  p : Permission ) : Prop := state perm tbl s appid p . C. Transition The execution of an operation results in state changes inthe system. The operations of our concern are as follows:install application, start a component execution, terminate acomponent execution, and remove an application. Those oper-ations affect the security of the system by changing the stateinformation: the foregroundcomponent, the package table, andthe permission table. We specify the four operations in termsof the precondition and the postcondition. A preconditiondescribes the conditions that have to be satisfied at state s , anda postcondition explains changes between s and another state s’ . Let us call those states pre-state and post-state, respectively.The below example specification below is of the terminate operation, which has simpler descriptions than others. Definition Pre terminate ( s : State ) ( cmpid  : CmpnntID ) : Prop := ∃ cmp : Cmpnnt  , state fgcmpnnt s = ExT cmp ∧ ( cmpid  = cmpnnt id cmp ). Definition Post terminate ( s s’ : State ) ( cmpid  : CmpnntID ): Prop := state package tbl s = state package tbl s’ ∧ state perm tbl s = state perm tbl s’ ∧ state fgcmpnnt s’ = NoneT  . Since terminate finishes the given foreground component,the operation is executed only when the given component isrunning in the foreground. The operation terminate does notchange installed applications and given permissions, but theforeground component will be removed.The specification of the operation install is a little longer: Definition Pre install ( s : State )( newapp :  AppPackage ) ( auth :  Authorization ) : Prop :=( ∀ ( app :  AppPackage ), ( ∀ p : Permission , state perm tbl s ( app id app ) p → permreq ineed  ( app permrqst app ) p )) ∧ ( ∀ cmp : Cmpnnt  , state fgcmpnnt s = ExT cmp → cmpnnt papp cmp  = newapp ) ∧ ( ∀ p : Permission , auth by user auth ( app id newapp ) p → permreq ineed  ( app permrqst newapp ) p → ˜( state perm tbl s ( app id newapp ) p )) ∧ ( ∀ app :  AppPackage , state package tbl s app → ( app id app  = app id newapp ) ) Definition Post install user success ( s s’ : State )( newapp :  AppPackage ) ( auth :  Authorization ) : Prop := ud  = ok  ∧ state fgcmpnnt s = state fgcmpnnt s’ ∧ ( ∀ app :  AppPackage , app id app  = app id newapp ) → ( state package tbl s app = state package tbl s’ app ) ∧ ( state perm tbl s ( app id app ) = state perm tbl s’ ( app id app ))) ∧ ( ∀ ( someapp :  AppPackage ) (  p : Permission ), ( app id newapp = app id someapp ) → state perm tbl s’ ( app id someapp ) p ) ∧ ( ∀ (  p : Permission ), state perm tbl s’ ( app id newapp ) p → auth by user auth ( app id newapp ) p ) ∧ ( ∀ ( someapp :  AppPackage ) (  p : Permission ), ( app id newapp = app id someapp ) → pIsRequested someapp p ) ∧ ( ∀ (  p : Permission ), state perm tbl s’ ( app id newapp ) p → auth by user auth ( app id newapp ) p → permreq ineed  ( app permrqst newapp ) p ) ∧ ( ∀ cmp : Cmpnnt  , state fgcmpnnt s’ = ExT cmp → ( app id  ( cmpnnt papp cmp ))  = ( app id newapp )). The precondition of  intall states the following conditions:granted permissions to all existing applications are requestedbeforehand according to the manifest information. If somepermissions are authorized for a new application, then thepermissions are requested by the application, and there is alsono relevant authorization in the current state. The existing ap-plications cannot be the new application. The new applicationdoes not exist in the package table of the current state andcannot be the parent of the currently running component.The postcondition of the install are distinctly defined bywhether the installation was successful or not. Whereas anunsuccessful install execution does not change any infor-mation, a successful execution changes the permission tableand the package table at post-state s’ . A new applicationis installed at s’ with a set of authorized permissions, andthe permissions must have been requested by the application.Other applications stay residing the same as the pre-state andso do their granted permissions. The new application cannotbe the parent of the foreground component at s’ , of course.Now, we define state transition by composing the specifiedoperations. In a state with a given operation, the transitionoccurs if the precondition is satisfied and results in yieldinga new state as the postcondition describes. If the preconditiondoes not hold, the system stays at the state. In the followingdefinition of the transition, Operation is an inductive typecomposed of the specified operations, so op will be pattern-matched. Inductive TransFunc ( s : State ) ( op : Operation ) ( s’ : State ): Prop := | transMove : PreCondition s op → PostCondition s s’ op → TransFunc s op s’ | transStay : ¬ PreCondition s op → s = s’ → TransFunc s op s’ . III. V ERIFICATION The objective of the verification is to confirm whether alltransitions satisfy the security property occurring over states.In order to do that, we have to prove the security conditionshold at poststate s’ for every operation with the followingassumptions: ã The security conditions hold at the prestate s 90
Related Search
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks