Towards a certified reference monitor of the Android 10 permission system

The Android security model is primarily based on a sandbox and permission mechanism. Each application runs in a private virtual machine with a unique ID assigned to it, which means that one application’s code is isolated from the code of all others. This way of protection entails the existence of a decision procedure (a reference validation mechanism) that arbitrates the access to sensitive data whenever an application wants to share resources with another (or the system). Decisions are made by following security policies using a simple notion of permission.

Every permission is identified by a unique name/text, has a protection level and may belong to a permission group. Furthermore, permissions can be classified into two groups: the ones defined by an application, for the sake of self-protection; and those predefined by Android, which are required to gain access to certain system features, like internet or location. Depending on the protection level of the permission, the system defines the corresponding decision procedure. There are three classes of permission levels [4]: i) normal, this permissions can be automatically granted since they cover data or resources where there’s very little risk to the user’s privacy or the operation of other apps; ii) dangerous, permissions of this level provide access to data or resources that may be sensitive or could potentially affect the operation of other applications, and explicit user approval is needed to be granted; and iii) signature, a permission of this level is granted only if the application that requires it and the application that defined it are both signed with the same certificate. An application must declare –in an XML file called AndroidManifest– the set of permissions it needs to acquire further capacities than the default ones. From version 6 of Android, dangerous permissions are granted on runtime whereas both normal and signature are given when the application is installed.

Permissions may belong to groups that reunites a device’s capabilities. The main purpose of grouping permissions this way is to handle permission requests at the group level, in order to avoid overwhelming the user with too many questions. For example, the SMS group includes the permission needed to read the text messages as well as the one needed to receive them (both considered to be dangerous). Whenever an application needs one of those for the first time, the user will be asked to authorize the whole group. On Section 2.2, we explain what authorizing a group means depending on the platform version.

An Android application is built up from components. A component is a basic unit that provides a particular functionality and that can be run by any other application with the right permissions. There exist four types of components [2]: i) activity, which is essentially a user interface of the application; ii) service, a component that executes in background without providing an interface to the user; iii) content provider, a component intended to share information among applications; and iv) broadcast receiver, a component whose objective is to receive messages, sent either by the system or an application, and trigger the corresponding actions. The communication between components is achieved with the exchange of special messages called intents, which can be either i) explicit, meaning that the target application is specified; or ii) implicit, where only the action to be performed is declared and the system determines which application will run the task (if there is more than one capable application, the user is allowed to choose). In order to be candidates for the implicit intents resolutions, an application must declare on their manifest an intent filter that indicates the types of intents it can respond to.

Android provides two mechanisms by which an application can delegate its own permissions to another one. These mechanisms are called pending intents and URI permissions. An intent may be defined by a developer to perform a particular action. A PendingIntent specifies a reference to an action, which might be used by another application to perform the operation with the same permissions and identity of the one that created the intent. The URI permissions mechanism can be used by an application that has read/write access to a content provider to temporarily delegate those permissions to another application. These permissions are revoked once the receiver activity or service become inactive.

As we described in our previous work [10], the sixth version of Android introduced an important change to the system, allowing the users to handle permissions at runtime. In this section, we give a short account of the changes introduced between Android Nougat (7) and Android 10, that had a significant impact on the permission system.

The Android security model we have developed has been formalized as an abstract state machine. In this model, states ($\mathsf{AndroidST}$) are modelled as 13-tuples that store dynamic data about the system such as the installed applications and their current permissions, as well as static data like the declared manifest of each installed app. A complete formal definition is given in Figure 1.

The type $\mathsf{PermId}$ represents the set of permissions identifiers; $\mathsf{PermGroup}$, the set of permission groups identifiers; $\mathsf{Comp}$, the application components whose code will run on the system; $\mathsf{AppId}$ represents the set of application identifiers; $\mathsf{iComp}$ is the set of identifiers of running instances of application components; $\mathsf{ContProv}$ is a subset of $\mathsf{Comp}$, a special type of component that allows sharing resources among different applications; a member of the type $\mathsf{Uri}$ is a particular URI (uniform resources identifier); the type $\mathsf{Res}$ represents the set of resources an application can have (through its $content~{}providers$, members of $\mathsf{ContProv}$); the type $\mathsf{Val}$ is the set of possible values that can be written on resources; an intent –i.e. a member of type $\mathsf{Intent}$– represents the intention of a running component instance to start or communicate with other applications; a member of $\mathsf{SysImgApp}$ is a special kind of applications which are deployed along with the OS itself and has certain privileges, like being impossible to uninstall.

