Apps don't come with any guarantees that they are not malicious. This paper introduces a PhD project designing the authorization framework used for App Guarden. App Guarden is a new project that uses a exible assurance framework based on distribution of evidence, attestation and checking algorithms to make explicit why an app isn't dangerous and to allow users to describe how they want apps on their devices to behave. We use the SecPAL policy language to implement a device policy and give a brief example of a policy being used. Finally we use SecPAL to describe some of the di erences between current app markets.
App stores allow users to buy and install software on their devices with a minimum of fuss. Users trust the app stores not to supply them with malware but sometimes this trust is misplaced. A survey of the various di erent Android markets revealed some malware in all of them|including Google's own Play Store [13]. Malware on mobile platforms typically steals user information and monetises itself by sending premium rate text messages [10]. Sometimes malware on mobile platforms isn't intentional: developers are not security specialists and sometimes make poor security decisions such as signing apps with the same key [2] which can lead to permission escalation on Android or by requesting excessive permissions [7].
Both Google and Apple (who operate the two biggest app markets) check apps submitted to them for malicious code, however neither states exactly what they check for. There is expectation amongst users that these markets check for and are free from malware, but this trust is misplaced [6]. Attempts to reverse engineer the checking procedures for Google's store suggest that they incorporate static and dynamic analysis as well as manual checking by a human being [9]. They o er no guarantees however that any check was actually run.
Digital evidence [11] can be used to con rm the results from static analyses; it is similar to older techniques [8] and allows us to split the inferring of a static analysis result (which may be computationally expensive) from the checking the evidence (which should be e cient). This allows us to verify the results of static analyses for security properties without having to fully run the analysis. ? With thanks to Martin Hofmann and Andy Gordon for their time and advice.
Static analysis checks used to create digital evidence could include taint analysis tools to check where sensitive information is being leaked between apps [5], or a security proof based on the architecture of the machine [3].
The App Guarden project aims to use digital evidence to provide apps with guarantees that the app cannot act maliciously. This will allow us to make explicit the checks made on an app. With explicit checks users will be able to write policies which describe what kinds of apps they will allow on their devices, and what level of trust they require in these checks for an app to be considered installable. We aim to create an enhanced app store that uses inference services, and assurance logics on a modi ed Android to increase trust in devices.
Figure 1 shows an App Guarden store. It provides apps with evidence generated by an inference service. Devices can check the evidence using a trusted checking service, or rely on their trust that the store believed the app to be safe. The SecPAL Engine on the phone is used to check the assertions made by the store and the checker service and enforce a device policy.
App Guarden
Store Apps
Evidence Trusts
Supplies App Guarden
Phone SecPAL Engine
Apps
Generates
Trusts Checks
Inference Service Checker
Service { Show how an authorization logic can specify a policy for how a device behaves. This will use ideas such as proof checking and inference, and show how trust can be distributed between principals. { Show how to use the logic to specify a device policy. We will use digital evidence, and assertions between trusted principals and show how the trust relationships can be propagated between devices. We show how we can use these statements to build con dence that an app is secure. { Describe the di erences between current app markets using the logic and show how they manage access to special resources (such as the address book or a user's photos). This will allow us to compare App Guarden to other systems and allow comparison between other di erent schemes. { Put the logic in a real device and app store and see how the system behaves with real malware and how they interact with device policies. We will look for ways to attack devices with our framework and explore it's limitations. 3
Suppose a user has a mobile device. They might wish that: \No app installed on my phone will send my location to an advertiser, and I wont install anything that Google says is malware."
We call this their device policy. It says what the user will allow on their
device for an app to be installable. To formally write the device policies we use
the SecPAL authorization language [4]. The device policy is show in (
SecPAL is designed to be extensible. Authorization statements take the form
of assertions made by principals. Statements can include predicates which are
de ned by the SecPAL program, as well as constraints (as seen in (
The shows . . . meets predicate in (
We also add an is installable statement to indicate an app is installable on a device and a requires statement to say an app needs a permission to run.
SecPAL allows for attestation of said statements with the can say statement:
these come with a delegation depth. A delegation depth of zero (as shown in (
To evaluate the device policy and decide whether a speci c app is installable SecPAL requires a set of assertions called the assertion-context. An example assertion-context and the proof, using two of SecPAL's evaluation rules from the original paper [4]. To illustrate a usage of SecPAL we give an example where a user wishes to decide whether an app Game can be installed. To do this we use the assertion context bellow:
AC := f Phone says app is installable if app meets NotMalware;
app meets NoInfoLeaks: anyone says app meets policy if evidence shows app meets policy: Phone says NILInferer can say0 app meets NoInfoLeaks: Phone says Google can say1 app meets NotMalware:
Google says AVChecker can say0 app meets NotMalware: AVChecker says Game meets NotMalware: NILInferer says Evidence shows Game meets NoInfoLeaks
if LocalNILCheck(Evidence; Game) = true:
g
(
We evaluate it using the SecPAL rules shown in the cond (
AC; 1 j= A says fact can say
We can use the SecPAL language to describe the di erences between various app markets and devices. The two most popular operating systems are Google's Android, and Apple's iOS. Apple's o ering is usually considered to be the more restrictive system as it doesn't allow the use of alternate market places, whereas an Android user can choose to relax the restrictions and install from anywhere.
For example on iOS an app is only installable on an iPhone if Apple has said
the app can be installed (
iPhone says Apple can say1 app is installable: AndroidPhone says AndroidUser can say1 app is installable:
AndroidUser says Google can say0 app is installable:
Similarly comparisons can be made when apps try to access resources. When
accessing components like the address book or photos; on iOS this is only allowed
when the user has explicitly okayed it. Other operating systems such as
Windows Mobile also follow this pattern. On Android, however, an app can access
any resource it declared itself as requiring it when it was installed.
(
app requires resource:
This is a brief comparison of the implicit device policies in current markets. It shows however that SecPAL is capable of describing the various di erence. This could be extended in future to allow proper comparisons of di erent markets. 5
We have given a brief introduction to App Guarden and the SecPAL language used to describe policies. Using the SecPAL language we described some of the di erences between current systems. The PhD work here is at an early stage. Next steps will include porting the SecPAL language to Android and using it to nd what kinds of device policies are most e ective at stopping dangerous apps, without overly inconveniencing the user. From here we will build an enhanced app market with its own set of policies where apps come with digital evidence to allow users to trust apps further.
Mobile devices are a growing target for malware, and with app stores appearing in conventional computers the di erences between mobile and traditional computing environments are blurring. The App Guarden will help give users greater assurance their software is secure; and provide a new security mechanism to compliment access control and anti-malware techniques.