The first component of the state records the identifiers ($\mathsf{AppId}$) of the applications installed by the user. The second component is a subset of the first one, and represents those applications that are considered to be old but have already been verified, also by the user. The third component keeps track of the permissions granted to every application present in the system, including the ones preinstalled on the system. Similarly, the next component holds the information about what permission groups have already been authorized by the user on each app. The fifth component of the state stores the set of running component instances ($\mathsf{CompInstance}$), while the components $\mathsf{DelPPerms}$ and $\mathsf{DelTPerms}$ store the information concerning permanent and temporary permissions delegations, respectively³³3A permanent delegated permission represents that an app has delegated permission to perform an operation on the resource identified by an URI. A temporary delegated permission refers to a permission that has been delegated to a component instance.. The eighth and ninth components of the state store respectively the values ($\mathsf{Val}$) of resources ($\mathsf{Res}$) of applications and the set of intents ($\mathsf{Intent}$) sent by running instances of components ($\mathsf{iComp}$) not yet processed. The four last components of the state record information that represents the manifests of the applications installed by the user, the certificates ($\mathsf{Cert}$) with which they were signed and the set of permissions they define. The last component of the state stores the set of (native) applications installed in the Android system image, information that is relevant when granting permissions of level $Signature/System$.

A manifest ($\mathsf{Manifest}$) is modelled as a 6-tuple that respectively declare application components (set of components, of type $\mathsf{Comp}$, included in the application); optionally, the minimum version of the Android SDK required to run the application; optionally, the version of the Android SDK targeted on development; the set of permissions it may need to run at its maximum capability; the set of permissions it declares; and the permission required to interact with its components, if any. Application components are all denoted by a component identifier. A content provider ($\mathsf{ContProv}$), in addition, encompasses a mapping to the managed resources from the URIs assigned to them for external access. While the components constitute the static building blocks of an application, all runtime operations are initiated by component instances, which are represented in our model as members of an abstract type.

We modelled the different functionalities provided by the Android security system as a set of actions (of type $\mathsf{Action}$) that determine how the system is able to transition from one state to another. Table 1 summarises the actions specified in our previous model that remained mostly the same since the new features didn’t affect them whereas Table 2 groups those that are new or that suffered a big semantic change.

The behaviour of each action is specified in terms of a precondition ($Pre:\mathsf{AndroidST}\rightarrow\mathsf{Action}\rightarrow Prop$) and a postcondition ($Post:\mathsf{AndroidST}\rightarrow\mathsf{Action}\rightarrow\mathsf{AndroidST}\rightarrow Prop$). For instance, the axiomatic semantics of the new feature about automatic granting of permissions grantAuto is given by:

The precondition establishes several conditions that must be fulfilled before this action is able to transition. The first one requires that the permission $p$ is listed on the application’s manifest (and this manifest, of course, is required to exist). Regarding the permission, it’s also required that its defined either by the user or the system, that its level is $dangerous$ and that it has not been already granted to $app$. Up to this point, the precondition of $grantAuto$ is exactly the same than the one of $grant$. The main difference is established by the following condition: the permission at issue should belong to a group $g$ and the system should know that the user had previously authorized that group for automatic granting.

The postcondition of $\texttt{grantAuto}\ p\ a$ requires that for an initial state $s$ and a final state $s^{\prime}$, the individual permission $p$ is granted to application $app$. This condition is enforced by the $\texttt{grantPerm}\ a\ p\ s\ s^{\prime}$ predicate which only alters the state in component that maps applications with their current dangerous permissions. Every other component of the state remains the same.

Whenever the system attempts to execute an action $a$ over a valid state $s$, there are two possible outcomes. If the precondition holds, the system will transition to another state $s^{\prime}$ where the postcondition of $a$ is established; but if the precondition is not satisfied on $s$, then the state remains unchanged and the system answers with an error message determined by the relation $ErrorMsg$⁴⁴4Given a state $s$, an action $a$ and an error code $ec$, $\mathit{ErrorMsg}(s,a,ec)$ holds iff $error~{}ec$ is an acceptable response when the execution of $a$ is requested on state $s$..

Formally, the possible answers of the system are defined by the type

and the executions can be specified with this operational semantics:

One-step execution with error management preserves valid states.

The property is proved by case analysis on $a$, for each condition in valid_state, using several auxiliary lemmas [19].

System state invariants, such as state validity, are useful to analyze other relevant properties of the model. In particular, the results presented in this work are obtained from valid states of the system.

In this section we present and discuss some properties about the Android 10 security framework. We focus on safety-related properties about the changes introduced on the later versions of Android (mainly Oreo and 10) rather than on security issues. Nevertheless, we also found potentially dangerous behaviours that may not be considered in the informal documentation of the platform and we formally reasoned about them as well. The full formal definition of these properties can be found in [19], along with the corresponding proofs.

On Table 3 we introduce helper functions and predicates used to define the properties that will follow.

The first property that we proved establishes a safety condition about the automatic granting of grouped permissions. It states that the system is not able to transition with this action unless the group of the permission involved is already authorized.

However, a few questions arise when trying to formally describe the situations in which a group is authorized. The following property formalizes an unclear behaviour: there’s at least one valid state where the system can automatically grant a grouped permission to an app even though that the application has no other permission of the same group granted at that moment. This means that an application can have a group authorized for automatic granting via a permission that no longer exist. This is not necessarily a security flaw. It may be a design principle to avoid asking the user to authorize the same group too many times, but the situation is not clear nor disambiguated in the official documentation.

The next property formalizes the situation described in Section 2.2 about normal and dangerous permissions sharing a group. Once again, the lack of a strict documentation about the platform can conduce to ambiguous cases or even to accept a dangerous behaviour as this one.

Users are able to revoke permissions at runtime. However, the UI does not allow to revoke grouped permissions individually, the complete group should be invalidated. Thus, we proved that whenever a user revokes a permission group from an application, every individual permission that belongs to that group is revoked.

The following property reasons about another change mentioned in Section 2.2. It reasons about a good behaviour about the unverified legacy applications.

Finally, we include here a property that holds since version 6 of Android. Any application that wants to send information through the network must have the permission $\mathsf{INTERNET}$, but since this permission is of level $normal$, the application just needs to declare it as used in its manifest. This will give access to the network in an implicit and irrevocable way. Once again, this has been criticized due to the potential information leakage it allows. The following property formally generalizes this situation and embodies a reasonable argument to roll back this security issue introduced in Android Marshmallow.

We proceed now to outline the proof that our functional implementation of the security mechanisms of Android correctly implements the axiomatic model. This property has been formally stated as the following correctness theorem which in turn was verified using Coq [19].

The proof of this theorem starts by performing a case analysis on the (decidable) predicate $Pre(s,a)$. Then, in case that the predicate holds, we apply Lemma 2; otherwise we continue by applying Lemma 3.

The proof of this lemmas proceeds by applying functional induction on $\mathit{step}(s,a)$. Then, in Lemma 2, the proof continues by applying the corresponding subproof of soundness of the function that implements each action; whereas in Lemma 3, a subproof about the existence of a proper error code is provided.

In this section we present several security properties we have stated and proved about the function $trace$ defined in Section 4.

The first property states that in Android 10, if an application that is considered to be old (as we defined in Section 2.2) is able to run, then it has been verified and validated by the user previously.

The next property establishes that for an application to have any dangerous permission (grouped or ungrouped) it must be explicitly granted to it, either by the user or automatically by the system.

The following property formally states that if an application used to have a permission that was later revoked, only re-granting it will allow the application to have it again.