A permission-dependent type system for secure information flow analysis

Abstract

We introduce a novel type system for enforcing secure information flow in an imperative language. Our work is motivated by the problem of statically checking potential information leakage in Android applications. To this end, we design a lightweight type system featuring Android permission model, where the permissions are statically assigned to applications and are used to enforce access control in the applications. We take inspiration from a type system by Banerjee and Naumann to allow security types to be dependent on the permissions of the applications. A novel feature of our type system is a typing rule for conditional branching induced by permission testing, which introduces a merging operator on security types, allowing more precise security policies to be enforced. The soundness of our type system is proved with respect to non-interference. A type inference algorithm is also presented for the underlying security type system, by reducing the inference problem to a constraint solving problem in the lattice of security types. In addition, a new way to represent our security types as reduced ordered binary decision diagrams is proposed.

Keywords

Secure information flow secure type system non-interference permission-dependent Android

1. Background and introduction

Mobile security has become increasingly important for our daily life due to the pervasive use of mobile applications. Among the mobile devices that are currently in the market, Android devices account for the majority of them so analyses of their security have been of significant interest. There has been a large number of analyses on Android security ([2,17,19,26,53]) focusing on detecting potential security violations. Here we are interested instead in the problem of constructing secure applications, in particular, in providing guarantees of information flow security in the constructed applications.

We follow the language-based security approach whereby information flow security is enforced through type systems [12,13,46,52]. In particular, we propose a design of a type system that guarantees a non-interference property [52], i.e., typable programs are non-interferent. As shown in [20], non-interference provides a general and natural way to model information flow security. The type-based approach to non-interference requires assigning security labels to program variables and security policies to functions or procedures. Such policies are typically encoded as types, and typeability of a program implies that the runtime behavior of the program complies with the stated policies. Security labels form a lattice structure with an underlying partial order ⩽, e.g., a lattice with two elements “high” (H) and “low” (L) where $L ⩽ H$ . Typing rules can then be designed to prevent both explicit and implicit flow (through conditionals, e.g., if-then-else statements) from H to L. To prevent an explicit flow, the typing rule for an assignment statement such as x := e would require that $l (e) ⩽ l (x)$ where $l (\cdot)$ denotes the security level of an expression. To prevent an implicit flow, e.g., if (y = 0) then x:= 0 else x := 1, most type systems for non-interference require that the assignments in both branches are given the same security level that is higher or at least equal to the security level of the condition (y=0). For example, if y is of type H and x is of type L, the statement would not be typable.

Listing 1.

Getting contact info with a permission check

1.1. Motivating examples

In designing an information flow type system for Android, we encounter a common pattern of conditionals that would not be typable using conventional type systems. Consider the pseudo-code in Listing 1. Such a code fragment could be part of a phone dialer or a social network service app such as Facebook and WhatsApp, where getContactNo provides a public interface to query the phone number associated with a name. The (implicit) security policy in this context is that contact information (the phone number) can only be released if the calling app has the permission READ_CONTACT. The latter is enforced using the checkPermission API in Android. Suppose phone numbers are labelled with H, and the empty string is labelled with L. If the interface is invoked by an app that has the required permission, the phone number (H) is returned; otherwise an empty string (L) is returned. In both cases, no data leakage happens: in the former case, the calling app is authorized; and in the latter case, no sensitive data is ever returned. By this informal reasoning, the function complies with the implicit security policy and it should be safe to be called in any context, regardless of the permissions the calling app has. However, in the traditional (non-value dependent) typing rule for the if-then-else construct, one would assign the same security level to both branches, and the return value of the function would be assigned level H. As a result, if this function is called from an app with no permission, assigning the return value to a variable with security level L has to be rejected by the type system even though no sensitive information is leaked. To cater for such a scenario, we need to make the security type of getContactNo depend on the permissions possessed by the caller.

Banerjee and Naumann [3] proposed a type system (which we shall refer to as BN system) that incorporates permissions into function types. Their type system was designed for an access control mechanism different from ours, but the basic principles are still applicable. In BN system, a Java class may be assigned a set of permissions which need to be explicitly enabled via an enable command for them to have any effect. We say a permission is disabled for a class if it is not assigned to the class, or it is assigned to the class but is not explicitly enabled. Depending on the permissions of the calling class (corresponding to an app in the above example), a function such as getContactNo can have a collection of types. In BN system, the types of a function take the form $(l_{1}, \dots, l_{n}) \overset{P}{\to} l$ where $l_{1}, \dots, l_{n}$ denote security levels of the input, l denotes the security level of the output and P denotes a set of permissions that are disabled by the caller. The idea is that permissions are guards to sensitive values. Thus conservatively, one would type the return value of getContactNo as L only if one knows that the permission READ_CONTACT is disabled. In BN system, getContactNo admits the following types: $\begin{matrix} getContactNo : L \overset{P}{\to} L getContactNo : L \overset{\emptyset}{\to} H \end{matrix}$ where $P = {READ_CONTACT}$ . When typing a call to getContactNo by an app without permissions, the first type of getContactNo is used; otherwise the second type is used.

In BN system, each class is assigned a set of permissions, but before these permissions can be exercised, they must be explicitly enabled with an enable command. Initially all permissions are disabled by default. The typing judgment in BN system keeps track of the set of permissions (denoted by Q in the rules below) that are disabled at a particular point in the program. The language of BN system also features a command “ $test (P) c_{1} else c_{2}$ ”, which means that if the permissions in the set P are all enabled, then the command behaves like $c_{1}$ ; otherwise it behaves like $c_{2}$ . The typing rules for the test command (in a much simplified form) are:

where Q is a set of permissions that are disabled. When $Q \cap P \neq \emptyset$ , then at least one of the permissions in P is disabled, thus one can determine statically that “test(P)” would fail and only the else branch would be executed at runtime. This case is reflected in the typing rule R2. When $Q \cap P = \emptyset$ , there can be two possible runtime scenarios. One scenario is that all permissions in P are enabled, so “test(P)” succeeds and $c_{1}$ is executed. The other is that some permissions in P are disabled, but are not accounted for in Q. This could happen in BN system due to the way permissions are propagated and/or inherited across different classes, so it could happen that the context in which the program being typed occurs is not authorized to access some permissions in P. As noted in [3], in this case, one cannot determine statically, from the information available in the typing judgment, whether the test ‘test(P)’ succeeds, so the typing rule R1 conservatively considers typing both branches.

In adapting BN system to Android, we can make some simplifications: permissions of an app are always enabled, and they are static.1

¹
Some permissions in Android 6 and above require user approval at runtime, but for the purpose of typing the ‘test’ command, we make the assumption that these permissions are enabled as well.

So in this case, we can assume that

Q = \emptyset

, and only the rule R1 is relevant here. However, even with these simplifications, it is still not possible to determine statically whether ‘test(P)’ would succeed or not, in the context where the program being typed is part of a service that may be called by arbitrary apps, so their permissions cannot be determined statically. So it seems that a straightforward adaptation of BN system to Android would still keep the form of R1. However, R1 is still too strong in some scenarios, where the desired security policy requires the absence of some permissions for the release of sensitive information. We call such a policy a non-monotonic policy, in the sense that, viewing a policy as a function from permission sets to security labels, the possession of more permissions does not equal the ability to acquire more sensitive information.

Listing 2.

An example with a non-monotonic policy

For an example of an application for which a non-monotonic policy is desirable, consider for example an application that provides the location information related to a certain advertising ID (in Listing 2), where the latter provides a unique ID for the purpose of anonymizing mobile users to be used for personalized advertising (instead of relying on hardware device IDs such as IMEI numbers). If one can correlate an advertising ID with a unique hardware ID, it will defeat the purpose of the anonymizing service provided by the advertising ID. To prevent that, getInfo returns the location information for an advertising ID only if the caller does not have access to the device ID. That is, if the caller of getInfo possess the permission to access the device ID, then the caller should not be able to obtain any information that contains the location information; so this policy is non-monotonic: a caller with no permissions is allowed to access the sensitive information (location), whereas another caller with more permission is not allowed to access that information.

To simplify the discussion, let us assume that the permissions to access the IMEI number and the location information are denoted by p and q, respectively; and aid denotes a unique advertising ID generated and stored by the app for the purpose of anonymizing user tracking and loc denotes the location information. The function getInfo first tests whether the caller has access to the IMEI number. If it does, and if it has access to the location information, then only the location information is returned. If the caller has no access to the IMEI number, but can access the location information, then the combination of the advertising id and the location information aid++loc is returned. In all other cases, the empty string is returned. Let us consider a lattice with four elements ordered as: $L ⩽ l_{1}, l_{2} ⩽ H$ , where $l_{1}$ and $l_{2}$ are incomparable. We specify that empty string is of type L, loc is of type $l_{1}$ , aid is of type $l_{2}$ , and the aggregate aid++loc is of type H. Consider the case where the caller has permissions p and q and both are (explicitly) enabled. When applying BN system, the desired type of getInfo in this case is $() \overset{\emptyset}{\to} l_{1}$ . This means that the type of r has to be at most $l_{1}$ . Since no permissions are disabled, only R1 is applicable to type this program. This, however, will force both branches of test(p) to have the same type. As a result, r has to be typed as H so that all four assignments in the program can be typed.

The issue with the example in Listing 2 is due to the inability to determine statically whether ‘test(P)’ succeeds, leading to a conservative choice in the rule R1 of assigning the same types to both branches of the test. As a result, BN system cannot precisely capture the non-monotonic security policy in our example above: when the caller has permissions p and q, the desired type of getInfo should be $l_{1}$ , which is not necessary larger than the types when the caller has neither p nor q (e.g. the type for the enabled set ${q}$ is H). The choice of R1 taken in [3] appears to be a design decision: they cited in [3] the lack of motivating examples for non-monotonic policies, and suggested that to accommodate such policies one might need to consider a notion of declassification. As we have seen, however, non-monotonic policies can arise naturally in mobile applications. In a study on Android malwares [17], Enck et al. identify several combinations of permissions that are potentially ‘dangerous’, in the sense that they allow potentially unsafe information flow. An information flow policy that requires the absence of such combinations of permissions in information release would obviously be non-monotonic. In general, non-monotonic policies can be required to solve the aggregation problem studied in information flow theory [25], where several pieces of low security level information may be pooled together to learn information at a higher security level.

We therefore designed a more precise type system for information flow under an access control model inspired by the Android framework. Our type system solves the problem of typing non-monotonic policies without resorting to downgrading or declassifying information. The technique we use is to keep information related to both branches of test via a merging operator on security types. Additionally, there is a significant difference between the permission model of Android and that of BN system, where permissions are propagated across method invocations among apps. In Android, permissions are relevant only during inter-process or inter-component calls and are not inherited along the call chains across apps. As we shall see in Section 2.5, this may give rise to a type of attack which we call “parameter laundering” attack if one adopts a naive typing rule for function calls. The soundness proof for our type system is significantly different from that for BN system due to the difference in permission model and the new merging operator on types in our type system.

The contributions of our work are four-fold.

We develop a lightweight type system in which security types are dependent on a permission-based access control mechanism, and prove its soundness with respect to a notion of non-interference (Section 2). A novel feature of the type system is the type merging constructor, used for typing the conditional branch in permission checking, which allows us to model non-monotonic information flow policies.

We identify a problem of explicit flow through function calls in the setting where permissions are not propagated during function calls. This problem arises as a byproduct of Android’s permission model, which is significantly different from that of JVM, and adopting a standard typing rule for function calls such as the one proposed for Java in [3] would lead to unsoundness. We call this problem the parameter laundering problem and we propose a typing rule for function calls that prevents it.

We show that the type inference is decidable for our type system, by reducing it to a constraint solving problem (Section 3).

We give a new way to represent our security types as reduced ordered binary decision diagrams, which generalizes boolean functions to functions mapping boolean formula to a multi-value set. We believe the representation will be efficient in practice.

This paper is an extension of [9]. It first extends the security type system with global variables and proves that it is still sound with respect to non-interference2

Due to space constraints, only the main proofs are presented here, and the other proofs, including the proofs for type inference and representation, can be found in the appendix.

(Section 2). It further revises type inference for global variables and contains the main lemmas for its decidability (Section 3). Finally, it also presents a representation for our types (Section 4).

The rest of the paper is organized as follows. Section 2 presents our security type system and its properties. Section 3 and Section 4 give the type inference for our security type system and the representation for our types, respectively. Section 5 presents related work. And Section 6 concludes the paper and discusses some future work.

2. A secure information flow type system

In this section, we present the proposed information flow type system. Section 2.1 informally discusses a permission-based access control model, which is an abstraction of the permission mechanism used in Android. Section 2.2 and Section 2.3 give the operational semantics of a simple imperative language that includes permission checking constructs based on the abstract permission model. Section 2.4 and Section 2.5 describe the type system for our language and prove its soundness with respect to a notion of non-interference.

2.1. A model of permission-based access control

Instead of taking all the language features and the library dependencies of Android apps into account, we focus on the permission model used in inter-component communications within and across apps. Such permissions are used to regulate access to protected resources, such as device id, location information, contact information, etc.

In Android, an app specifies the permissions it needs at the installation time via a manifest file. In recent versions of Android (since Android 6.0, API level 23), some of these permissions need to be granted by users at runtime. But at no point a permission request is allowed if it is not already specified in the manifest. For now, we assume a permission enforcement mechanism that applies to Android versions prior to version 6.0,3

³
To be specific, runtime permission request requires the compatible version specified in the manifest file to be greater than or equal to API level 23, and running OS should be at least Android 6.0.

so it does not account for permission granting at runtime. Runtime permission granting [1] poses some problems in typing non-monotonic policies; we shall come back to this point later in Section 6.

An Android app may provide services to other apps, or other components within the app itself. Such a service provider may impose permissions on other apps who want to access its services. Communication between apps is implemented through Binder IPC (inter-process communications) [14].

In our model, a program can be seen as a highly abstracted version of an app, and the intention is to show how one can reason about information flows in such a service provider when access control is imposed on the calling app. In the following we shall not model explicitly the IPC mechanism of Android, but will instead model it as a function call. Note that this abstraction is practical since it can be achieved by conventional data and control flow analyses, together with the modeling of Android IPC specific APIs. The feasibility has been demonstrated by frameworks like FlowDroid [2], Amandroid [53], IccTA [26], etc.4

⁴

We have also been implementing a permission-dependent information flow analysis tool on top of Amandroid. The basic idea is similar to the one mentioned in this paper, however the focus is improving the precision of information leakage detection rather than non-interference certification.

One significant issue that has to be taken into account is that the Android framework does not track IPC call chains between apps and permissions of an app are not propagated to the callee. That is, an app A calling another app B does not grant B the permissions assigned to A. This is different from the traditional type systems such as BN where permissions can potentially propagate along the call stacks. Note however that B can potentially have more permissions than A, leading to a potential privilege escalation, a known weakness in Android permission system [10]. Another consequence of lacking transitivity is that in designing the type system, one must be careful to avoid what we call a “parameter laundering” attack (see Section 2.4).

2.2. A language with permission checks

As mentioned earlier, we do not model directly all the language features of an Android app, but use a much simplified language to focus on the permission mechanism part. The language is a variant of the language considered in [52], extended with functions and an operator for permission checks.

We model an app as a collection of functions (services), together with a statically assigned permission set. A system, denoted by $S$ , consists of a set of apps. We use capital letters $A, B, \dots$ to denote apps. A function f defined in an app A is denoted by $A . f$ , and may be called independently of other functions in the same app. The intention is that a function models an application component (i.e., Activity, Service, BroadCastReceiver, and ContentProvider) in Android, which may be called from within the same app or other apps.

We assume that only one function is executed at a time, so we do not model concurrent executions of apps. We think that in the Android setting, considering sequential behavior only is not overly restrictive. This is because the communication between apps are (mostly) done via IPC. Shared states between apps, which is what contributes to the difficulty in concurrency handling, is mostly absent, apart from the very limited sharing of preferences. In such a setting, each invocation of a service can be treated independently as there is usually no synchronization needed between different invocations. Additionally, we assume functions in a system are not (mutually) recursive, so there is a finite chain of function calls from any given function. The absence of recursion is not a restriction, since our functions are supposed to model communications in Android, which are rarely recursive. We denote with P the finite set containing all permissions in the system. Each app is assigned a static set of permissions drawn from this set. The powerset of P is written as $P$ .

For simplicity, we consider only programs manipulating integers, so the expressions in our language all have the integer type. Boolean values are encoded as 0 (false) and any non-zero values (true). The grammar for expressions is given below: $\begin{matrix} e : : = n ∣ x ∣ e op e \end{matrix}$ where n denotes an integer literal, x denotes a variable, and $op$ denotes a binary operation. The commands of the language are given in the following grammar: $\begin{array}{l} c : : = x : = e ∣ if e then c else c ∣ while e do c ∣ c; c \\ ∣ letvar x = e in c ∣ x : = call A . f (\overline{e}) ∣ test (p) c else c \end{array}$ The first four constructs are respectively assignment, conditional, while-loop and sequential composition. The statement “ $letvar x = e in c$ ” is a local variable declaration statement. Here x is declared and initialized to e, and its scope is the command c. We require that x does not occur in e. The statement “ $x : = call A . f (\overline{e})$ ” denotes an assignment whose right hand side is a function call to $A . f$ . The statement “ $test (p) c_{1} else c_{2}$ ” checks whether the calling app has permission p: if it does then $c_{1}$ is executed, otherwise $c_{2}$ is executed. This is similar to the test construct in BN system, except that we allow testing only one permission at a time. This is a not real restriction since both versions of the test can simulate one another. The set of free variables occurring in an expression e or a command c is defined as follows: $\begin{array}{l} fv (n) = \emptyset fv (if e then c_{1} else c_{2}) = fv (e) \cup fv (c_{1}) \cup fv (c_{2}) \\ fv (x) = {x} fv (while e do c) = fv (e) \cup fv (c) \\ fv (e_{1} op e_{2}) = fv (e_{1}) \cup fv (e_{2}) fv (letvar x = e in c) = (fv (e) \cup fv (c)) ∖ {x} \\ fv (x : = e) = {x} \cup fv (e) fv () x : = call A . f (\overline{e}) = {x} \cup ⋃_{e_{i} \in \overline{e}} fv (e_{i}) \\ fv (c_{1}; c_{2}) = fv (c_{1}) \cup fv (c_{2}) fv (test (p) c_{1} else c_{2}) = fv (c_{1}) \cup fv (c_{2}) \end{array}$

A function declaration has the following syntax: $\begin{matrix} F : : = A . f (\overline{x}) {init r = 0 in {c; return r}} \end{matrix}$ where $A . f$ is the name of the function, $\bar{x}$ are function parameters, c is a command and r is a local variable that holds the return value of the function. The variables $\overline{x}$ and r are bound variables with the command “ $c; return r$ ” in their scopes. The set of free variables occurring a function f is defined as follows: $\begin{matrix} fv (A . f (\overline{x}) {init r = 0 in {c; return r}}) = fv (c) ∖ ({x_{i} | x_{i} \in \overline{x}} \cup {r}) \end{matrix}$

Given a system $S$ , we call the free variables occurring in $S$ as global variables, i.e., the variables that are neither introduced by letvar nor from the variable set ${\overline{x}, r}$ of any function in $S$ . Global variables can be used to model the shared preference between apps. Formally, the global variables of $S$ is defined as follows: $\begin{matrix} gv (S) = ⋃_{A \in S} fv (A) = ⋃_{A \in S} ⋃_{A . f \in A} fv (A . f) \end{matrix}$ The others, i.e., the variables that are either introduced by letvar or from the variable set $x, r$ of any function in $S$ , are called local variables. To simplify presentation, we assume that (1) variables in a system are named differently so there are no naming clashes between them; and (2) the variable x in $x : = call A . f (\overline{e})$ is not a global one, since we can encode $x_{g} : = call A . f (\overline{e})$ as $letvar x_{l} = 0 in x_{l} : = call A . f (\overline{e}); x_{g} : = x_{l}$ , where $x_{g}$ is a global variable and $x_{l}$ is a fresh local variable.

Fig. 1.

Evaluation rules for expressions and commands, given a function definition table $FD$ and a permission assignment Θ.

2.3. Operational semantics

Given a system $S$ , we assume that the permission sets assigned to the apps in $S$ are given by a table Θ indexed by app names, and function definitions in $S$ are stored in a table $FD$ indexed by function names.

An evaluation environment is a finite mapping from variables to values (i.e., integers). We denote with $EEnv$ the set of evaluation environments. Elements of $EEnv$ are ranged over by η. We use the notation $[x_{1} \mapsto v_{1}, \dots, x_{n} \mapsto v_{n}]$ to denote an evaluation environment mapping variable $x_{i}$ to value $v_{i}$ ; this will sometimes be abbreviated as $[\overline{x} \mapsto \overline{v}]$ . The domain of $η = [x_{1} \mapsto v_{1}, \dots, x_{n} \mapsto v_{n}]$ (i.e., ${x_{1}, \dots, x_{n}}$ ) is denoted by $dom (η)$ . Given two environments $η_{1}$ and $η_{2}$ , we define $η_{1} η_{2}$ as an environment η such that $η (x) = η_{2} (x)$ if $x \in dom (η_{2})$ , otherwise $η (x) = η_{1} (x)$ . For example, $η [x \mapsto v]$ maps x to v, and y to $η (y)$ for any $y \in dom (η)$ such that $y \neq x$ . Given a mapping η and a variable x, we write $η - x$ to denote the mapping resulting from removing x from $dom (η)$ . To simplify proofs of various properties, we split the evaluation environment into two parts $(η^{G}, η)$ : one (i.e., $η^{G}$ ) for the global variables and the other (i.e., η) for the non-global ones, and require that $dom (η^{G}) = gv (S)$ .

The operational semantics for expressions and commands is given in Fig. 1. The evaluation judgment for expressions has the form $(η^{G}, η) ⊢ e ⇝ v$ , which states that expression e evaluates to value v when variables in e are interpreted in the evaluation environment $(η^{G}, η)$ . We write $(η^{G}, η) ⊢ \overline{e} ⇝ \overline{v}$ , where $\overline{e} = e_{1}, \dots, e_{n}$ and $\overline{v} = v_{1}, \dots, v_{n}$ for some n, to denote a sequence of judgments $(η^{G}, η) ⊢ e_{1} ⇝ v_{1}, \dots, (η^{G}, η) ⊢ e_{n} ⇝ v_{n}$ .

The evaluation judgment for commands takes the form $(η^{G}, η); A; P ⊢ c ⇝ (η_{1}^{G}, η_{1})$ , where $(η^{G}, η)$ is an evaluation environment before the execution of the command c, and $(η_{1}^{G}, η_{1})$ is the evaluation environment after the execution of c. Here A refers to the app to which the command c belongs. The permission set P denotes the permission context, i.e., it is the set of permissions of the app which invokes the function of A in which the command c resides. The caller app may be A itself (in which case the permission context will be the same as the permission set of A) but more often it is another app in the system.

The operational semantics of most commands are straightforward. We explain the semantics of the test primitive and the function call. Rules (E-CP-T) and (E-CP-F) capture the semantics of the test primitive. These are where the permission context P in the evaluation judgement is used. The semantics of function calls is given by (E-CALL). Notice that c inside the body of callee is executed under the permission context $Θ (A)$ , which is the permission set of A. The permission context P in the conclusion of that rule, which denotes the permission of the app that calls A, is not used in the premise. That is, the permission context of A is not inherited by the callee function $B . f$ . This reflects the way permission contexts in Android are passed on during IPCs [14,15], and is also a major difference between our permission model and that in BN system, where permission contexts are inherited by successive function calls.

2.4. Security types

In information flow type systems such as [52], it is common to adopt a lattice structure to encode security levels. Security types in this setting are just security levels. In our case, we generalize the security types to account for the dependency of security levels on permissions. So we shall distinguish security levels, given by a lattice structure which encodes sensitivity levels of information, and security types, which are mappings from permissions to security levels. We assume the security levels are given by a lattice $L$ , with a partial order $⩽_{L}$ . Security types are defined in the following.

Definition 2.1.
A base security type (or base type) t is a mapping from $P$ to $L$ . We denote with $T$ the set of base types. Given two base types s and t, we say $s = t$ iff $s (P) = t (P)$ for all $P \in P$ . We define an ordering $⩽_{T}$ on base types as follows: $s ⩽_{T} t$ iff ∀ $P \in P$ , $s (P) ⩽_{L} t (P)$ .

As we shall see, if a variable is typed by a base type, the sensitivity of its content may depend on the permissions of the app which writes to the variable. In contrast, in traditional information flow type systems, a variable annotated with a security level has a fixed sensitivity level regardless of the permissions of the app that writes to the variable.

Next, we show that the set of base types with the order $⩽_{T}$ forms a lattice.
Definition 2.2.
For $s, t \in T$ , $s ⊔ t$ and $s ⊓ t$ are defined as $\begin{matrix} (s ⊔ t) (P) = s (P) ⊔ t (P), \forall P \in P (s ⊓ t) (P) = s (P) ⊓ t (P), \forall P \in P \end{matrix}$
Lemma 2.1.
$⩽_{T}$ is a partial order relation on $T$ .
Lemma 2.2.
$(T, ⩽_{T})$ forms a lattice.

From now on, we shall drop the subscripts in $⩽_{L}$ and $⩽_{T}$ when no ambiguity arises.

Accordingly, a security level l can be lifted to the base type $\hat{l}$ that maps all permission sets to level l itself, which we call as a level type.
Definition 2.3.
Given a security level l, we define $\hat{l}$ as follows: for all $P \in P$ , we have $\hat{l} (P) = l$ .
Definition 2.4.
A function type has the form $\overline{t} \overset{s}{\to} t$ , where $\overline{t} = (t_{1}, \dots, t_{m})$ , $m ⩾ 0$ and $t, s, t_{i}$ are base types. The types $\overline{t}$ are the types for the arguments of the function, t is the return type of the function, and s is the type for the body of the function.

In our type system, security types of expressions (commands, functions, resp.) may be altered depending on the execution context. That is, when an expression is used in a context where a permission check has been performed (either successfully or unsuccessfully), its type may be adjusted to take into account the presence or absence of the checked permission. Such an adjustment is called a promotion or a demotion. Definition 2.5.
Given a permission p, the promotion and demotion of a base type t with respect to p are: $\begin{array}{l} (t ↑_{p}) (P) = t (P \cup {p}), \forall P \in P (promotion) \\ (t ↓_{p}) (P) = t (P ∖ {p}), \forall P \in P (demotion) \end{array}$ The promotion and demotion of a function type $\overline{t} \overset{s}{\to} t$ , where $\overline{t} = (t_{1}, \dots, t_{m})$ , are respectively: $\begin{matrix} (\overline{t} \overset{s}{\to} t) ↑_{p} = \overline{t} ↑_{p} \overset{s ↑_{p}}{\to} t ↑_{p} (\overline{t} \overset{s}{\to} t) ↓_{p} = \overline{t} ↓_{p} \overset{s ↓_{p}}{\to} t ↓_{p} \end{matrix}$ where $\overline{t} ↑_{p} = (t_{1} ↑_{p}, \dots, t_{m} ↑_{p})$ and $\overline{t} ↓_{p} = (t_{1} ↓_{p}, \dots, t_{m} ↓_{p})$ .
Lemma 2.3.
Given $P \in P$ and $p \in P$ , (a) $(t ↑_{p}) (P) = t (P)$ if $p \in P$ ; and (b) $(t ↓_{p}) (P) = t (P)$ if $p \notin P$ .

2.5. Security type system

We first define a couple of operations on security types and permissions that will be used later.

A function called by different callers may have different the permission contexts, so we define type projection to extract types according to the permission sets of callers.

Definition 2.6.
Given $t \in T$ and $P \in P$ , the projection of t on a permission set P is a security type $π_{P} (t)$ defined as $π_{P} (t) (Q) = t (P), \forall Q \in P$ . Type projection of a list of types on P is then written as $π_{P} ((t_{1}, \dots, t_{n})) = (π_{P} (t_{1}), \dots, π_{P} (t_{n}))$ .

In order to type the permission check $test (p) c_{1} else c_{2}$ precisely, we need to construct a type t from the types $t_{1}, t_{2}$ respectively for its two branches $c_{1}, c_{2}$ , such that t acts like $t_{1}$ ( $t_{2}$ resp.) when p is enabled (disabled resp.).
Definition 2.7.
Given a permission p and two types $t_{1}$ and $t_{2}$ , the merging of $t_{1}$ and $t_{2}$ along p, denoted as $t_{1} ⊳_{p} t_{2}$ , is: $\begin{matrix} (t_{1} ⊳_{p} t_{2}) (P) = \{\begin{matrix} t_{1} (P) & p \in P \\ t_{2} (P) & p \notin P \end{matrix} \forall P \in P \end{matrix}$

A typing environment is a finite mapping from variables to base types. We use the notation $[x_{1} : t_{1}, \dots, x_{n} : t_{n}]$ to enumerate a typing environment with domain ${x_{1}, \dots, x_{n}}$ . Typing environments are ranged over by Γ. Given $Γ_{1}$ and $Γ_{2}$ such that $dom (Γ_{1}) \cap dom (Γ_{2}) = \emptyset$ , we write $Γ_{1} Γ_{2}$ to denote a typing environment that is the (disjoint) union of the mappings in $Γ_{1}$ and $Γ_{2}$ . Accordingly, we split the typing environment into two parts $Γ^{G}$ and Γ, where $Γ^{G}$ denotes the part for the global variables and Γ denotes the other part for the non-global ones. And we also require that $dom (Γ^{G}) = gv (S)$ .
Definition 2.8.
Given a typing environment Γ, its promotion and demotion along p are typing environments $Γ ↑_{p}$ and $Γ ↓_{p}$ , such that $(Γ ↑_{p}) (x) = Γ (x) ↑_{p}$ and $(Γ ↓_{p}) (x) = Γ (x) ↓_{p}$ for every $x \in dom (Γ)$ . The projection of Γ on $P \in P$ is a typing environment $π_{P} (Γ)$ such that $(π_{P} (Γ)) (x) = π_{P} (Γ (x))$ for each $x \in dom (Γ)$ .

There are three typing judgments in our type system as explained below. All these judgments are implicitly parameterized by a function type table, $FT$ , which maps all function names to function types, and a mapping Θ assigning permission sets to apps.
Expression typing: $(Γ^{G}, Γ) ⊢ e : t$ . This says that under $(Γ^{G}, Γ)$ , the expression e has a base type at most t.

Command typing: $(Γ^{G}, Γ); A ⊢ c : t$ . This means that the command c writes to variables with type at least t, when executed by app A, under the typing environment $(Γ^{G}, Γ)$ .

Function typing: The typing judgment takes the form: $\begin{matrix} Γ^{G} ⊢ B . f (\overline{x}) {init r = 0 in {c; return r}} : \overline{t} \overset{s}{\to} t^{'} \end{matrix}$ where $\overline{x} = (x_{1}, \dots, x_{n})$ and $\overline{t} = (t_{1}, \dots, t_{n})$ for some $n ⩾ 0$ . Functions are polymorphic in the permissions of the caller. Intuitively, this means that each caller of the function above with permission set P “sees” the function as having type $π_{P} (\overline{t}) \overset{π_{P} (s)}{\to} π_{P} (t^{'})$ . That is, if the function is called from another app with permission P, then it expects input of type up to $π_{P} (\overline{t})$ , a return value of type at most $π_{P} (t^{'})$ , and the type for the function body at least $π_{P} (s)$ .
When proving the soundness of our type system, we need to make sure that the system of apps are well-typed in the following sense:
Definition 2.9.
Let $S$ be a system, and let $FD$ , $FT$ , and Θ be its function declaration table, function type table, and permission assignments. We say $S$ is well-typed under a global typing environment $Γ^{G}$ iff for every function $A . f$ , $Γ^{G} ⊢ FD (A . f) : FT (A . f)$ is derivable.

Fig. 2.
Typing rules for expressions, commands and functions.

The typing rules are given in Fig. 2. Most of them are common to information flow type systems [3,46,52] except for T-CP and T-CALL. Note that the types for constants depend on the constants themselves. Taking loc and aid in Section 1 for example, their types are respectively $\hat{l_{1}}$ and $\hat{l_{2}}$ . Also note that in the subtyping rule for commands ( ${T-SUB}_{c}$ ), the security type of the effect of the command can be safely downgraded, since typing for commands keeps track of a lower bound of the write effects of the command. This typing rule for command is standard, see, e.g., [52] for a more detailed discussion.

In T-CP , to type statement $test (p) c_{1} else c_{2}$ , we type $c_{1}$ in a promoted typing environment for a successful permission check on p, and $c_{2}$ in a demoted typing environment for a failed permission check on p. The challenge is how to combine the types of the two premises to obtain the type for the conclusion. One possibility is to force the type of the two premises and the conclusion to be identical (i.e., treat permission check the same as other if-then-else statements and apply T-IF). This, as we have seen in Section 1, leads to a loss in precision of the type for test construct. Instead, we consider a more refined merged type $t_{1} ⊳_{p} t_{2}$ for the conclusion, where $t_{1}$ ( $t_{2}$ resp.) is the type of the left (right resp.) premise. To understand the merged type, consider a scenario where the statement is executed in a context where permission p is present. Then the permission check succeeds and the statement $test (p) c_{1} else c_{2}$ is equivalent to $c_{1}$ . In this case, one would expect that the behavior of $test (p) c_{1} else c_{2}$ would be equivalent to that of $c_{1}$ . This is in fact captured by the equation $(t_{1} ⊳_{p} t_{2}) (P) = t_{1} (P)$ for all P such that $p \in P$ , which holds by definition. A dual scenario arises when p is not in the permissions of the execution context.

In T-CALL , the callee function $B . f$ is assumed to be type checked under the global typing environment $Γ^{G}$ beforehand and its type is given in the FT table. Here the function $B . f$ is called by A so the type of $B . f$ as seen by A should be a projection of the type given in $FT (B . f)$ on the permissions of A (given by $Θ (A)$ ): $π_{Θ (A)} (\overline{t}) \overset{π_{Θ (A)} (s)}{\to} π_{Θ (A)} (t^{'})$ . Therefore the arguments for the function call should be typed as $Γ ⊢ \overline{e} : π_{Θ (A)} (\overline{t})$ and the return type (as viewed by A) should be dominated by the type of x, i.e., $π_{Θ (A)} (t^{'}) ⩽ Γ (x)$ . Finally, the projection of the body type, i.e., the effect of the function call by A, should be propagated to the result type: one can think this is the sequential composition of the function body and the assignment. Due to global variables, we need to accumulate the type (i.e., effects) of the commands in the function body that involves global variables. But to make our presentation simple, we do not separate them from local ones. In addition, note that the execution of a function call depends on the permissions of the caller, but this does not mean the permissions of the caller is passed to the callee.

Attack on global variables. We require that the type of a global variable should be invariant for all permission sets, that is, the global typing environment $Γ^{G}$ is form of $[x_{1} : \hat{l_{1}}, \dots, x_{n} : \hat{l_{n}}]$ , where $x_{i}$ is a global variable, $l_{i}$ is a security level. The reason is that different from non-global variables, there is only one copy for global variables. In other words, all the apps share this unique evaluation environment $η^{G}$ of global variables (e.g., such as the shared preference files), which could easily lead to information leaks via global variables. For example, consider a global variable x with a non-constant type, e.g., $t_{x} = {\emptyset \mapsto L, {p} \mapsto H}$ , and two apps $A, B$ satisfying that A has permission p to access some security information but B does not. Suppose that A would like to get the security information and store in x. As A has p, when running on A, the type for x is $\hat{H}$ . Therefore, the behavior of A is typeable. Consider another situation that B would like to get information from x and store in any variable typed of $\hat{L}$ . Similarly, it is easy to check that the behavior of B is typeable as well. However, if the behavior of A happens before the behavior of B, then there is an information leak, but the whole system is typeable according to the discussion above.

Parameter laundering. It is essential that in Rule T-CALL, the arguments $\overline{e}$ and the return value of the function call are typed according to the projection of $\overline{t}$ and $t^{'}$ on $Θ (A)$ . If they are instead typed with $\overline{t}$ , then there is a potential implicit flow via a “parameter laundering” attack. To see why, consider the following alternative to T-CALL:

Notice that the type of the argument $\overline{e}$ must match the type of the formal parameter of the function $B . f$ . This is essentially what is adopted in BN system for method calls [3].

Listing 3.
An example for parameter laundering issue

Let us consider the example in Listing 3. Let $P = {p}$ and t be the base type $t = {\emptyset \mapsto L, {p} \mapsto H}$ , where L and H are bottom and top levels respectively. Here we assume P_INFO is a sensitive value of security level H that needs to be protected, so function C.getsecret is required to have type $() \overset{t}{\to} t$ . That is, only apps that have the required permission p may obtain the secret value. Suppose the permissions assigned to the apps are given by: $Θ (A) = Θ (B) = \emptyset, Θ (C) = Θ (M) = {p}$ . As no global variables occur here, we omit the global environment $Γ^{G}$ .

If we were to adopt the modified T-CALL’ instead of T-CALL, then we can assign the following types to the above functions: $\begin{matrix} FT : = {A . f \mapsto t \overset{\hat{L}}{\to} \hat{L}; B . g \mapsto t \overset{\hat{L}}{\to} \hat{L}; C . g e t s e c r e t \mapsto () \overset{t}{\to} t; M . m a i n \mapsto () \overset{\hat{L}}{\to} \hat{L}} \end{matrix}$ Notice that the return type of $M . m a i n$ is $\hat{L}$ despite having a return value that contains sensitive value P_INFO. If we were to use T-CALL’ in place of T-CALL, the above functions can be typed as shown in Fig. 3. Finally, still assuming T-CALL’, a partial typing derivation for $M . m a i n$ is given in Fig. 4.

Fig. 3.
Typing derivations for functions A.f, B.g and C.getsecret.

Fig. 4.
A typing derivation for function M.main.

As shown in Fig. 3, B.g can be given type $t \overset{\hat{L}}{\to} \hat{L}$ . Intuitively, it checks that the caller has permission p. If it does, then B.g returns 0 (non-sensitive), otherwise it returns the argument of the function (i.e., x). This is as expected and is sound, under the assumption that the security level of the content of x is dependent on the permissions of the caller. If the caller of B.g is the original creator of the content of x, then the assumption is trivially satisfied. The situation gets a bit tricky when the caller simply passes on the content it receives from another app to x. In our example, app A makes a call to B.g, and passes on the value of x it receives. In the run where A.f is called from M.main, the value of x is actually sensitive since it requires the permission p to acquire. However, when it goes through A.f to B.g, the value of x is perceived as non-sensitive by B, since the caller in this case (A) has no permissions. The use of the intermediary A in this case in effect launders the permissions associated with x. Therefore, if the rule T-CALL’ is used in place of T-CALL, the call chain from M.main to A.f and finally to B.g can all be typed. This is correct in a setting where permissions are propagated along with calling context (e.g., [3]) however it is incorrect in the Android permission model 2.1. To avoid the parameter laundering problem, our approach is to make sure that an app may only pass an argument to another function if the app itself is authorized to access the content of the argument in the first place, as formalized in the rule T-CALL.

With the correct typing rule for function calls, the function $A . f$ cannot be assigned type $t \to \hat{L}$ , since that would require the instance of T-CALL (i.e., when making the call to $B . g$ ) in this case to satisfy the constraint $x : t, r : \hat{L} ⊢ x : π_{Θ (A)} (t)$ , where $π_{Θ (A)} (t) = \hat{L}$ , which is impossible since $t ≰ \hat{L}$ . What this means is essentially that in our type system, information received by an app A from the parameters cannot be propagated by A to another app B, unless A is already authorized to access the information contained in the parameter. Note that this only restricts the propagation of such parameters to other apps; the app A can process the information internally without necessarily violating the typing constraints.

Finally, the reader may check that if we fix the type of $B . g$ to $t \overset{\hat{L}}{\to} \hat{L}$ then $A . f$ can only be assigned type $\hat{L} \overset{\hat{L}}{\to} \hat{L}$ . In no circumstances can $M . m a i n$ be typed, since the statement $x_{H} : = C . g e t s e c r e t ()$ forces $x_{H}$ to have type $\hat{H}$ , and thus cannot be passed to $A . f$ as an argument.

Non-monotonic example. Let us consider the example about non-monotonic policy, that is, the function getInfo in Listing 2. Thanks to the rule T-CP, our system is able to capture the non-monotonic policy, so that the function getInfo can be precisely typed in our system, whose typing derivation is given in Fig. 5, where $Γ^{G}$ is omitted for simplicity.

Fig. 5.
Typing derivation for functions A.getInfo in Listing 2.
2.6. Noninterference and soundness

We first define an indistinguishability relation between evaluation environments. Such a definition typically assumes an observer who may observe values of variables at a certain security level. In the non-dependent setting, the security level of the observer is fixed, say at $l_{O}$ , and valuations of variables at level $l_{O}$ or below are required to be identical. In our setting, the security level of a variable in a function can vary depending on the permissions of the caller app (which may be the observer itself), so it may seem more natural to define indistinguishability in terms of the permission set assigned to the caller app. However, we argue that such a definition is subsumed by the more traditional definition that is based on the security level of the observer. Assuming that the observer app is assigned a permission set P, then given two variables $x : t$ and $y : t^{'}$ , the level of information that the observer can access through x and y is at most $t (P) ⊔ t^{'} (P)$ . In general the least upper bound of the security level that an observer with permission P has access to can be computed from the least upper bound of projections (along P) of the types of variables and the return types of functions in the system. In the following definition of indistinguishability, we simply assume that such an upper bound has been computed, and we will not refer explicitly to the permission set of the observer from which this upper bound is derived.

Definition 2.10.
Given two evaluation environments $η, η^{'}$ , a typing environment Γ, a security level $l_{O} \in L$ of the observer, the indistinguishability relation $=_{Γ}^{l_{O}}$ is defined as: $\begin{matrix} η =_{Γ}^{l_{O}} η^{'} iff. \forall x \in dom (Γ) . (Γ (x) ⩽ \hat{l_{O}} \Rightarrow η (x) = η^{'} (x)) \end{matrix}$ where $η (x) = η^{'} (x)$ holds iff both sides of the equation are defined and equal, or both sides are undefined.

Note that in Definition 2.10, η and $η^{'}$ may not have the same domain, but they must agree on their valuations for the variables in the domain of Γ. Note also that since base types are functions from permissions to security level, the security level $l_{O}$ needs to be lifted to a base type in the comparison $Γ (x) ⩽ \hat{l_{O}}$ . The latter implies that $Γ (x) (P) ⩽ l_{O}$ (in the latice $L$ ) for every permission set P. If the base type of each variable assigns the same security level to every permission set (i.e., the security level is independent of the permissions), then our notion of indistinguishability coincides with the standard definition for the non-dependent setting.
Lemma 2.4.
$=_{Γ}^{l_{O}}$ is an equivalence relation on $EEnv$ .

Recall that we assume no (mutual) recursions, so every function call chain in a well-typed system is finite; this is formalized via the rank function below. We will use this as a measure in our soundness proof (Lemma 2.9). $\begin{array}{l} r (if e then c_{1} else c_{2}) = max (r (c_{1}), r (c_{2})) r (x : = e) = 0 \\ r (c_{1}; c_{2}) = max (r (c_{1}), r (c_{2})) r (while e do c) = r (c) \\ r (test (p) c_{1} else c_{2}) = max (r (c_{1}), r (c_{2})) r (letvar x = e in c) = r (c) \\ r (x : = call A . f (\overline{e})) = r (FD (A . f)) + 1 r (A . f (\overline{} x) {init r = 0 in {c; return r}}) = r (c) \end{array}$

The next two lemmas relate projection, promotion/demotion and the indistinguishability relation.
Lemma 2.5.
If $p \in P$ , then $η =_{π_{P} (Γ)}^{l_{O}} η^{'}$ iff $η =_{π_{P} (Γ ↑_{p})}^{l_{O}} η^{'}$ .
Lemma 2.6.
If $p \notin P$ , then $η =_{π_{P} (Γ)}^{l_{O}} η^{'} ⟺ η =_{π_{P} (Γ ↓_{p})}^{l_{O}} η^{'}$ .

The key to the soundness proof is the following two lemmas, which are the analogs to the simple security property and the confinement property in [52].
Lemma 2.7.
Suppose $(Γ^{G}, Γ) ⊢ e : t$ . For $P \in P$ , if $t (P) ⩽ l_{O}$ and $η_{1} =_{π_{P} (Γ)}^{l_{O}} η_{2}$ , $η_{1}^{G} =_{Γ^{G}}^{l_{O}} η_{2}^{G}$ , $(η_{1}^{G}, η_{1}) ⊢ e ⇝ v_{1}$ and $(η_{2}^{G}, η_{2}) ⊢ e ⇝ v_{2}$ , then $v_{1} = v_{2}$ .
Proof.
The proof proceeds by induction on the derivation of $(Γ^{G}, Γ) ⊢ e : t$ . T-VAR-L
We have $(Γ^{G}, Γ) ⊢ x : Γ (x) = t$ and x is non-global. Since $t (P) ⩽ l_{O}$ and $η_{1} =_{π_{P} (Γ)}^{l_{O}} η_{2}$ , it is deducible that $v_{1} = η_{1} (x) = η_{2} (x) = v_{2}$ .
T-VAR-G
We have $(Γ^{G}, Γ) ⊢ x : Γ^{G} (x) = t$ and x is global. Since $t (P) ⩽ l_{O}$ and $Γ^{G} (x)$ is invariant for all permission sets, we have $Γ^{G} (x) ⩽ \hat{l_{O}}$ . Then from $η_{1}^{G} =_{Γ^{G}}^{l_{O}} η_{2}^{G}$ , we get $v_{1} = η_{1}^{G} (x) = η_{2}^{G} (x) = v_{2}$ .
T-OP
We have the typing derivation

and the evaluations

By induction on $e_{i}$ , we can get $v_{1 i} = v_{2 i}$ . Therefore $v_{1} = v_{2}$ .
${T-SUB}_{e}$
we have

since $s (P) ⩽ t (P)$ and $t (P) ⩽ l_{O}$ , then $s (P) ⩽ l_{O}$ as well, thus the result follows by induction on $(Γ^{G}, Γ) ⊢ e : s$ .
□
Lemma 2.8.
Suppose $(Γ^{G}, Γ); A ⊢ c : t$ . Then for any $P \in P$ , if $t (P) ≰ l_{O}$ and $(η^{G}, η); A; P ⊢ c ⇝ (η_{1}^{G}, η_{1})$ , then $η =_{π_{P} (Γ)}^{l_{O}} η_{1}$ and $η^{G} =_{Γ^{G}}^{l_{O}} η_{1}^{G}$ .
Proof.
By induction on the derivation of $(Γ^{G}, Γ); A ⊢ c : t$ , with subinduction on the derivation of $(η^{G}, η); A; P ⊢ c ⇝ (η_{1}^{G}, η_{1})$ . T-ASS-L
In this case x is non-global, $t = Γ (x)$ and the typing derivation has the form:

and the evaluation under $(η^{G}, η)$ takes the form:

That is, $η_{1} = η [x \mapsto v]$ and $η_{1}^{G} = η^{G}$ . So η and $η_{1}$ differ possibly only in the mapping of x. Since $Γ (x) (P) = t (P) ≰ l_{O}$ , that is $π_{P} (Γ) (x) ≰ \hat{l_{O}}$ , the difference in the valuation of x is not observable at level $l_{O}$ . It then follows from Definition 2.10 that $η =_{π_{P} (Γ)}^{l_{O}} η_{1}$ .
T-ASS-G
In this case x is global, $t = Γ^{G} (x)$ and the typing derivation has the form:

and the evaluation under $(η^{G}, η)$ takes the form:

That is, $η_{1} = η$ and $η_{1}^{G} = η^{G} [x \mapsto v]$ . So $η^{G}$ and $η_{1}^{G}$ differ possibly only in the mapping of x. Since $Γ^{G} (x) (P) = t (P) ≰ l_{O}$ and $Γ^{G} (x)$ is invariant for all permission sets, we have $Γ^{G} (x) ≰ \hat{l_{O}}$ . Then the difference in the valuation of x is not observable at level $l_{O}$ . It then follows from Definition 2.10 that $η^{G} =_{Γ^{G}}^{l_{O}} η_{1}^{G}$ .
T-CALL
In this case c has the form $x : = call B . f (\overline{e})$ and the typing derivation takes the form:

and we have that $t = Γ (x) ⊓ π_{Θ (A)} (s_{b})$ . The evaluation under $(η^{G}, η)$ is derived as follows:

where $η_{1} = η [x \mapsto η_{2} (r)]$ and $η_{1}^{G} = η_{2}^{G}$ . Since $t (P) ≰ l_{O}$ , we have $Γ (x) (P) ≰ l_{O}$ and therefore $Γ (x) ≰ l_{O}$ and $η =_{π_{P} (Γ)}^{l_{O}} η [x \mapsto η_{2} (r)]$ , that is, $η =_{π_{P} (Γ)}^{l_{O}} η_{1}$ .

The remaining is to prove $η^{G} =_{Γ^{G}}^{l_{O}} η_{1}^{G}$ . As we consider only well-typed systems, the function $FD (B . f)$ is also typable under $Γ^{G}$ :

From $t (P) ≰ l_{O}$ , we also deduce $π_{Θ (A)} (s_{b}) ≰ l_{O}$ . By induction on $(T_{2})$ and $(T_{1})$ , we get $[\overline{y} \mapsto \overline{v}, r \mapsto 0] =_{π_{Θ (A)} ([\overline{y} : \overline{s}, r : s^{'}])} η_{2}$ and $η^{G} =_{Γ^{G}}^{l_{O}} η_{1}^{G}$ . The latter implies $η^{G} =_{Γ^{G}}^{l_{O}} η_{2}^{G}$ .
T-IF
This follows straightforwardly from the induction hypothesis.
T-WHILE
We look at the case where the condition of the while loop evaluates to true, otherwise it is trivial. In this case the typing derivation is

and the evaluation derivation is

Applying the induction hypothesis (on typing derivation) and the inner induction hypothesis (on the evaluation derivation) we get $η =_{π_{P} (Γ)}^{l_{O}} η_{2}$ and $η^{G} =_{Γ^{G}}^{l_{O}} η_{2}^{G}$ , and then $η_{2} =_{π_{P} (Γ)}^{l_{O}} η_{1}$ and $η_{2}^{G} =_{Γ^{G}}^{l_{O}} η_{1}^{G}$ ; by transitivity of $=_{π_{P} (Γ)}^{l_{O}}$ the result follows.
T-SEQ
This follows from the induction hypothesis and transitivity of the indistinguishability relation.
T-LETVAR
This case follows from the induction hypothesis and the fact that we can choose fresh variables for local variables, and that the local variables are not visible outside the scope of letvar.
T-CP
We have:

There are two possible derivations for the evaluation. In one case, we have

Since $t (P) ≰ l_{O}$ and $p \in P$ , by Definition 2.7, we have $t_{1} (P) ≰ l_{O}$ . By induction hypothesis, we have $η =_{π_{P} (Γ ↑_{p})}^{l_{O}} η_{1}$ and $η^{G} =_{Γ^{G}}^{l_{O}} η_{1}^{G}$ . by Lemma 2.5, we have $η =_{π_{P} (Γ)}^{l_{O}} η_{1}$ .

The case where $p \notin P$ can be handled similarly, making use of Lemma 2.6.
${T-SUB}_{c}$
Straightforward by induction.
□

Before we define the notion of non-interference for a system, we need to define what it means for a command to be non-interferent.
Definition 2.11.
A command c executed in app A is said to be non-interferent iff for all $η_{1}$ , $η_{2}$ , $η_{1}^{G}$ , $η_{2}^{G}$ , Γ, $Γ^{G}$ , P, $l_{O}$ , if $η_{1} =_{π_{P} (Γ)}^{l_{O}} η_{2}$ , $η_{1}^{G} =_{Γ^{G}}^{l_{O}} η_{2}^{G}$ , $(η_{1}^{G}, η_{1}); A; P ⊢ c ⇝ (η_{3}^{G}, η_{3})$ and $(η_{2}^{G}, η_{2}); A; P ⊢ c ⇝ (η_{4}^{G}, η_{4})$ then $η_{3} =_{π_{P} (Γ)}^{l_{O}} η_{4}$ and $η_{3}^{G} =_{Γ^{G}}^{l_{O}} η_{4}^{G}$ .

The main technical lemma is that well-typed commands are non-interferent. Lemma 2.9.
Suppose $(Γ^{G}, Γ); A ⊢ c : t$ , for any $P \in P$ , if $η_{1} =_{π_{P} (Γ)}^{l_{O}} η_{2}$ , $η_{1}^{G} =_{Γ^{G}}^{l_{O}} η_{2}^{G}$ $(η_{1}^{G}, η_{1}); A; P ⊢ c ⇝ (η_{3}^{G}, η_{3})$ , and $(η_{2}^{G}, η_{2}); A; P ⊢ c ⇝ (η_{4}^{G}, η_{4})$ , then $η_{3} =_{π_{P} (Γ)}^{l_{O}} η_{4}$ and $η_{3}^{G} =_{Γ^{G}}^{l_{O}} η_{4}^{G}$ .
Proof.
If $t (P) ≰ l_{O}$ , then according to Lemma 2.8, we have $\begin{matrix} η_{3} =_{π_{P} (Γ)}^{l_{O}} η_{1} =_{π_{P} (Γ)}^{l_{O}} η_{2} =_{π_{P} (Γ)}^{l_{O}} η_{4} and η_{3}^{G} =_{η^{G}}^{l_{O}} η_{1}^{G} =_{Γ^{G}}^{l_{O}} η_{2}^{G} =_{Γ^{G}}^{l_{O}} η_{4}^{G} \end{matrix}$ and thus the lemma follows. In the following, we assume that $t (P) ⩽ l_{O}$ . The proof proceeds by induction on r(c), with subinduction on the derivations of $(Γ^{G}, Γ); A ⊢ c : t$ and $(η_{1}^{G}, η_{1}); A; P ⊢ c ⇝ (η_{3}^{G}, η_{3})$ . In the following, we shall omit the superscript $l_{O}$ from $=_{π_{P} (Γ)}^{l_{O}}$ to simplify presentation. T-ASS-L
In this case, $c \equiv x : = e$ , x is non-global, and the typing derivation takes the form:

where $t = Γ (x)$ , and suppose the two executions of c are derived as follows:

So $η_{3} = η_{1} [x \mapsto v_{1}]$ , $η_{4} = η_{2} [x \mapsto v_{2}]$ , $η_{3}^{G} = η_{1}^{G}$ and $η_{4}^{G} = η_{2}^{G}$ . Note that $η_{3}^{G} =_{Γ^{G}} η_{4}^{G}$ holds trivially. Let us consider $η_{3}$ and $η_{4}$ . As $t (P) ⩽ l_{O}$ , applying Lemma 2.7 to $(η_{1}^{G}, η_{1}) ⊢ e ⇝ v_{1}$ and $(η_{2}^{G}, η_{2}) ⊢ e ⇝ v_{2}$ we get $v_{1} = v_{2}$ , so it then follows that $η_{3} =_{π_{P} (Γ)} η_{4}$ .
T-ASS-G
In this case, $c \equiv x : = e$ , x is global, and the typing derivation takes the form:

where $t = Γ^{G} (x)$ , and suppose the two executions of c are derived as follows:

So $η_{3} = η_{1}$ , $η_{4} = η_{2}$ , $η_{3}^{G} = η_{1}^{G} [x \mapsto v_{1}]$ and $η_{4}^{G} = η_{2}^{G} [x \mapsto v_{2}]$ . Note that $η_{3} =_{π_{P} (Γ)} η_{4}$ holds trivially. Let us consider $η_{3}^{G}$ and $η_{4}^{G}$ . As $t (P) ⩽ l_{O}$ , applying Lemma 2.7 to $(η_{1}^{G}, η_{1}) ⊢ e ⇝ v_{1}$ and $(η_{2}^{G}, η_{2}) ⊢ e ⇝ v_{2}$ we get $v_{1} = v_{2}$ , so it then follows that $η_{3}^{G} =_{Γ^{G}} η_{4}^{G}$ .
T-IF
In this case $c \equiv if e then c_{1} else c_{2}$ and we have

The evaluation derivation under $(η_{1}^{G}, η_{1})$ takes either one of the following forms:

We consider here only the case where $v \neq 0$ ; the case with $v = 0$ can be dealt with similarly. We first need to show that the evaluation of c under $(η_{2}^{G}, η_{2})$ would take the same if-branch. That is, suppose $(η_{2}^{G}, η_{2}) ⊢ e ⇝ v^{'}$ . Since $t (P) ⩽ l_{O}$ , we can apply Lemma 2.7 to conclude that $v^{'} = v \neq 0$ , hence the evaluation of c under $(η_{2}^{G}, η_{2})$ takes the form:

The lemma then follows straightforwardly from the induction hypothesis.
T-WHILE
$c \equiv while e do c_{b}$ and we have

According to Lemma 2.7, if $(η_{1}^{G}, η_{1}) ⊢ e ⇝ v_{1}$ and $(η_{2}^{G}, η_{2}) ⊢ e ⇝ v_{2}$ , then $v_{1} = v_{2}$ . If both are 0 then the conclusion holds according to (E-WHILE-F). Otherwise, we have

Applying the induction hypothesis to $(Γ^{G}, Γ); A ⊢ c_{b} : t$ , $(η_{1}^{G}, η_{1}); A; P ⊢ c_{b} ⇝ (η_{5}^{G}, η_{5})$ and $(η_{2}^{G}, η_{2}); A; P ⊢ c_{b} ⇝ (η_{6}^{G}, η_{6})$ , we obtain $η_{5} =_{π_{P} (Γ)} η_{6}$ and $η_{5}^{G} =_{Γ^{G}} η_{6}^{G}$ . Then applying the inner induction hypothesis to $(η_{5}^{G}, η_{5}); A; P ⊢ while e do c_{b} ⇝ (η_{3}^{G}, η_{3})$ and $(η_{6}^{G}, η_{6}); A; P ⊢ while e do c_{b} ⇝ (η_{4}^{G}, η_{4})$ , we obtain $η_{3} =_{π_{P} (Γ)} η_{4}$ and $η_{3}^{G} =_{Γ^{G}} η_{4}^{G}$ .
T-SEQ
In this case we have $c \equiv c_{1}; c_{2}$ and $(Γ^{G}, Γ); A ⊢ c : t$ . It holds by induction on $c_{1}$ and $c_{2}$ .
T-LETVAR
In this case we have $c \equiv letvar x = e in c_{b}$ . This case follows from the induction hypothesis and the fact that the mapping for the local variable x is removed in $η_{2}$ and $η_{2}^{'}$ .
T-CALL
In this case, c has the form $x : = call B . f (\overline{e})$ . Suppose the typing derivation is the following (where we label the premises for ease of reference later):

where $t = Γ (x) ⊓ π_{Θ (A)} (s_{b})$ , and the executions under $(η_{1}^{G}, η_{1})$ and $(η_{2}^{G}, η_{2})$ are derived, respectively, as follows:

where $FD (B . f) = B . f (\overline{x}) {init r = 0 in {c_{1}; return r}}$ , $η_{3} = η_{1} [x \mapsto η_{5} (r)]$ , $η_{4} = η_{2} [x \mapsto η_{6} (r)]$ , $η_{3}^{G} = η_{5}^{G}$ and $η_{4}^{G} = η_{6}^{G}$ .

Moreover, since we consider only well-typed systems, the function $FD (B . f)$ is also typable:

Let $Γ^{'} = π_{Θ (A)} ([\overline{y} : \overline{s}, r : s^{'}])$ . We first prove several claims:
Claim 1: $[\overline{y} \mapsto \overline{v_{1}}, r \mapsto 0] =_{Γ^{'}} [\overline{y} \mapsto \overline{v_{2}}, r \mapsto 0]$ .

Proof: Let $ρ = [\overline{y} \mapsto \overline{v_{1}}, r \mapsto 0]$ and $ρ^{'} = [\overline{y} \mapsto \overline{v_{2}}, r \mapsto 0]$ . We only need to check that the two mappings agree on mappings of $\overline{y}$ that are of type $⩽ {\hat{l}}_{O}$ . Suppose $y_{u}$ is such a variable, i.e., $Γ^{'} (y_{u}) = u ⩽ {\hat{l}}_{O}$ , and suppose $ρ (y_{u}) = v_{u}$ and $ρ^{'} (y_{u}) = v_{u}^{'}$ for some $y_{u} \in \overline{y}$ . From $(E_{1})$ we have $(η_{1}^{G}, η_{1}) ⊢ e_{u} ⇝ v_{u}$ and from $(E_{2})$ we have $(η_{2}^{G}, η_{2}) ⊢ e_{u} ⇝ v_{u}^{'}$ , and from $(T_{1})$ we have $(Γ^{G}, Γ) ⊢ e_{u} : u$ . Since $u ⩽ {\hat{l}}_{O}$ , applying Lemma 2.7, we get $v_{u} = v_{u}^{'}$ .

Claim 2: $η_{5} =_{Γ^{'}} η_{6}$ and $η_{5}^{G} =_{Γ^{G}} η_{6}^{G}$ .

Proof: From Claim 1, we know that $[\overline{y} \mapsto \overline{v_{1}}, r \mapsto 0] =_{Γ^{'}} [\overline{y} \mapsto \overline{v_{2}}, r \mapsto 0]$ .

If $s_{b} (Θ (A)) ≰ l_{O}$ , similarly, the results follows according to Lemma 2.8. Let us assume $s_{b} (Θ (A)) ⩽ l_{O}$ . Since $r (c_{1}) < r (c)$ , we can apply the outer induction hypothesis to $(E_{2})$ , $(E_{2}^{'})$ and $(T_{3})$ to obtain $η_{5} =_{Γ^{'}} η_{6}$ and $η_{5}^{G} =_{Γ^{G}} η_{6}^{G}$ .

Claim 3: $η_{1} [x \mapsto η_{5} (r)] =_{π_{P} (Γ)} η_{2} [x \mapsto η_{6} (r)]$

Proof: We first note that if $Γ (x) (P) ≰ l_{O}$ , then x is not observable at level $l_{O}$ , and thus the result follows from $η_{1} =_{π_{P} (Γ)} η_{2}$ . Assume that $Γ (x) (P) ⩽ l_{O}$ . From $(T_{2})$ , we get $(π_{Θ (A)} (s^{'})) (P) ⩽ l_{O}$ . The latter, by Definition 2.6, implies that $π_{Θ (A)} (s^{'}) ⩽ \hat{l_{O}}$ . Since $r \in dom (Γ^{'})$ , it is obvious that $η_{5} (r) = η_{6} (r)$ From Claim 2.
The statement we are trying to prove, i.e., $η_{3} =_{π_{P} (Γ)} η_{4}$ and $η_{3}^{G} =_{Γ^{G}} η_{4}^{G}$ , follows immediately from Claim 2 and 3 above.
T-CP
$c \equiv test (p) c_{1} else c_{2}$ and we have

We need to consider two cases, one where $p \in P$ and the other where $p \notin P$ .

Assume that $p \in P$ . Then the evaluation of c under $(η_{1}^{G}, η_{1})$ and $(η_{2}^{G}, η_{2})$ are respectively:

since $p \in P$ , we have $t_{1} (P) = t (P) ⩽ l_{O}$ . Moreover, since $η_{1} =_{π_{P} (Γ)} η_{2}$ , by Lemma 2.5, we have $η_{1} =_{π_{P} (Γ ↑_{p})} η_{2}$ . Therefore by the induction hypothesis applied to $c_{1}$ , we obtain $η_{3} =_{π_{P} (Γ ↑_{p})} η_{4}$ and $η_{3}^{G} =_{Γ^{G}} η_{4}^{G}$ . And by Lemma 2.5, we get $η_{3} =_{π_{P} (Γ)} η_{4}$ .

For the case where $p \notin P$ , we apply a similar reasoning as above, but using Lemma 2.6 in place of Lemma 2.5.
□
Definition 2.12.
Let $S$ be a system with the global typing environment $Γ^{G}$ . A function $\begin{matrix} A . f (\overline{x}) {init r = 0 in {c; return r}} \end{matrix}$ in $S$ with $FT (A . f) = \overline{t} \overset{s}{\to} t^{'}$ is non-interferent iff. for all $η_{1}$ , $η_{2}$ , $η_{1}^{G}$ , $η_{2}^{G}$ , P, v, $l_{O}$ , if the following hold:
$t^{'} (P) ⩽ l_{O}$ ,

$η_{1} =_{π_{P} (Γ)}^{l_{O}} η_{2}$ and $η_{1}^{G} =_{Γ^{G}}^{l_{O}} η_{2}^{G}$ , where $Γ = [\overline{x} : \overline{t}, r : t^{'}]$ ,

$(η_{1}^{G}, η_{1}); A; P ⊢ c ⇝ (η_{3}^{G}, η_{3})$ , and $(η_{2}^{G}, η_{2}); A; P ⊢ c ⇝ (η_{4}^{G}, η_{4})$ ,
then $η_{3} (r) = η_{4} (r)$ and $η_{3}^{G} =_{η^{G}}^{l_{O}} η_{4}^{G}$ . The system $S$ is non-interferent iff all functions in $S$ are non-interferent.
Theorem 2.1.
Well-typed systems are non-interferent.
Proof.
Follows from Lemma 2.9. □

3. Type inference

This section describes a decidable inference algorithm for the language in Section 2.2. Section 3.1 firstly rewrites the typing rules (Fig. 2) in the form of permission trace rules (Fig. 6), then reduces the type inference into a constraint solving problem; Section 3.2 provides procedures to solve the generated constraints.

Fig. 6.

Permission trace rules for expressions, commands and functions.

3.1. Constraint generation

3.1.1. Permission tracing

In an IPC between different apps (components), there may be multiple permission checks in a calling context. Therefore, to infer a security type for an expression, a command or a function, we need to track the applications of promotions $Γ ↑_{p}$ and demotions $Γ ↓_{q}$ in their typing derivations. To this end, we keep the applications symbolic and collect the promotions and demotions into a sequence. In other words, we treat them as a sequence of promotions $↑_{p}$ and demotions $↓_{p}$ applied on a typing environment Γ. For example, $(Γ ↑_{p}) ↓_{q}$ can be viewed as an application of the sequence $↑_{p} ↓_{q}$ on Γ. The sequence of promotions and demotions is called a permission trace and denoted by Λ. The grammar of Λ is: $\begin{matrix} Λ : : = \oplus p : : Λ ∣ ⊖ p : : Λ ∣ ϵ p \in P \end{matrix}$ and its length, denoted by $len (Λ)$ , is defined as: $\begin{matrix} len (Λ) = \{\begin{matrix} 0 & if Λ = ϵ \\ 1 + len (Λ^{'}) & if Λ = ⊚ p : : Λ^{'}, ⊚ \in {\oplus, ⊖} \end{matrix} \end{matrix}$

Definition 3.1.
Given a base type t and a permission trace Λ, the application of Λ to t, denoted by $t \cdot Λ$ , is defined as: $\begin{matrix} t \cdot Λ = \{\begin{matrix} t & if Λ = ϵ \\ (t ↑_{p}) \cdot Λ^{'} & if \exists p, Λ^{'}, s . t . Λ = \oplus p : : Λ^{'} \\ (t ↓_{p}) \cdot Λ^{'} & if \exists p, Λ^{'}, s . t . Λ = ⊖ p : : Λ^{'} \end{matrix} \end{matrix}$

We also extend the application of a permission trace Λ to a typing environment Γ (denoted by $Γ \cdot Λ$ ), such that $\forall x . (Γ \cdot Λ) (x) = Γ (x) \cdot Λ$ . Based on permission traces, we give the definition of partial subtyping relation.
Definition 3.2.
The partial subtyping relation $⩽_{Λ}$ , which is the subtyping relation applied on the permission trace, is defined as $s ⩽_{Λ} t iff. s \cdot Λ ⩽ t \cdot Λ$ .

The application of permission traces to types preserves the subtyping relation.
Lemma 3.1.
$\forall s, t \in T$ , $s ⩽ t ⟹ s ⩽_{Λ} t$ for all Λ.

The following four lemmas discuss the impact of permission checking order on the same or different permissions.
Lemma 3.2.
$\forall t \in T$ , $p, q \in P$ s.t. $p \neq q$ , $t \cdot (⊚ p ⊛ q) = t \cdot (⊛ q ⊚ p)$ , where $⊚, ⊛, \in {\oplus, ⊖}$ .
Lemma 3.3.
$\forall t \in T$ , $(t \cdot ⊚ p) \cdot Λ = (t \cdot Λ) \cdot ⊚ p$ , where $⊚ \in {\oplus, ⊖}$ and $p \notin Λ$ .
Lemma 3.4.
$\forall t \in T$ , $p \in P$ , $(t \cdot ⊚ p) \cdot ⊛ p = t \cdot (⊚ p)$ , where $⊚, ⊛ \in {\oplus, ⊖}$ .
Lemma 3.5.
$\forall t \in T$ , $(t \cdot Λ) \cdot Λ = t \cdot Λ$ .

Lemmas 3.2 and 3.3 state that the order of applications of promotions and demotions on different permissions does not affect the result, which enables us to solve the constraints in any order (see Section 3.2). Lemmas 3.4 and 3.5 indicate that only the first application takes effect if there exist several (consecutive) applications of promotions and demotions on the same permission p. Therefore, we can safely keep only the first application, by removing the other applications on the same permission.

Let $occur (p, Λ)$ be the number of occurrences of p in Λ. We say Λ is consistent iff. $occur (p, Λ) \in {0, 1}$ for all $p \in P$ . According to Lemmas 3.4 and 3.5, we can safely assume that all permission traces are consistent; we do so from now on. Moreover, to ensure that the traces collected from the derivations of commands are consistent, we assume that in nested permission checks of a function definition, each permission is checked at most once.
Lemma 3.6.
$\forall s, t \in T . \forall p \in P . (s ⊳_{p} t) \cdot Λ = (s \cdot Λ) ⊳_{p} (t \cdot Λ)$ , where $p \notin Λ$ .

Lemma 3.6 states the application of trace Λ and the merging along p are orthogonal if $p \notin Λ$ . And the following lemma (Lemma 3.7) indicates the subtyping checking can be divided into two cases: one applied by $\oplus p$ and the other applied by $⊖ p$ . Lemma 3.7.
$\forall s, t \in T . \forall p \in P$ . $s ⩽ t ⟺ s \cdot \oplus p ⩽ t \cdot \oplus p$ and $s \cdot ⊖ p ⩽ t \cdot ⊖ p$ .

3.1.2. Permission trace rules

We keep the applications of the promotions and demotions symbolically (i.e., representing the applications as combinations of typing environments and permission traces), and move the subsumption rules (guarded by permission traces) for expressions and commands to where they are needed. This yields the syntax-directed typing rules given in Fig. 6, which we call the permission trace rules and mark with a subscript $tr$ (i.e., $⊢_{tr}$ ). The judgments of the trace rules are similar to those of typing rules, except that each trace rule is guarded by the permission trace Λ collected from the context, which keeps track of the adjustments of non-global variables depending on the permission checks, and that the subtyping relation in the trace rules is the partial subtyping one $⩽_{Λ}$ .

Next, we show the trace rules are sound and complete with respect to the typing rules, that is, an expression (command, function, resp.) is typeable under the trace rules, if and only if it is typeable under the typing rules.

Lemma 3.8.

If $Γ^{G}; Γ; Λ ⊢_{tr} e : t$ , then $(Γ^{G}, Γ \cdot Λ) ⊢ e : (t \cdot Λ)$ .

If $Γ^{G}; Γ; Λ; A ⊢_{tr} c : t$ , then $(Γ^{G}, Γ \cdot Λ); A ⊢ c : (t \cdot Λ)$ .

If $Γ^{G} ⊢_{tr} B . f (\overline{x}) {init r = 0 in {c; return r}} : \overline{t} \overset{s}{\to} t^{'}$ , then $Γ^{G} ⊢ B . f (\overline{x}) {init r = 0 in {c; return r}} : \overline{t} \overset{s}{\to} t^{'}$ .

Lemma 3.9.

If $(Γ^{G}, Γ \cdot Λ) ⊢ e : t \cdot Λ$ , then there exists s such that $Γ^{G}; Γ; Λ ⊢_{tr} e : s$ and $s ⩽_{Λ} t$ .

If $(Γ^{G}, Γ \cdot Λ); A ⊢ c : t \cdot Λ$ , then there exists s such that $Γ^{G}; Γ; Λ; A ⊢_{tr} c : s$ and $t ⩽_{Λ} s$ .

If $Γ^{G} ⊢ B . f (\overline{x}) {init r = 0 in {c; return r}} : \overline{t} \overset{s_{b}}{\to} s$ , then $Γ^{G} ⊢_{tr} B . f (\overline{x}) {init r = 0 in {c; return r}} : \overline{t} \overset{s_{b}}{\to} s$ .

3.1.3. Constraint generation rules

To infer types for functions in System $S$ , we assign a function type $\overline{α} \overset{γ}{\to} β$ for each function $A . f$ whose type is unknown and a type variable $γ_{x}$ for each variable x with unknown type respectively, where $\overline{α}, β, γ, γ_{x}$ are fresh type variables. And we mark the type variables for global variables with superscripts. Then according to permission trace rules, we try to build a derivation for each function in $S$ , in which we collect the side conditions (i.e., the partial subtyping relation $⩽_{Λ}$ ) needed by the rules. If the side conditions hold under a context, then $FD (A . f)$ is typed by $FT (A . f)$ under the same context for each function $A . f$ in $S$ .

To describe the side conditions (i.e., $⩽_{Λ}$ ), we define the permission guarded constraints as follows: $\begin{array}{l} c : : = (Λ, LHS ⩽ RHS) \\ LHS : : = α ∣ α^{G} ∣ t_{g} ∣ LHS ⊔ LHS ∣ π_{P} (LHS) \\ RHS : : = α ∣ α^{G} ∣ t_{g} ∣ RHS ⊓ RHS ∣ RHS ⊳_{p} RHS ∣ π_{P} (RHS) \end{array}$ where Λ is a permission trace, $α, α^{G}$ are fresh type variables for non-global and global variables respectively, and $t_{g}$ is a ground type.

A type substitution is a finite mapping from type variables to security types: $\begin{matrix} θ : : = ϵ ∣ α \mapsto t, θ ∣ α^{G} \mapsto \hat{l}, θ \end{matrix}$

Definition 3.3.
Given a constraint set C and a substitution θ, we say θ is a solution to C, denoted by $θ ⊨ C$ , iff. for each $(Λ, t_{l} ⩽ t_{r}) \in C$ , $t_{l} θ ⩽_{Λ} t_{r} θ$ holds.

The constraint generation rules are presented in Fig. 7, where each rule is marked with a subscript $cg$ (i.e., $⊢_{cg}$ ), and ${FT}_{C}$ is the extended function type table such that ${FT}_{C}$ maps all function names to function types and their corresponding constraint sets. The judgments of the constraint rules are similar to those of trace rules, except that each rule generates a constraint set C, which consists of the side conditions needed by the typing derivation of $S$ . In addition, as the function call chains starting from a command are finite, the constraint generation will terminate.

Fig. 7.
Constraint generation rules for expressions, commands and functions, given function type table ${FT}_{C}$ .

Next, we show the constraint rules are sound and complete with respect to permission trace rules, that is, the constraint set generated by the derivation of an expression (command, function, resp.) under the constraint rules is solvable, if and only if an expression (command, function, resp.) is typable under trace rules.
Lemma 3.10.
The following statements hold:
If $Γ^{G}; Γ; Λ ⊢_{cg} e : t ⇝ C$ and $θ ⊨ C$ , then $Γ^{G} θ; Γ θ; Λ ⊢_{tr} e : t θ$ .

If $Γ^{G}; Γ; Λ; A ⊢_{cg} c : t ⇝ C$ and $θ ⊨ C$ , then $Γ^{G} θ; Γ θ; Λ; A ⊢_{tr} c : t θ$ .

If $Γ^{G} ⊢_{cg} B . f (x) {init r = 0 in {c; return r}} : \overline{α} \overset{γ}{\to} β ⇝ C$ and $θ ⊨ C$ , then $Γ^{G} θ ⊢_{tr} B . f (x) {init r = 0 in {c; return r}} : \overline{θ (α)} \overset{θ (γ)}{\to} θ (β)$ .

Lemma 3.11.
The following statements hold:
If $Γ^{G}; Γ; Λ ⊢_{tr} e : t$ , then there exist $Γ_{1}, Γ_{1}^{G}, s, C, θ$ such that $Γ_{1}^{G}; Γ_{1}; Λ ⊢_{cg} e : s ⇝ C$ , $θ ⊨ C$ , $Γ_{1} θ = Γ$ , $Γ_{1}^{G} θ = Γ^{G}$ and $s θ = t$ .

If $Γ^{G}; Γ; Λ; A ⊢_{tr} c : t$ , then there exist $Γ_{1}, Γ_{1}^{G}, s, C, θ$ such that $Γ_{1}^{G}; Γ_{1}; Λ; A ⊢_{cg} c : s ⇝ C$ , $θ ⊨ C$ , $Γ_{1} θ = Γ$ , $Γ_{1}^{G} = Γ^{G}$ , and $s θ = t$ .

If $Γ^{G} ⊢_{tr} B . f (\overline{x}) {init r = 0 in {c; return r}} : \overline{t_{p}} \overset{t_{b}}{\to} t_{r}$ , then there exist $Γ_{1}^{G}, \overline{α}, β, γ, C, θ$ such that $Γ_{1}^{G} ⊢_{cg} B . f (\overline{x}) {init r = 0 in {c; return r}} : \overline{α} \overset{γ}{\to} β ⇝ C$ , $θ ⊨ C$ , $Γ_{1}^{G} θ = Γ^{G}$ , and $(\overline{α} \overset{γ}{\to} β) θ = \overline{t_{p}} \overset{t_{b}}{\to} t_{r}$ , where $α, β, γ$ are fresh type variables.

Listing 4.
The example in Listing 2 in a calling context

Recall the function getInfo in Listing 2 and assume that getInfo is defined in app A (thus A.getInfo) and called by app B through the function fun (thus B.fun). The rephrased program is shown in Listing 4, where $l_{1}, l_{2}$ are the types for loc and aid respectively, $Θ (B) = {q}$ , and $l_{1} ⊔ l_{2} = H$ . Let us apply the constraint generation rules in Fig. 7 on each function, yielding the constraint sets $C_{A}$ and $C_{B}$ 5
⁵
If we split the types for commands into global ones and non-global ones, we could have simpler constraints.

$\begin{array}{l} \begin{matrix} C_{A} & = {(\oplus p \oplus q, \hat{l_{1}} ⩽ α), (\oplus p ⊖ q, \hat{L} ⩽ α), (⊖ p \oplus q, \hat{H} ⩽ α), (⊖ p ⊖ q, \hat{L} ⩽ α), \\ (ϵ, α_{b} ⩽ (α ⊳_{q} α) ⊳_{p} (α ⊳_{q} α))} \end{matrix} \\ \begin{matrix} C_{B} & = {(ϵ, \hat{L} ⩽ γ), (\oplus p, \hat{L} ⩽ β), (⊖ p, π_{Θ (B)} (α) ⩽ γ), (ϵ, \hat{L} ⩽ β), (ϵ, γ ⩽ β ⊓ β), \\ (ϵ, β_{b} ⩽ (β ⊳_{p} (γ ⊓ π_{Θ (B)} (α_{b}))) ⊓ (β ⊓ β))} \end{matrix} \end{array}$ and the types $t_{A} = () \overset{α_{b}}{\to} α$ and $t_{B} = () \overset{β_{b}}{\to} β$ for the functions getInfo and fun6
⁶
Indeed, the constraint set for fun is $C_{A} \cup C_{B}$ , but here we focus on the constraints generated by the function itself.

respectively. Thus, the constraint set $C_{eg}$ for the whole program is $C_{A} \cup C_{B}$ .
3.2. Constraint solving

To start with, we present the interpretation and the difference on traces that are needed for constraint solving. A permission trace Λ is a property on permission sets and can be interpreted as a set of permission sets. Formally, the interpretation of Λ is $\begin{matrix} I (Λ) = {P ∣ \forall \oplus p \in Λ . p \in P and \forall ⊖ p \in Λ . p \notin P} \end{matrix}$ We said a permission trace Λ is satisfiable, denoted by $Δ (Λ)$ , iff. $I ($ Λ $) \neq \emptyset$ ; and a permission set P entails Λ, denoted by $P ⊨ Λ$ , iff. $P \in I (Λ)$ . We write $Λ_{P}$ for the permission trace that only P can entail (i.e., $I (Λ_{P}) = {P}$ ). Given two traces $Λ_{1}, Λ_{2}$ , the difference of $Λ_{1}$ from $Λ_{2}$ , denoted by $dif (Λ_{1}, Λ_{2})$ , is the trace consisting of the promotions and demotions in $Λ_{1}$ but not in $Λ_{2}$ . For example, $dif (\oplus p ⊖ q \oplus r, ⊖ q \oplus l) = \oplus p \oplus r$ .

We now present an algorithm for solving the constraints generated by the rules in Fig. 7. For these constraints, both types appearing on the two sides of subtyping are guarded by the same permission trace. But during the process of solving these constraints, new constraints, whose two sides of subtyping are guarded by different traces, may be generated. Take the constraint $(Λ, π_{P} (t_{l}) ⩽ π_{Q} (α))$ for example, $t_{l}$ is indeed guarded by $Λ_{P}$ while α is guarded by $Λ_{Q}$ , where P and Q are different permission sets. So for constraint solving, we use a generalized version of the permission guarded constraints, allowing types on the two sides to be guarded by different permission traces: $((Λ_{l}, t_{l}) ⩽ (Λ_{r}, t_{r}))$ , where $t_{l} \neq t_{r}$ . Likewise, a solution to a generalized constraint set C is a substitution θ, denoted by $θ ⊨ C$ , such that for each $((Λ_{l}, t_{l}) ⩽ (Λ_{r}, t_{r})) \in C$ , $(t_{l} θ \cdot Λ_{l}) ⩽_{} (t_{r} θ \cdot Λ_{r})$ holds.

It is easy to transform a permission guarded constraint set C into a generalized constraint set $C^{'}$ : by rewriting each $(Λ, t_{l} ⩽ t_{r})$ as $((Λ, t_{l}) ⩽ (Λ, t_{r}))$ . Moreover, it is trivial that $θ ⊨ C ⟺ θ ⊨ C^{'}$ . Therefore, we focus on solving generalized constraints in the following. For example, the constraint set $C_{eg}$ can be rewritten as follows, where the first two lines are from $C_{A}$ while the last two lines from $C_{B}$ : $\begin{matrix} C_{eg} & = {((\oplus p \oplus q, \hat{l_{1}}) ⩽ (\oplus p \oplus q, α)), ((\oplus p ⊖ q, \hat{L}) ⩽ (\oplus p ⊖ q, α)), \\ ((⊖ p \oplus q, \hat{H}) ⩽ (⊖ p \oplus q, α)), \\ ((⊖ p ⊖ q, \hat{L}) ⩽ (⊖ p ⊖ q, α)), ((ϵ, α_{b}) ⩽ (ϵ, (α ⊳_{q} α) ⊳_{p} (α ⊳_{q} α))), \\ ((ϵ, \hat{L}) ⩽ (ϵ, γ)), ((\oplus p, \hat{L}) ⩽ (\oplus p, β)), ((⊖ p, π_{Θ (B)} (α)) ⩽ (⊖ p, γ)), ((ϵ, \hat{L}) ⩽ (ϵ, β)), \\ ((ϵ, γ) ⩽ (ϵ, β ⊓ β)), ((ϵ, β_{b}) ⩽ (ϵ, (β ⊳_{p} (γ ⊓ π_{Θ (B)} (α_{b}))) ⊓ (β ⊓ β)))} \end{matrix}$

The constraint solving consists of three steps: 1) decompose types in constraints into ground types and type variables; 2) saturate the constraint set by the transitivity of the subtyping relation; 3) solve the final constraint set by merging the lower and upper bounds of same variables and unifying them to emit a solution.

3.2.1. Decomposition

The first step is to decompose the types into the simpler ones, namely, type variables and ground types, according to their structures. This decomposition is formalized as the decomposing rules, which are given in Fig. 8. Rules (CD-CUP), (CD-CAP), (CD-SVAR) and ( ${CD-MEGER}_{0}$ )7

⁷
Rule ( ${CD-MEGER}_{0}$ ) is not necessary but can simplify the constraints as shown in the illustrated example.

are trivial. Rule (

{CD-MEGER}_{1}

) states that two p-merged types satisfy the relation if and only if both their p-promotions and p-demotions satisfy the relation, where t can be viewed as a p-merged type

t ⊳_{p} t

. The projection of types yields a “monomorphic type” such that any successive trace application makes no changes, therefore we have (CD-LAPP) and (CD-RAPP). Rules (

{CD-SUB}_{0}

) and (

{CD-SUB}_{1}

) handle the constraints on ground types, where ⊥ denotes the failure case. Let dec be the procedure for the constraint decomposition.

Fig. 8.

Constraint solving rules, including decomposition (CD-) and saturation (CS-).

After decomposition, constraints have one of the forms: $\begin{matrix} ((Λ_{l}, α) ⩽ (Λ_{r}, t_{g})), ((Λ_{l}, t_{g}) ⩽ (Λ_{r}, β)), ((Λ_{l}, α) ⩽ (Λ_{r}, β)) \end{matrix}$ Considering the constraint set $C_{eg}$ , these are four constraints that need to be decomposed. Take the constraint $((ϵ, β_{b}) ⩽ (ϵ, (β ⊳_{p} (γ ⊓ π_{Θ (B)} (α_{b}))) ⊓ (β ⊓ β)))$ for example, where $Θ (B) = {q}$ . Rules (CD-CAP), ( ${CD-MEGER}_{1}$ ), and (CD-RAPP) are performed, yielding ${((ϵ, β_{b}) ⩽ (ϵ, β)), ((⊖ p, β_{b}) ⩽ (⊖ p, γ)), ((⊖ p, β_{b}) ⩽ (⊖ p \oplus q, α_{b})), ((\oplus p, β_{b}) ⩽ (\oplus p, β))}$ . After decomposing, $C_{eg}$ becomes $\begin{array}{l} {((\oplus p \oplus q, \hat{l_{1}}) ⩽ (\oplus p \oplus q, α)), ((\oplus p ⊖ q, \hat{L}) ⩽ (\oplus p ⊖ q, α)), ((⊖ p \oplus q, \hat{H}) ⩽ (⊖ p \oplus q, α)), \\ ((⊖ p ⊖ q, \hat{L}) ⩽ (⊖ p ⊖ q, α)), ((ϵ, α_{b}) ⩽ (ϵ, α)), ((ϵ, \hat{L}) ⩽ (ϵ, γ)), ((\oplus p, \hat{L}) ⩽ (\oplus p, β)), \\ ((⊖ p \oplus q, α) ⩽ (⊖ p, γ)), ((ϵ, \hat{L}) ⩽ (ϵ, β)), ((ϵ, γ) ⩽ (ϵ, β)), ((ϵ, β_{b}) ⩽ (ϵ, β)), \\ ((⊖ p, β_{b}) ⩽ (⊖ p, γ)), ((⊖ p, β_{b}) ⩽ (⊖ p \oplus q, α_{b})), ((\oplus p, β_{b}) ⩽ (\oplus p, β))} \end{array}$

3.2.2. Saturation

Considering a variable α, to ensure any lower bound (e.g., $((Λ_{l}, t_{l}) ⩽ (Λ_{1}, α))$ ) is “smaller” than any of its upper bound (e.g., $((Λ_{2}, α) ⩽ (Λ_{r}, t_{r}))$ ), we need to saturate the constraint set by adding these conditions. However, since our constraints are guarded by permission traces, we need to consider lower-upper bound relations only when the traces of the variable α can be entailed by the same permission set, namely, the intersection of their interpretations are not empty. In that case, we extend the traces of both the lower and upper bound constraints such that the traces of α are the same (i.e., $Λ_{1} : : Λ_{2}$ 8

⁸
It should be $Λ_{1} : : dif (Λ_{1}, Λ_{2})$ or $Λ_{2} : : dif (Λ_{2}, Λ_{1})$ . But thanks to Lemmas 3.4 and 3.2, we assume the duplicated promotions and demotions can be removed implicitly and the remaining promotions and demotions can be reordered if needed. Here we write $Λ_{1} : : Λ_{2}$ for short.

), by adding the missing traces (i.e.,

dif (Λ_{1} : : Λ_{2}, Λ_{1})

for lower bound constraint while

dif (Λ_{1} : : Λ_{2}, Λ_{2})

for the upper one). This is done by the saturation rule (i.e., CS-LU in Fig. 8). Let sat be the procedure for the constraint saturation.

Assume that there is an order < on type variables and the smaller variable has a higher priority. If two variables $α, β$ with $α < β$ are in the same constraint $β ⩽ α$ (or $α ⩽ β$ ), we consider the variable β with the larger order is a bound for the variable α with the smaller order during constraint solving, but not vice-versa. There is a special case where both variables on two sides are the same, e.g., $((Λ, α) ⩽ (Λ^{'}, α))$ . In that case, we regroup all the traces of the variable α as the trace set ${Λ_{i} ∣ i \in I}$ such that the set is full (i.e., $⋃_{i \in I} I (Λ_{i}) = P$ ) and disjoint (i.e., $\forall i, j \in I . i \neq j \Rightarrow I (Λ_{i}) \cap I (Λ_{j}) = \emptyset$ ), and rewrite the constraints of α w.r.t. the set ${Λ_{i} ∣ i \in I}$ . A possible trace set is the combination of the promotions and demotions on the permissions related to the variable α. For example, the combination on the permission set ${p, q}$ is ${\oplus p : : \oplus q, \oplus p : : ⊖ q, ⊖ p : : \oplus q, ⊖ p : : ⊖ q}$ . Then we treat each $(Λ_{i}, α)$ as different fresh variables $α_{i}$ . Therefore, with the ordering, there are no loops like: $(Λ, α) ⩽ \dots ⩽ (Λ^{'}, α)$ . Note that different ordering could yield different results.

Let us consider the constraint set $C_{eg}$ and assume that the order on variables is $β_{b} < α_{b} < α < γ < β$ . There are four lower bounds and one upper bound for α. But only the lower bound $((⊖ p \oplus q, \hat{H}) ⩽ (⊖ p \oplus q, α))$ shares the same satisfiable trace with the upper bound $((⊖ p \oplus q, α) ⩽ (⊖ p, γ))$ . So we saturate the set with the constraint $((⊖ p \oplus q, \hat{H}) ⩽ (⊖ p, γ))$ . Note that the constraint $((ϵ, α_{b}) ⩽ (ϵ, α))$ is not considered as a lower bound for α due to $α_{b} < α$ . Likewise, there are two lower bounds (i.e., $((ϵ, \hat{L}) ⩽ (ϵ, γ))$ and the one newly generated above) and one upper bound (i.e., $((ϵ, γ) ⩽ (ϵ, β))$ ) for γ. Each lower bound has a satisfiable intersected trace with the upper bound, which yields the following constraints $((ϵ, \hat{L}) ⩽ (ϵ, β))$ (already existing in $C_{eg}$ ) and $((⊖ p \oplus q, \hat{H}) ⩽ (⊖ p, β))$ (extended by $⊖ p$ ). While there are no upper bounds for β and no lower bounds for $α_{b}$ and $β_{b}$ , so no constraints are generated. After saturation, the example set $C_{eg}$ is $\begin{array}{l} {((ϵ, β_{b}) ⩽ (ϵ, β)), ((⊖ p, β_{b}) ⩽ (⊖ p, γ)), ((⊖ p, β_{b}) ⩽ (⊖ p \oplus q, α_{b})), ((\oplus p, β_{b}) ⩽ (\oplus p, β)), \\ ((ϵ, α_{b}) ⩽ (ϵ, α)), ((\oplus p \oplus q, \hat{l_{1}}) ⩽ (\oplus p \oplus q, α)), ((\oplus p ⊖ q, \hat{L}) ⩽ (\oplus p ⊖ q, α)), \\ ((⊖ p \oplus q, \hat{H}) ⩽ (⊖ p \oplus q, α)), ((⊖ p ⊖ q, \hat{L}) ⩽ (⊖ p ⊖ q, α)), \\ ((⊖ p \oplus q, α) ⩽ (⊖ p, γ)), ((⊖ p \oplus q, \hat{H}) ⩽ (⊖ p, γ)), ((ϵ, \hat{L}) ⩽ (ϵ, γ)), \\ ((ϵ, γ) ⩽ (ϵ, β)), ((⊖ p \oplus q, \hat{H}) ⩽ (⊖ p, β)), ((ϵ, \hat{L}) ⩽ (ϵ, β)), ((\oplus p, \hat{L}) ⩽ (\oplus p, β))} \end{array}$ where the constraints are rearranged via the ordering.

Given two constraint sets $C_{1}, C_{2}$ , we say $C_{1}$ entails $C_{2}$ , denoted as $C_{1} ⊨ C_{2}$ , iff. for any substitution θ, if $θ ⊨ C_{1}$ , then $θ ⊨ C_{2}$ . We proved that the constraint solving rules are sound and complete, that is, the original constraint set entails the converted set (obtained by decomposition and saturation), and vice-versa. Lemma 3.12.

If $C ⇝_{r} C^{'}$ , then $C ⊨ C^{'}$ and $C^{'} ⊨ C$ , where $r \in {d, s}$ .

3.2.3. Unification

There are two kinds of variables in our setting: global variables and non-global ones, and the constraints for them are all guarded by permission traces. Since the types for non-global variables are dependent on the permission sets, we need to consider the satisfiability of (any subset of) the permission traces of a non-global variable α under any permission set when constructing a type for it. For that, we consider the evaluation of a type t guarded by a permission trace Λ along a permission set P. If $P ⊨ Λ$ , according to Definition 2.5 and Lemma 2.3, then the security level along P is preserved after the application of Λ. So clearly $(t \cdot Λ) (P) = t (P)$ . While for $P ⊭ Λ$ , the security level along P is no longer preserved. Let us consider the simple case $P ⊭ ⊖ p$ (i.e., $p \in P$ ). According to Definition 2.5, we have $(t \cdot ⊖ p) (P) = (t ↓_{p}) (P) = t (P ∖ {p})$ . That is, the security level along a set P containing p is updated as the one along $P ∖ {p}$ . Similar to $\oplus p$ . Therefore, for a trace Λ, we have $(t \cdot Λ) (P) = t (P \cdot Λ)$ , where the application $P \cdot Λ$ is defined as $P \cdot (\oplus p : : Λ^{'}) = (P \cup {p}) \cdot Λ^{'}$ , $P \cdot (⊖ p : : Λ^{'}) = (P ∖ {p}) \cdot Λ^{'}$ , and $P \cdot ϵ = P$ . It is easy to show that $P \cdot Λ = P$ if $P ⊨ Λ$ . So we can uniform the above two cases into $(t \cdot Λ) (P) = t (P \cdot Λ)$ .

Let us consider a non-global variable α and assume that the constraints on it to be solved are ${((Λ_{i}^{l}, t_{i}^{l}) ⩽ (Λ_{i}, α))}_{i \in I}$ (i.e., the lower bounds) and ${((Λ_{j}, α) ⩽ (Λ_{j}^{r}, t_{j}^{r}))}_{j \in J}$ (i.e., the upper bounds). According the above discussion, for any permission set P, α can take a type t such that $(t \cdot Λ_{i}) (P)$ (i.e., $t (P \cdot Λ_{i})$ ) is bigger than $(t_{i}^{l} \cdot Λ_{i}^{l}) (P)$ for any $Λ_{i}$ and that $(t \cdot Λ_{j}) (P)$ (i.e., $t (P \cdot Λ_{j})$ ) is smaller than $(t_{j}^{r} \cdot Λ_{j}^{r}) (P)$ for any $Λ_{j}$ . Consequently, $t (P)$ should be bigger than the union $⨆_{P^{'} \cdot Λ_{i} = P} (t_{i}^{l} \cdot Λ_{i}^{l}) (P^{'})$ and smaller than the intersection $⊓_{P^{'} \cdot Λ_{j} = P} (t_{j}^{r} \cdot Λ_{j}^{r}) (P^{'})$ . In other words, $t (P)$ is equivalent to $((⨆_{P^{'} \cdot Λ_{i} = P} t_{i}^{l} \cdot Λ_{i}^{l}) (P^{'}) ⊔ α^{'} (P)) ⊓ (⊓_{P^{'} \cdot Λ_{j} = P} t_{j}^{r} \cdot Λ_{j}^{r}) (P^{'})$ , where $α^{'}$ is a fresh type variable. Note that the constraint contributes to $t (P)$ if P entails its guarded permission trace Λ. The type above is exactly what we want. We define the construction of the above type via the function $toType$ : (with the convention $⨆_{(i, P') \in \emptyset} t_{i} (P') = L$ and $⊓_{(j, P') \in \emptyset} t_{j} (P') = H$ .) Note that the fresh variables enable us to get a principal type [42] such that every possible type can be obtained from it via subsumption or instantiation. In practice, we take the least possible type.

Since the types for global variables are invariant for all permission sets, that is, the type for a global variable $α^{G}$ should be a level type, e.g., $\hat{l}$ . So the level type $\hat{l}$ should be bigger than all its lower bounds and smaller than all its upper bounds. Let us consider a global variable $α^{G}$ and assume that the constraints on it to be solved are ${((Λ_{i}^{l}, t_{i}^{l}) ⩽ (Λ_{i}, α^{G}))}_{i \in I}$ (i.e., the lower bounds) and ${((Λ_{j}, α^{G}) ⩽ (Λ_{j}^{r}, t_{j}^{r}))}_{j \in J}$ (i.e., the upper bounds). Given a type t, let $maxlevel (t)$ and $minlevel (t)$ denote the maximum level and the minimum level in type t, respectively. So the level l should be bigger than any maximum level of all its lower bounds (i.e., $l ⩾ maxlevel (t_{i}^{l} \cdot Λ_{i}^{l})$ ) and smaller than any minimum level of all its upper bounds (i.e., $l ⩽ minlevel (t_{j}^{r} \cdot Λ_{j}^{r})$ ). In other words, l can take any level ranging from $⨆_{i \in I} maxlevel (t_{i}^{l} \cdot Λ_{i}^{l})$ to $⊓_{j \in J} minlevel (t_{j}^{r} \cdot Λ_{j}^{r})$ , which indicates that l is equivalent to $(⨆_{i \in I} maxlevel (t_{i}^{l} \cdot Λ_{i}^{l}) ⊔ l_{α^{G}}) ⊓ ⊓_{j \in J} minlevel (t_{j}^{r} \cdot Λ_{j}^{r})$ , where $l_{α^{G}}$ is a fresh level variable. Likewise, we define the construction of the type above via the function ${toType}^{G}$ : (with the convention $⨆_{i \in \emptyset} l_{i} = L$ and $⊓_{j \in \emptyset} l_{j} = H$ ).

Moreover, due to the absence of loops in constraints and that the variables are in order, we can solve the constraints in reverse order on variables by unification. The unification algorithm unify is presented as follows.

Consider the constraint set $C_{eg}$ again and assume the set P of all permissions is ${p, q}$ . Firstly, let us take the constraints on the maximum variable β, which are the following set without any upper bounds $\begin{matrix} {((⊖ p \oplus q, \hat{H}) ⩽ (⊖ p, β)), ((ϵ, \hat{L}) ⩽ (ϵ, β)), ((\oplus p, \hat{L}) ⩽ (\oplus p, β))} \end{matrix}$ For the security level along the permission set ∅, there are three combinations contributing to it: $(⊖ p, \emptyset)$ , $(⊖ p, {p})$ and $(ϵ, \emptyset)$ . So the level for ∅ is $((\hat{H} \cdot ⊖ p \oplus q) (\emptyset) ⊔ (\hat{H} \cdot ⊖ p \oplus q) ({p}) ⊔ (\hat{L} \cdot ϵ) (\emptyset) ⊔ β' (\emptyset)) ⊓ H$ , which is equivalent to H. Similar to the other sets. So by applying the function $toType$ , we construct for β the type $t_{β} = {\emptyset \mapsto H, {p} \mapsto (L ⊔ β' ({p})) ⊓ H, {q} \mapsto H, {p, q} \mapsto (L ⊔ β' ({p, q})) ⊓ H}$ , where $β'$ is a fresh variable. For simplicity, we pick the least possible upper bound when constructing types. So we take ${\emptyset \mapsto H, {p} \mapsto L, {q} \mapsto H, {p, q} \mapsto L}$ as $t_{β}$ instead. Next, we substitute $t_{β}$ for all the occurrences of β in the remaining constraints and continue with the constraints on γ, α, $α_{b}$ , and $β_{b}$ . Finally, the types constructed for these type variables are $t_{γ} = t_{β}$ and $t_{α} = {\emptyset \mapsto L, {p} \mapsto L, {q} \mapsto H, {p, q} \mapsto l_{1}}$ , $t_{α_{b}} = t_{α}$ , $t_{β_{b}} = t_{β}$ , respectively. Therefore, the types we infer for A.getInfo and B.fun are $() \overset{t_{α}}{\to} t_{α}$ and $() \overset{t_{β}}{\to} t_{β}$ , respectively.

Next, we show that our unification is sound and complete.

Lemma 3.13.
If $unify (C) = θ$ , then $θ ⊨ C$ .
Lemma 3.14.
If $θ ⊨ C$ , then there exist $θ'$ and $θ ″$ such that $unify (C) = θ'$ and $θ = θ' θ ″$ .

Let sol be the function for the constraint solving algorithm, that is, $sol (C) = unify (sat (dec (C)))$ . It is provable that the constraint solving algorithm is sound and complete.
Lemma 3.15.
If $sol (C) = θ$ , then $θ ⊨ C$ .
Proof.
By Lemma 3.12 and Lemma 3.13. □
Lemma 3.16.
If $θ ⊨ C$ , then there exist $θ'$ and $θ ″$ such that $sol (C) = θ'$ and $θ = θ' θ ″$ .
Proof.
By Lemma 3.12 and Lemma 3.14. □

To conclude, an expression (command, function, resp.) is typable, iff it is derivable under the constraint rules with a solvable constraint set by our algorithm. Therefore, our type inference system is sound and complete. Moreover, as the function call chains are finite, the constraint generation terminates with a finite constraint set, which can be solved by our algorithm in finite steps. Thus, our type inference system terminates. Theorem 3.1.
The type inference system is sound, complete and decidable.
Proof.

sound: By Lemma 3.8, Lemma 3.10, and Lemma 3.15.

complete: By Lemma 3.9, Lemma 3.11, and Lemma 3.16.

decidable: as the function call chains are finite, the constraint generation terminates with a finite constraint set, which can be solved by $sol$ in finite steps. Thus, the type inference system terminates.
□

4. A representation of types

As given in Definition 2.1, our types are defined as mappings from the power set $P$ of the permission set P to the lattice $L$ of security levels. Naively encoding types as permission sets leads to an exponential increase in time as well as size required to process and manipulate them due to the cardinality of the power set $P$ growing as $2^{n}$ , where n is the number of permissions. Android, itself, has around 200 permissions9

⁹
https://developer.android.com/reference/android/Manifest.permission.html

which can lead to performance decreases due to the time taken to process permissions. In practice, we can expect a security type to consist only of a few ‘interesting’ mappings for some combinations of permissions, and a ‘default’ mapping for the rest of the combinations of permissions, so the actual size of security types used in practice should be much smaller.

There are a number of choices one can make as to how to encode the ‘default’ mappings; for example, one could use propositional logic, first order logic, or some ad hoc data structures. Two main considerations are the space complexity of the chosen representation (in the average case) and the space/time complexity of the type-related operations on the representation. Here we choose a representation of types that builds on the concept of reduced ordered binary decision diagrams (ROBDDs) [7,24]. ROBDD has been well-studied and has been applied successfully in areas such as model checking [11], so we think it is a good choice to build our representation on.

The principle idea behind choosing ROBDDs as the underlying data structure for representing types lies in the fact that any permission set can be encoded as bit vectors (after fixing an order on these permissions), namely, the presence or absence of permissions can be represented by a sequence of 1s and 0s. Taking the permission set $P = {p, q}$ from Listing 2 as example, all the possible permission sets can be represented as the bit vectors ${00, 01, 10, 11}$ . Moreover, as shown in Section 3.2, the permission traces are interpreted as sets of permission sets and can be considered as boolean logic formulae on permission sets, where ⊕ and ⊖ respectively denote the positive and negative literals, corresponding to the presence or absence of permissions. Thus the encoding of ROBDD enables us to infer our types directly on the permission traces via the logic connectives. The key is to generate a set of permission traces ${Λ_{i} | i \in I}$ for each variable such that they are full (i.e., $⋃_{i \in I} I (Λ_{i}) = P$ ) and disjoint (i.e., $\forall i, j \in I . i \neq j \Rightarrow I (Λ_{i}) \cap I (Λ_{j}) = \emptyset$ ). For example, we can infer for β in Listing 4 the type $t_{β} = {⊖ p \mapsto H, \oplus p \mapsto (L ⊔ l_{β}^{\oplus p}) ⊓ H}$ (no matter what P is), which is a variant of ROBDD, rather than ${\emptyset \mapsto H, {p} \mapsto (L ⊔ l_{β}^{{p}}) ⊓ H, {q} \mapsto H, {p, q} \mapsto (L ⊔ l_{β}^{{p, q}}) ⊓ H}$ ( $P = {p, q}$ ).

For simplicity, we shall refer to ROBDDs as just binary decision diagrams (BDDs). BDDs have some important and useful properties: (i) canonicity, that is to say for a fixed boolean variable ordering, each boolean function has a canonical (i.e. unique) representation (up to isomorphism) [7,24]; and (ii) operations on BDDs are efficient. With proper ordering, the time complexity of operations usually depends linearly on the number of boolean variables [7]. Note that a security type with a two-element lattice (‘High’ and ‘Low’) is essentially a boolean function. So the worst case space complexity of the BDD representation (or any known representation of boolean functions, for that matter) is exponential [7].

4.1. Types as binary decision diagrams

In this section, we give the definition of a binary decision diagram that fits our types, which is a modification10

¹⁰
Our modification generalizes the set of outputs from binary to an arbitrary finite set.

of the one in [7]. Note that in all our definitions, we assume that a static global order has been defined on the permissions. This serves two purposes: (i) the concept of representing permission sets as bit vectors would be meaningless otherwise; and (ii) it helps in the construction of binary decision diagrams.

To start with, let us consider a general function $f : {0, 1}^{n} \to S$ , where S is an arbitrary finite set. Clearly, we can represent it as a truth table. More specifically, we can represent the function $f (x_{1}, \dots, x_{n})$ as a $2^{n}$ -bit string of values, where each value is some $s \in S$ . This string starts with the function value $f (0, \dots, 0)$ and continues on with $f (0, \dots, 0, 1), \dots, f (1, \dots, 1, 1)$ . As an example, the truth table for the boolean function $g = x_{1} \land x_{2}$ would be $g (0, 0) g (0, 1) g (1, 0) g (1, 1) = FFFT$ .

Definition 4.1.

Given an arbitrary finite set S and a natural number n, a truth table of order n is a string $α \in S^{*}$ of length $2^{n}$ . A bead of order n is a truth table α of order n that is not square, that is, α can not be represented as $β β$ for any string $β \in S^{*}$ of length $2^{n - 1}$ .

Given a finite set S, there are $| S |$ beads of order 0; and $| S |^{2} - | S |$ beads of order 1. In general, there are $| S |^{2^{n}} - | S |^{2^{n - 1}}$ beads of order n. This is derived simply by removing elements on the diagonal of a square matrix of order $2^{n - 1}$ , that is, by removing all combinations $α β$ with $α = β$ , where $α, β$ are truth tables of order $n - 1$ .

Our modified definition of a binary decision diagram to represent the function $f : {0, 1}^{n} \to S$ is given below.

Definition 4.2.

A binary decision diagram (BDD) is a rooted, directed graph with vertex set V containing two types of vertices. A nonterminal vertex (node) m has as attributes an argument index $m . v \in {1, 2, \dots, n}$ ; and two children $m . l, m . h \in V$ (referred to as low and high respectively). A terminal vertex (sink or leaf) m has as attribute a value $m . val \in S$ , where S is an arbitrary finite set.

Furthermore, a strict ordering restriction is imposed on nonterminal vertices. For any nonterminal vertex m, if $m . l$ is also nonterminal, then it must be the case that $m . v < m . l . v$ . Similarly, if $m . h$ is nonterminal, then it must be the case that $m . v < m . h . v$ .

A BDD is reduced if no two nodes are allowed to have the same triple of values $(v, l, h)$ . Therefore, no node m in a reduced BDD is allowed to have $m . l = m . h$ , which indicates that the output does not depend on this particular node m. Figure 9 gives two examples of BDDs that represent the same function $f_{e}$ given in Table 1, wherein $n = 3$ and $S = {L, M, H}$ . Note that, in this figure and others henceforth, the dashed lines represent the ‘0’ or low branch. We can see that the first example (i.e., Fig. 9a) is not reduced, because (i) the leftmost node of $x_{3}$ has two equal children, and ( $ii$ ) both the high children of the nodes $x_{2}$ are equal. While the second example (i.e., Fig. 9b) is reduced.

Fig. 9.

Examples of binary decision diagram.

Table 1

The truth table of function $f_{e}$

$x_{1}$	$x_{2}$	$x_{3}$	$f_{e} (x_{1}, x_{2}, x_{3})$	$x_{1}$	$x_{2}$	$x_{3}$	$f_{e} (x_{1}, x_{2}, x_{3})$
0	0	0	L	1	0	0	L
0	0	1	L	1	0	1	H
0	1	0	L	1	1	0	L
0	1	1	M	1	1	1	M

We now show that our modified definition of a BDD still holds the property of canonicity. To that end, we modify a proof for canonicity as described by Knuth [24].

Theorem 4.1.

Given an arbitrary finite set S, any function of the form $f : {0, 1}^{n} \to S$ has a unique (up to isomorphism) reduced binary decision diagram, where n is the number of inputs.

Proof.

We argue that every truth table τ can be represented as a power of a unique bead. Let τ be a truth table of order n that is not a bead. Then, by Definition 4.1, it is the square of a truth table $τ'$ of order $n - 1$ . By induction on the order of τ, we have that $τ' = β^{k}$ , where k is a power of 2, and β is a bead of order $⩽ n - 1$ . Hence, we have that τ can be represented as $τ = β^{2 k}$ . We call this β the root of τ (and $τ'$ ). Therefore, by the principle of induction, every truth table τ is a power of a unique bead.

A truth table τ of order $n > 0$ can be represented as $τ_{0} τ_{1}$ , where $τ_{0}$ and $τ_{1}$ are truth tables of order $n - 1$ . By construction, τ represents the function $f (x_{1}, x_{2}, \dots, x_{n})$ if and only if $τ_{0}$ represents $f (0, x_{2}, \dots, x_{n})$ and $τ_{1}$ represents $f (1, x_{2}, \dots, x_{n})$ . The functions $f (0, x_{2}, \dots, x_{n})$ and $f (1, x_{2}, \dots, x_{n})$ are called subfunctions of f; and $τ_{0}$ and $τ_{1}$ are called subtables of τ. The beads of such a function f are the subtables of its truth table that are beads.

Now we come to the crux of the argument: the nodes of a binary decision diagram for a function f (as described above) are in bijection with the beads of f. A function’s truth tables of order $n + 1 - k$ (with $1 ⩽ k ⩽ n$ ) correspond to its subfunctions $f (c_{1}, \dots, c_{k - 1}, x_{k}, \dots, x_{n})$ , where $c_{i}$ denotes a binary value. Hence, the beads of order $n + 1 - k$ correspond to those subfunctions that depend on their first boolean variable $x_{k}$ . Therefore, every such bead corresponds to a node in the BDD. Let the truth table corresponding to this node be $τ' = τ_{0}^{'} τ_{1}^{'}$ , then its l and h attributes point respectively to the nodes that correspond to the roots of $τ_{0}^{'}$ and $τ_{1}^{'}$ . □

Considering the function $f_{e}$ in Table 1, the truth table $τ_{f_{e}}$ for $f_{e}$ is $LLLMLHLM$ and hence, all possible subtables of $τ_{f_{e}}$ are ${LLLMLHLM, LLLM, LHLM, LL, LM, LH, L, M, H}$ . Given this, the beads of $f_{e}$ then are ${LLLMLHLM, LLLM, LHLM, LM, LH, L, M, H}$ . Note that the subtable $LL$ is not present since it is not a bead. Figure 10 showcases the BDD formed by the beads of $f_{e}$ as laid out in Theorem 4.1. Note the isomorphism between Fig. 9b and 10.

Fig. 10.

BDD formed by beads of $f_{e}$ .

Let us return to our types. As mentioned above, permission sets can be encoded as bit vectors, where ‘0’ represents the absence of a permission and ‘1’ represents the presence of a permission. Moreover, operations on sets such as $\cup, \cap, ∖$ , etc. can easily be transcribed into operations on bit vectors. Accordingly, we redefine our types as folllows:

Definition 4.3.

A base security type t is a mapping from the set of all possible bit vectors representing permission sets to the lattice of security levels, i.e. $t : P \to L$ . The set of base types is denoted with $T$ .

Using Theorem 4.1, the new definition of a type, and the definition of a binary decision diagram, we define the representation of types as follows:

Definition 4.4.

Let t be a base type. The representation of t, denoted by $R (t)$ , is a reduced ordered binary decision diagram, where each nonterminal node m represents (the position in the static order of) a permission $p \in {1, 2, \dots | P |}$ ; the low and $high$ branches of m (i.e., $m . l$ and $m . h$ ) represent the absence and the presence of p, respectively; and each terminal (or sink) node represents an output security level $l \in L$ .

In order to evaluate a permission set for the representation of a given type, one can simply move down the diagram by choosing the branch that corresponds to the 0–1 value in the bit vector for that particular permission. If a node for a permission p does not exist, then one can simply skip that permission as the output security level does not depend on p’s value. Formally, the evaluation of the representation r along (a bit vector representing) a permission set P can be defined as $\begin{matrix} r (P) = \{\begin{matrix} r . v a l & r is sink \\ r . l (P) & P [r . v] = 0 \\ r . h (P) & P [r . v] = 1 \end{matrix} \end{matrix}$ Clearly, it is easy to get that our representation is correct, as shown in Lemma 4.1.

Lemma 4.1.

Let t be a type. Then for any permission set P, we have $(1) t (P) = R (t) (P)$ ; and $(2) R (t) (P) = R (t) (P \cup {p}) = R (t) (P ∖ {p})$ for any permission $p \notin R (t)$ .

Fig. 11.

Representation of type t.

To illustrate, let us consider the type t that maps the sets of permissions ${p_{1}}$ and ${p_{2}, p_{3}}$ to H, and any other subset of ${p_{1}, p_{2}, p_{3}}$ to L. Figure 11 show the BDD of t, where the bit vector is represented as $p_{1} p_{2} p_{3}$ . Following the paths to H in the diagram gives us the following bit vectors: ${100, 011}$ . On the other hand, following the paths to L in the diagram gives us the following bit vectors: ${00 x, 010, 101, 11 x}$ , where ‘x’ represents permissions whose values do not affect the output security level. These values encompass all elements of the powerset $P$ and accurately represents the mapping in type t as required. Moreover, the permissions whose values do not affect the output security level can be removed in BDD, which yields the small numbers (i.e., 5 and 6, resp.) of nodes and of paths to the sinks. In comparison, a binary decision tree would have $2^{3} - 1$ nodes and $2^{3}$ different paths to sinks.

An example in practice is the type $t = {\emptyset \mapsto L, {p} \mapsto L, {q} \mapsto H, {p, q} \mapsto l_{1}}$ used in Listing 2. Assuming the order is $q, p$ , the paths to L in the corresponding BDD could be merged, resulting in fewer nodes and paths. Moreover, many apps or services require more than two permissions, such as the facial recognition service requiring the permissions for camera and storage (2 permissions for the storage group) and the video calling service requiring the permissions11

¹¹

https://developers.connectycube.com/android/videocalling

for Wi-Fi, camera, audio, and storage. These services terminate immediately if any permission is not granted.12

¹²

Such a multiple permission checking refers to https://codingmitra.com/multiple-permission-run-time-in-android/.

So the type for these services maps the set containing all the required permissions to a non-low security level depending on the services and the other sets to L, whose representation is given in Fig. 12, where the dashed rectangle denotes a group of permissions, for example, the permission group for storage may contain READ_EXTERNAL_STORAGE and WRITE_EXTERNAL_STORAGE. Figure 12 shows that the representation requires

| P |

nodes and

| P | + 1

paths to sinks, rather than

2^{| P |} - 1

nodes and

2^{| P |}

paths (even worse if all the permissions are considered), where P is the set of all required permissions. In addition, some services take different actions depending the granted permissions. For example, the location service determines the current location from GPS sensor (requiring the permissions for location), networks (requiring the permissions for Wi-Fi), or the last known location (requiring the permissions for storage). The type for the location service would map the set containing any group of required permissions to a non-low security level for the location and the other sets to L, whose representation is given in Fig. 13, wherein a group is not granted if any one of its permissions is not granted. Similarly, the corresponding BDD has

| P |

nodes and at least

| P | + 1

paths to sinks. So we believe the representation will be efficient in practice.

Fig. 12.

Representation of type for video calling.

Fig. 13.

Representation of type for location.

4.2. Operations on types

Unlike BDDs in [7], the outputs of our BDDs are a multi-value lattice. It is quite difficult to come up with a general framework describing operations on types as directly working on the Boolean functions (i.e., BDDs on two-value lattice). Therefore, we directly provide algorithms for operations on types mentioned in Section 2.4, via reasoning on the structure of the diagram. Here we focus on the operations only for our types, namely, projection, promotion, demotion, and merging. While the others, namely, the intersection $s ⊓ t$ , the union $s ⊔ t$ , and the subtyping $s ⩽ t$ , could be obtained directly via the Apply function as described in [7,24].

Firstly, with respect to the definition of type presentations, the properties for promotion, demotion, projection, and merging defined in Definition 2.5, 2.6, and 2.7 still hold.

Lemma 4.2.
Given a base type t, a permission p, and a permission set $P \in P$ , then $(1) R (t ↑_{p}) (P) = R (t) (P \cup {p})$ and $(2) R (t ↓_{p}) (P) = R (t) (P ∖ {p})$ .
Lemma 4.3.
Given a type t and a permission set $P \in P$ , then for any permission set $Q \in P$ , $R (π_{P} (t)) (Q) = R (t) (P)$ .
Lemma 4.4.
Given two types $t_{1}, t_{2}$ and a permission p, then for any permission set $P \in P$ , $\begin{matrix} R (t_{1} ⊳_{p} t_{2}) (P) = \{\begin{matrix} R (t_{1}) (P) & p \in P \\ R (t_{2}) (P) & p \notin P \end{matrix} \end{matrix}$

According to Lemma 4.3, we argue that we can simply represent the projection as a binary decision diagram with a single vertex, being a sink node.
Lemma 4.5.
Given a base type t and a permission set $P \in P$ , the projection of t on P can be represented as a constant terminal vertex m with $m . val = t (P)$ .

Fig. 14.
Algorithms for promotion and demotion.

The case for promotion and demotion is slightly more complicated. Recalling the Definition 2.5, the promotion of a base type t with respect to a permission p involves removing all branches where $p = 0$ and redirecting them to where $p = 1$ . In other words, p is present in all permission sets regardless. We formalize this intuitive explanation into an algorithm as described in Fig. 14a. Likewise, the algorithm for demotion is given in Fig. 14b, where all branches with $p = 1$ are removed and redirected the one with $p = 0$ instead.

The function Index(p) is a helper function that outputs the position of the permission p in the static global order; and Reduce( ) is a procedure which restores the reduced property of a binary decision diagram [7,24]. Hence, given a base type t, and a permission p, the promotion operation is performed in situ by calling Promotion( $R (t), p$ ).

Figure 15 shows the promotion of the type t in Fig. 9 with respect to $p_{2}$ , where the dashed lines in red denote the modifications needed by the promotion.

Fig. 15.
Example for promotion (the dashed lines in red denote the modifications needed by the promotion).

The correctness of the algorithms for promotion and demotion is given in Lemma 4.6.
Lemma 4.6.
Given a base type t and a permission p, then $(a) P ROMOTION (R (t), p) = R (t ↑_{p})$ and $(b) D EMOTION (R (t), p) = R (t ↓_{p})$ .

One can see that the number of operations required for promoting a type depends on the number of nodes in $R (t)$ , or more accurately, the number of nodes m such that $m . v ⩽ I NDEX (p)$ . Note that since the procedure is performed in situ, we do not actually introduce any new nodes, and in fact our output will have fewer nodes (than initially) after reduction. Also note that the time complexity of Reduce( ), as defined in [24], is $O (N + n)$ , where N is the size of the input BDD, and n is the number of boolean variables. Given the above, we can say that the time complexity of Promotion is $O (N + n + N) = O (2 N + n)$ . A similar argument can be constructed for the case of Demotion as well.

Fig. 16.
Algorithm for merge.

Finally, let us describe how the merge operation could be implemented. Recall the definition: the merging of two types $t_{1}$ and $t_{2}$ along the permission p is: $\begin{matrix} t_{1} ⊳_{p} t_{2} (P) = \{\begin{matrix} t_{1} (P), & p \in P \\ t_{2} (P), & p \notin P \end{matrix} \forall P \in P \end{matrix}$ That is, the node of p in the merged diagram is formed by the low branch of the node of p in $R (t_{2})$ and the high branch of the node of p in $R (t_{1})$ . Due to the reducing, the permission p may not occur in $R (t_{1})$ or $R (t_{2})$ . So we divide the problem into two cases: (i) p occurs in neither $R (t_{1})$ nor $R (t_{2})$ (e.g., both $R (t_{1})$ and $R (t_{2})$ are sink or both $R (t_{1}) . v$ and $R (t_{2}) . v$ are greater than $I NDEX (p)$ ); and (ii) p occurs in at least one of $R (t_{1})$ and $R (t_{2})$ . The first case is intuitively easy to reason for: we simply create a node for p and let the low branch and the high branch point to (the roots of) $R (t_{2})$ and $R (t_{1})$ , respectively.

The second case is slightly more complex. Let us assume p occurs in both $R (t_{1})$ and $R (t_{2})$ and further divide it into two subcases: (i) both representations are rooted by p; and (ii) one of the representations is not rooted by p. For the first subcase, we simply redirect the low branch (i.e. l or ‘0’ branch) of (the root of) $R (t_{1})$ to the low branch of (the root of) $R (t_{2})$ . And for the second subcase, we recursively traverse $R (t_{1})$ and $R (t_{2})$ until we reach a point where both the representations are rooted by p, and then merge as per the first subcase at that point. Moreover, if p does not occur in $R (t_{1})$ (resp. $R (t_{2})$ ), then we can imagine that there is a dummy node for p, where both its low branch and high branch are the smallest node in $R (t_{1})$ (resp. $R (t_{2})$ ) that is greater than $I NDEX (p)$ . The algorithm is a slightly modified version of the Apply function as described in [7,24]. The intuition behind our change lies in, besides the sinks, all nodes with index no smaller than p are treated as a terminal (i.e. as a base case). Figure 16 gives the details for the Merge( ) algorithm.

An example of the merge of the type t in Fig. 9 and another type s along $p_{2}$ is given in Fig. 17. The following lemma shows the correctness of the Merge( ) algorithm.

Fig. 17.
Example for merge.
Lemma 4.7.
Given two types $t_{1}, t_{2}$ and a permission p, then $M ERGE (R (t_{1}), R (t_{2}), p) = R (t_{1} ⊳_{p} t_{2})$ .

Note that unlike Promotion-Recurse( ) and Demotion-Recurse( ), Merge-Recurse( ) constructs an entire new diagram such that the p nodes of both diagrams have been merged. Hence, the space complexity of this operation drastically increases. The time complexity of Merge-Recurse( ) has order of $| R (t_{1}) | \cdot | R (t_{2}) |$ as the merge operation essentially creates ordered pairs of nodes of the two diagrams. Moreover, we can represent the above as a matrix of values. Then we can reduce the time complexity of Merge-Recurse( ) to $| R (t_{1} ⊳_{p} t_{2}) |$ , by only filling entries in the matrix that are reachable by $t_{1} ⊳_{p} t_{2}$ .
5. Related work

There is a large body of work on language-based information flow security. We shall discuss only closely related work.

We have extensively discussed the work by Banerjee and Naumann [3] and highlighted the major differences between our work and theirs in Section 1.

Flow-sensitive and value-dependent information flow type systems provide a general treatment of security types that may depend on other program variables or execution contexts [23,27,29,30,32–38,40,44,49–51,54–56]. Hunt and Sands [23] proposed a flow-sensitive type system where order of execution is taken into account in the analysis, and demonstrated that the system is precise. But the system is simpler than ours. Mantel et. al. [34] introduced a rely-guarantee style reasoning for information flow security in which the same variable can be assigned different security levels depending on whether some assumption is guaranteed, which is similar to our notion of permission-dependent security types. Li and Zhang [27] proposed both flow-sensitive and path-sensitive information flow analysis with program transformation techniques and dependent types. Information flow type systems that may depend on execution contexts have been considered in work on program synthesis [44] and dynamic information flow control [54]. Our permission context can be seen as a special instance of execution context, however, our intended applications and settings are different from [44,54], and issues such as parameter laundering does not occur in their setting. Lourenço and Caires [33] provided a precise dependent type system where security labels can be indexed by data structures, which can be used to encode the dependency of security labels on other values in the system. It may be possible to encode our notion of security types as a dependent type in their setting, by treating permission sets explicitly as an additional parameter to a function or a service, and to specify security levels of the output of the function as a type dependent on that parameter. Currently it is not yet clear to us how one could give a general construction of the index types in their type system that would correspond to our security types, and how the merge operator would translate to their dependent type constructors, among other things. We leave the exact correspondence to the future work.

Recent research on information flow has also been conducted to deal with Android security issues ([8,10,18,19,22,31,39]). SCandroid [8,19] is a tool automating security certification of Android apps that focuses on typing communication between applications. Unlike our work, they do not consider implicit flows, and do not take into account access control in their type system. Ernst et al [18] proposed a verification model, SPARTA, for use in app stores to guarantee that apps are free of malicious information flows. Their approach requires the collaboration between software vendor and app store auditor and the additional modification of Android permission model to fit for their Information Flow Type-checker; soundness proof is also absent. Our work is done in the context of providing information flow security certificates for Android applications, following the Proof-Carrying-Code architecture by Necula and Lee [41] and does not require extra changes on existing Android application supply chain systems. Cassandra [31] performs the security analysis of apps on a server, which employs the proof-carrying code paradigm such that the server’s analysis result can be validated on the client. H. Gunadi [22] presented a type system for DEX bytecode and prove the soundness of the type system with respect to a notion of non-interference. Both [31] and [22] do not consider permission-dependent. ComDroid [10] detects communication vulnerabilities in Android applications from the perspectives of Intent senders and Intent recipients. Weir [39] is a practical DIFC system for Android, allowing data owner applications to set secrecy policies and control the export of their data to the network. And a number of security analysis tools, such as TaintDroid [16], DroidSafe [21] and TaintART [47], perform a data flow analysis on Android apps to track information-flow. But there is no soundness result for these analyses.

A few inference algorithms [28,43] have been proposed to infer dependent labels. Lifty [43] employed refinement types to encode information flow security, and proposed an inference algorithm based on the inference engine of liquid types [45]. While this is a neat solution for a two-level security lattice, the encoding does not apply to applications that require multiple security labels. Li and Zhang [28] proposed a general framework for designing and checking label inference algorithms for information flow analysis with dependent security labels. Based on the framework, novel inference algorithms that are both sound and complete are developed. The predicated constraint they proposed can express predicate on program state, and thus is a general version of ours. Limited to our setting, their one-shot algorithm is equivalent to ours. However, although efficient, the algorithms, except the one-shot one, may be over-conservative. For example, the early-accept algorithm and hybrid algorithm would infer $\hat{H}$ for the motivation example getInfo listed in 2, which is clearly imprecise. Moreover, Li and Zhang did not provide a principal solution for their algorithms. This indicates that the algorithms, except the one-shot one, may not be complete in the sense that every possible solution can be obtained by the algorithm, such as the precise type for getInfo can’t be obtained from $\hat{H}$ via subsumption or instantiation.

6. Conclusion and future work

We have provided a lightweight yet precise type system featuring Android permission model for enforcing secure information flow in an imperative language and proved its soundness with respect to non-interference. Compared to existing work, our type system can specify a broader range of security policies, including non-monotonic ones. We have also proposed a decidable type inference algorithm by reducing it to a constraint solving problem, as well as a new way to represent our security types as reduced ordered binary decision diagrams.

We next discuss briefly several directions for future work.

The immediate one is to extend our system to richer programming languages, including object-oriented features (like [48]), exceptions (like [6]), etc. Another extension is to incorporate the efficient type representation in the inference algorithm. A proposed solution is to encode our permission guarded constraints as a special BDD, where the outputs are the constraints without guards (i.e., constraints on the output labels).

We also plan to apply our type system to real Android applications to enforce permission-dependent information flow policies. A main challenge is to facilitate type inference so that a programmer does not need to type every variable and instead focuses only on policy specifications of a service. To enable this, we need to be able to extract all permissions relevant to an app and to identify all commands relevant to permission checking in an app. The former is straightforward since the permissions that can be granted to an app is statically specified in the app’s manifest file. For the latter, the permission checking code segments (typically library function calls) can be located with pre-processed static analyses (e.g., [2,53]).

Another interesting direction is in modeling runtime permission request. From Android 6.0 and above, several permissions are classified as dangerous permissions and granting of these permissions is subject to users’ approval at runtime. This makes enforcing non-monotonic policies impossible in some cases, e.g., when a policy specifies the absence of a dangerous permission in releasing sensitive information. However, an app can only request for a permission it has explicitly declared in the manifest file, so to this extent, we can statically determine whether a permission request is definitely not going to be granted (as it is absent from the manifest), and whether it can potentially be granted. And fortunately (but unfortunately from a security perspective) the typical scenarios are that users grant all the requested permissions during runtime when requested (in order to gain a better user experience with the app). Therefore one can assume optimistically that all permissions in the manifest are finally granted. In the future, we plan to resolve this issue with weaker assumptions. One feasible approach is to model dangerous permissions in a typing environment separately and allow policies to be non-monotonic on non-dangerous permissions only.

Lastly, our eventual goal is to translate source code typing into Dalvik bytecode typing, following a similar approach done by Gilles Barthe et al. [4–6] from Java source to JVM bytecode. The key idea that we describe in the paper, i.e., precise characterizations of security of IPC channels that depends on permission checks, can still be applied to richer type systems such as those used in the Cassandra project [31] or Gunadi’s type system [22]. We envision our implementation can piggyback on, say, Cassandra system to improve the coverage of typable applications.

Footnotes

Acknowledgments

This work has been partially supported by the National Natural Science Foundation of China under Grants No. 61972260, 61772347, 61836005, Guangdong Basic and Applied Basic Research Foundation under Grant No. 2019A1515011577, Guangdong Science and Technology Department under Grant No. 2018B010107004, and the National Satellite of Excellence in Trustworthy Software Systems (Award No. NRF2018NCR-NSOE003) funded by NRF Singapore under National Cyber-security R&D (NCR) programme.

Proofs for soundness

Proofs for type inference

To prove the completeness, we need to prove some auxiliary lemmas.

Before proving our unification is sound and complete, we show the $toType$ is correct. Lemma B.3.

Consider a type variable α with $C_{α}^{L} = {((Λ_{i}^{l}, t_{i}^{l}) ⩽ (Λ_{i}, α))}_{i \in I}$ and $C_{α}^{U} = {((Λ_{j}, α) ⩽ (Λ_{j}^{r}, t_{j}^{r}))}_{j \in J}$ . Let $t_{α}$ be the type constructed from $toType (C_{α}^{L}, C_{α}^{U})$ if α is local or ${toType}^{G} (C_{α}^{L}, C_{α}^{U})$ otherwise.

${α \mapsto t_{α}} ⊨ C_{α}^{L} \cup C_{α}^{U}$ .

If $θ ⊨ C_{α}^{L} \cup C_{α}^{U}$ , then there exists $θ'$ such that $dom (θ') ♯ dom (θ)$ and $(θ \cup θ') (α) = t_{α} (θ \cup θ')$ .

Proof.

The proof of (a): Let us consider any lower bound $((Λ_{i}^{l}, t_{i}^{l}) ⩽ (Λ_{i}, α))$ and any permission set P: $\begin{matrix} (t_{α} \cdot Λ_{i}) (P) & = t_{α} (P \cdot Λ_{i}) \\ = {P \mapsto (⨆_{(i, P') \in S_{I}^{P}} (t_{i}^{l} \cdot Λ_{i}^{l}) (P') ⊔ α' (P)) ⊓ ⊓_{(j, P') \in S_{J}^{P}} (t_{j}^{r} \cdot Λ_{j}^{r}) (P') | P \subseteq P} (P \cdot Λ_{i}) \\ = (⨆_{(i, P') \in S_{I}^{P \cdot Λ_{i}}} (t_{i}^{l} \cdot Λ_{i}^{l}) (P') ⊔ α' (P \cdot Λ_{i})) ⊓ ⊓_{(j, P') \in S_{J}^{P \cdot Λ_{i}}} (t_{j}^{r} \cdot Λ_{j}^{r}) (P') \\ ⩾ ⨆_{(i, P') \in S_{I}^{P \cdot Λ_{i}}} (t_{i}^{l} \cdot Λ_{i}^{l}) (P') \\ ⩾ (t_{i}^{l} \cdot Λ_{i}^{l}) (P) (as (i, P) \in S_{I}^{P \cdot Λ_{i}}) \end{matrix}$ So ${α \mapsto t_{α}} ⊨ C_{α}^{L}$ . Similar to ${α \mapsto t_{α}} ⊨ C_{α}^{U}$ .

The proof of (b): Let $θ_{0} = {α' \mapsto θ (α)}$ , where $α'$ is a fresh variable introduced by $toType$ . Clearly, we have $dom (θ_{0}) ♯ dom (θ)$ . Since $θ ⊨ C_{α}^{L} \cup C_{α}^{U}$ , we have $(t_{i}^{l} θ) \cdot Λ_{i}^{l} ⩽ θ (α) \cdot Λ_{i}$ and $θ (α) \cdot Λ_{j} ⩽ (t_{j}^{r} θ) \cdot Λ_{j}^{r}$ for all $i \in I$ and $j \in J$ . So we have $((t_{i}^{l} θ) \cdot Λ_{i}^{l}) (P) ⩽ (θ (α) \cdot Λ_{i}) (P)$ and $(θ (α) \cdot Λ_{j}) (P) ⩽ ((t_{j}^{r} θ) \cdot Λ_{j}^{r}) (P)$ for any permission set P. In other words, for any permission set P, we have $((t_{i}^{l} θ) \cdot Λ_{i}^{l}) (P') ⩽ θ (α) (P)$ if $P' \cdot Λ_{i} = P$ and $θ (α) (P) ⩽ ((t_{j}^{r} θ) \cdot Λ_{j}^{r}) (P')$ if $P' \cdot Λ_{j} = P$ . Moreover, $\begin{matrix} t_{α} (θ \cup θ_{0}) (P) \\ = {P \mapsto (⨆_{(i, P') \in S_{I}^{P}} (t_{i}^{l} \cdot Λ_{i}^{l}) (P') ⊔ α' (P)) ⊓ ⊓_{(j, P') \in S_{J}^{P}} (t_{j}^{r} \cdot Λ_{j}^{r}) (P') | P \subseteq P} (θ \cup θ_{0}) (P) \\ = (⨆_{(i, P') \in S_{I}^{P}} (t_{i}^{l} (θ \cup θ_{0}) \cdot Λ_{i}^{l}) (P') ⊔ ((θ \cup θ_{0}) (α')) (P)) ⊓ ⊓_{(j, P') \in S_{J}^{P}} (t_{j}^{r} (θ \cup θ_{0}) \cdot Λ_{j}^{r}) (P') \\ = (⨆_{(i, P') \in S_{I}^{P}} (t_{i}^{l} θ \cdot Λ_{i}^{l}) (P') ⊔ θ (α) (P)) ⊓ ⊓_{(j, P') \in S_{J}^{P}} (t_{j}^{r} θ \cdot Λ_{j}^{r}) (P') \\ = θ (α) (P) ⊓ ⊓_{(j, P') \in S_{J}^{P}} (t_{j}^{r} θ \cdot Λ_{j}^{r}) (P') (as (t_{i}^{l} θ \cdot Λ_{i}^{l}) (P') ⩽ θ (α) (P) for (i, P') \in S_{I}^{P}) \\ = θ (α) (P) (as θ (α) (P) ⩽ ((t_{j}^{r} θ) \cdot Λ_{j}^{r}) (P') for (j, P') \in S_{J}^{P}) \\ = (θ \cup θ_{0}) (α) \cdot Λ \end{matrix}$

Otherwise, α is global. The proof is similar to the case above and based on the fact that the types for global variables are invariance for all permission sets. □

Proof for Lemma 3.13.

By induction on $| C |$ . $| C | = 0$

Trivial.

| C | > 0

In this case we have $C = {((Λ_{i}^{l}, t_{i}^{l}) ⩽ (Λ_{i}, α))}_{i \in I} \cup {((Λ_{j}, α) ⩽ (Λ_{j}^{r}, t_{j}^{r}))}_{j \in J} \cup C'$ , where $O (α)$ is the greatest. Let $t_{α}$ be the type constructed from the constraints on α (denoted as $C_{α}$ ) and $C ″$ be the constraint set obtained by replacing in $C'$ every occurrence of α by $t_{α}$ . Assume $unify (C ″) = θ'$ . Thus $θ = θ' \cup {α \mapsto t_{α}}$ . First, by Lemma B.3, we have ${α \mapsto t_{α}} ⊨ C_{α}$ , and thus $θ ⊨ C_{α}$ . Next, by induction, we have $θ' ⊨ C ″$ . Let’s consider the constraints ${((Λ_{i}^{l}, s_{i}^{l}) ⩽ (Λ_{i}, β))}_{i \in I} \cup {((Λ_{j}, β) ⩽ (Λ_{j}^{r}, s_{j}^{r}))}_{j \in J} \subseteq C'$ of any other variable β. Then we have ${((Λ_{i}^{l}, s_{i}^{l} {α \mapsto t_{α}}) ⩽ (Λ_{i}, β))}_{i \in I} \cup {((Λ_{j}, β) ⩽ (Λ_{j}^{r}, s_{j}^{r} {α \mapsto t_{α}}))}_{j \in J} \subseteq C ″$ . $\begin{matrix} θ (β) \cdot Λ_{i} & = θ' (β) \cdot Λ_{i} (Apply θ) \\ ⩾ ((s_{i}^{l} {α \mapsto t_{α}}) θ') \cdot Λ_{i}^{l} (θ' ⊨ C ″) \\ = (s_{i}^{l} (θ' \cup {α \mapsto t_{α}})) \cdot Λ_{i}^{l} \end{matrix}$ and $\begin{matrix} θ (β) \cdot Λ_{j} & = θ' (β) \cdot Λ_{j} (Apply θ) \\ ⩽ ((s_{j}^{r} {α \mapsto t_{α}}) θ') \cdot Λ_{j}^{r} (θ' ⊨ C ″) \\ = (s_{j}^{r} (θ' \cup {α \mapsto t_{α}})) \cdot Λ_{j}^{r} \end{matrix}$ Therefore, the result follows.

□

Proof for Lemma 3.14.

We prove that the statement $θ = θ' θ$ , which deduces the result. The statement holds trivially when $| C | = 0$ .

When $| C | > 0$ , we have $C = {((Λ_{i}^{l}, t_{i}^{l}) ⩽ (Λ_{i}, α))}_{i \in I} \cup {((Λ_{j}, α) ⩽ (Λ_{j}^{r}, t_{j}^{r}))}_{j \in J} \cup C'$ , where $O (α)$ is the greatest. Let $t_{α}$ be the type constructed from the constraints on α (denoted as $C_{α}$ ) and $C_{0}$ be the constraint set obtained by replacing in $C'$ every occurrence of α by $t_{α}$ . Since $θ ⊨ C$ , we have $θ ⊨ C'$ and $θ ⊨ C_{α}$ , and thus $θ ⊨ C_{0}$ . By induction on $C_{0}$ , there exists $θ'_{0}$ such that $unify (C_{0}) = θ'_{0}$ and $θ = θ'_{0} θ$ . According to the function unify, we get $unify (C) = θ'_{0} \cup {α \mapsto t_{α}} = θ'$ . For any $β \notin dom (θ')$ , clearly $β (θ' θ) = β θ$ . Considering α, since $θ ⊨ C_{α}$ , by Lemma B.3, we have $α θ = t_{α} θ$ , and thus $α θ = α (θ' θ)$ . While for any other variable $β \in dom (θ')$ , we have $β (θ' θ) = β ((θ'_{0} \cup {α \mapsto t_{α}}) θ) = β (θ'_{0} θ) = β θ$ . □

Proofs for representation

References

Android, Requesting permissions at run time. https://developer.android.com/training/permissions/requesting.html.

Arzt,

Rasthofer,

Fritz,

Bodden,

Bartel,

Klein,

Le Traon,

Octeau and

McDaniel, FlowDroid: Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps, SIGPLAN Not. 49(6) (2014), 259–269. doi:10.1145/2666356.2594299.

Banerjee and

D.A.

Naumann, Stack-based access control and secure information flow, Journal of Functional Programming 15(2) (2005), 131–177. doi:10.1017/S0956796804005453.

Barthe,

Pichardie and

Rezk, A certified lightweight non-interference Java bytecode verifier, in: Proceedings of the 16th European Symposium on Programming, ESOP’07, Berlin, Heidelberg, 2007, pp. 125–140.

Barthe and

Rezk, Non-interference for a JVM-like language, in: TLDI, 2005, pp. 103–112. doi:10.1145/1040294.1040304.

Barthe,

Rezk and

D.A.

Naumann, Deriving an information flow checker and certifying compiler for Java, in: IEEE Symposium on Security and Privacy, 2006, pp. 230–242.

R.E.

Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers 35(8) (1986), 677–691. doi:10.1109/TC.1986.1676819.

Chaudhuri, Language-based security on Android, in: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, PLAS ’09, New York, NY, USA, 2009, pp. 1–7.

Chen,

Tiu,

Xu and

Liu, A permission-dependent type system for secure information flow analysis, in: 31st IEEE Computer Security Foundations Symposium, CSF, IEEE Computer Society, Oxford, United Kingdom, 2018, pp. 218–232.

10.

Chin,

A.P.

Felt,

Greenwood and

Wagner, Analyzing inter-application communication in Android, in: Proceedings of the 9th International Conference on Mobile Systems, Applications, and Services, MobiSys ’11, New York, NY, USA, 2011, pp. 239–252.

11.

E.M.

Clarke,

T.A.

Henzinger,

Veith and

Bloem (eds), Handbook of Model Checking, Springer, 2018. ISBN 978-3-319-10574-1. doi:10.1007/978-3-319-10575-8.

12.

D.E.

Denning, A lattice model of secure information flow, Communications of the ACM 19(5) (1976), 236–243. doi:10.1145/360051.360056.

13.

D.E.

Denning and

P.J.

Denning, Certification of programs for secure information flow, Communications of the ACM 20(7) (1977), 504–513. doi:10.1145/359636.359712.

14.

A. Developers, Binder, 2017, online, accessed on 07-July-2017.

15.

A. Developers, PermissionChecker | Android Developers, 2017, online, accessed on 07-July-2017.

16.

Enck,

Gilbert,

Chun,

L.P.

Cox,

Jung,

P.D.

McDaniel and

Sheth, TaintDroid: An information-flow tracking system for realtime privacy monitoring on smartphones, in: 9th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2010), 2010, pp. 393–407.

17.

Enck,

Ongtang and

McDaniel, Understanding Android security, IEEE Security and Privacy 7(1) (2009), 50–57. doi:10.1109/MSP.2009.26.

18.

M.D.

Ernst,

Just,

Millstein,

Dietl,

Pernsteiner,

Roesner,

Koscher,

P.B.

Barros,

Bhoraskar,

Han,

Vines and

E.X.

Wu, Collaborative verification of information flow for a high-assurance app store, in: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS ’14, ACM, New York, NY, USA, 2014, pp. 1092–1104. ISBN 978-1-4503-2957-6.

19.

A.P.

Fuchs,

Chaudhuri and

Foster, SCanDroid: Automated security certification of android applications, Technical Report, CS-TR-4991, University of Maryland, 2009.

20.

J.A.

Goguen and

Meseguer, Security policies and security models, in: SOSP, 1982, pp. 11–20.

21.

M.I.

Gordon,

Kim,

Perkins,

Gilham,

Nguyen and

Rinard, Information-flow analysis of Android applications in DroidSafe, in: 22nd Annual Network and Distributed System Security Symposium (NDSS 2015), 2015.

22.

Gunadi, Formal certification of non-interferent Android bytecode (DEX bytecode), in: Proceedings of the 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS), ICECCS ’15, Washington, DC, USA, 2015, pp. 202–205. doi:10.1109/ICECCS.2015.36.

23.

Hunt and

Sands, On flow-sensitive security types, in: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’06, ACM, New York, NY, USA, 2006, pp. 79–90. ISBN 1-59593-027-2. doi:10.1145/1111037.1111045.

24.

D.E.

Knuth, The Art of Computer Programming, Vol. 4. Fascicle 1, 1st edn, Addison Wesley Longman Publishing Co., Inc., United States, 2009.

25.

Landauer and

Redmond, A lattice of information, in: 6th IEEE Computer Security Foundations Workshop – CSFW’93, Franconia, New Hampshire, USA, June 15–17, 1993, Proceedings, IEEE Computer Society, 1993, pp. 65–70.

26.

Li,

Bartel,

T.F.

Bissyandé,

Klein,

Le Traon,

Arzt,

Rasthofer,

Bodden,

Octeau and

McDaniel, IccTA: Detecting inter-component privacy leaks in Android apps, in: Proceedings of the 37th International Conference on Software Engineering – Volume 1, ICSE ’15, IEEE Press, Piscataway, NJ, USA, 2015, pp. 280–291. ISBN 978-1-4799-1934-5.

27.

Li and

Zhang, Towards a flow- and path-sensitive information flow analysis, in: 2017 IEEE 30th Computer Security Foundations Symposium (CSF), 2017, pp. 53–67. doi:10.1109/CSF.2017.17.

28.

Li and

Zhang, A derivation framework for dependent security label inference, in: Proc. ACM Program. Lang. 2(OOPSLA), 2018, pp. 115:1–115:26.

29.

Li,

Nielson,

H.R.

Nielson and

Feng, Disjunctive information flow for communicating processes, in: TGC, 2015.

30.

Li,

Nielson and

Riis Nielson, Future-dependent flow policies with prophetic variables, in: The 2016 ACM Workshop, ACM Press, New York, NY, USA, 2016, pp. 29–42.

31.

Lortz,

Mantel,

Starostin,

Bahr,

Schneider and

Weber, Cassandra: Towards a certifying app store for Android, in: Proceedings of the 4th ACM Workshop on Security and Privacy in Smartphones and Mobile Devices, SPSM ’14, New York, NY, USA, 2014, pp. 93–104.

32.

Lourenço and

Caires, Information flow analysis for valued-indexed data security compartments, in: Trustworthy Global Computing – 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30–31, 2013, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 8358, Springer, 2014, pp. 180–198.

33.

Lourenço and

Caires, Dependent information flow types, in: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15, New York, NY, USA, 2015, pp. 317–328.

34.

Mantel,

Sands and

Sudbrock, Assumptions and guarantees for compositional noninterference, in: Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27–29 June, 2011, IEEE Computer Society, 2011, pp. 218–232. doi:10.1109/CSF.2011.22.

35.

Murray, Short paper: On high-assurance information-flow-secure programming languages, in: Proceedings of the 10th ACM Workshop on Programming Languages and Analysis for Security, 2015.

36.

Murray,

Sison,

Pierzchalski and

Rizkallah, Compositional verification and refinement of concurrent value-dependent noninterference, in: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), 2016, pp. 417–431.

37.

Murray,

Sison,

Pierzchalski and

Rizkallah, A dependent security type system for concurrent imperative programs, Archive of Formal Proofs (2016), http://isa-afp.org/entries/Dependent_SIFUM_Type_Systems.shtml, Formal proof development.

38.

Murray,

Sison,

Pierzchalski and

Rizkallah, Compositional security-preserving refinement for concurrent imperative programs, Archive of Formal Proofs (2016), http://isa-afp.org/entries/Dependent_SIFUM_Refinement.shtml, Formal proof development.

39.

Nadkarni,

Andow,

Enck and

Jha, Practical DIFC enforcement on Android, in: USENIX Security Symposium, 2016.

40.

Nanevski,

Banerjee and

Garg, Verification of information flow and access control policies with dependent types, in: 32nd IEEE Symposium on Security and Privacy, S&P 2011, 22–25 May 2011, Berkeley, California, USA, IEEE Computer Society, 2011, pp. 165–179. doi:10.1109/SP.2011.12.

41.

G.C.

Necula and

Lee, Proof-carrying code, Technical Report, School of Computer Science, Carnegie Mellon University, 1996, CMU-CS-96-165.

42.

B.C.

Pierce, Types and Programming Languages, MIT Press, 2002. ISBN 978-0-262-16209-8.

43.

Polikarpova,

Yang,

Itzhaky,

Hance and

Solar-Lezama, Enforcing information flow policies with type-targeted program synthesis, 2018, arXiv preprint arXiv:1607.03445v2.

44.

Polikarpova,

Yang,

Itzhaky and

Solar-Lezama, Type-driven repair for information flow security, CoRR abs/1607.03445 (2016). http://arxiv.org/abs/1607.03445.

45.

P.M.

Rondon,

Kawaguchi and

Jhala, Liquid types, in: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7–13, 2008,

Gupta and

S.P.

Amarasinghe, eds, ACM, 2008, pp. 159–169. doi:10.1145/1375581.1375602.

46.

Sabelfeld and

A.C.

Myers, Language-based information-flow security, IEEE Journal on Selected Areas in Communications 21(1) (2003), 5–19. doi:10.1109/JSAC.2002.806121.

47.

Sun,

Wei and

J.C.S.

Lui, TaintART: A practical multi-level information-flow tracking system for Android RunTime, in: Proceedings of the 23rd ACM Conference on Computer and Communications Security, CCS’16, 2016.

48.

Sun,

Banerjee and

D.A.

Naumann, Modular and constraint-based information flow inference for an object-oriented language, in: Static Analysis,

Giacobazzi, ed., Springer, Berlin Heidelberg, Berlin, Heidelberg, 2004, pp. 84–99. ISBN 978-3-540-27864-1. doi:10.1007/978-3-540-27864-1_9.

49.

Swamy,

Chen and

Chugh, Enforcing stateful authorization and information flow policies in FINE, in: Programming Languages and Systems, 19th European Symposium on Programming (ESOP), Lecture Notes in Computer Science, Vol. 6012, Springer, 2010, pp. 529–549. doi:10.1007/978-3-642-11957-6_28.

50.

Swamy,

Chen,

Fournet,

Strub,

Bhargavan and

Yang, Secure distributed programming with value-dependent types, Journal of Functional Programming 23(4) (2013), 402–451. doi:10.1017/S0956796813000142.

51.

Tse and

Zdancewic, Run-time principals in information-flow type systems, ACM Trans. Program. Lang. Syst. 30(1) (2007). doi:10.1145/1290520.1290526.

52.

Volpano,

Irvine and

Smith, A sound type system for secure flow analysis, Journal of Computer Security 4(2–3) (1996), 167–187. doi:10.3233/JCS-1996-42-304.

53.

Wei,

Roy,

Ou and

Robby, A precise and general inter-component data flow analysis framework for security vetting of Android apps, in: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS ’14, ACM, New York, NY, USA, 2014, pp. 1329–1341. ISBN 978-1-4503-2957-6.

54.

Yang,

Yessenov and

Solar-Lezama, A language for automatically enforcing privacy policies, in: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, ACM, 2012, pp. 85–96. doi:10.1145/2103656.2103669.

55.

Zhang,

Wang,

G.E.

Suh and

A.C.

Myers, A hardware design language for timing-sensitive information-flow security, in: The Twentieth International Conference, ACM Press, New York, New York, USA, 2015, pp. 503–516.

56.

Zheng and

A.C.

Myers, Dynamic security labels and static information flow control, International Journal of Information Security 6(2–3) (2007), 67–84. doi:10.1007/s10207-007-0019-9.

A permission-dependent type system for secure information flow analysis

Abstract

Keywords

1. Background and introduction

1 Some permissions in Android 6 and above require user approval at runtime, but for the purpose of typing the ‘test’ command, we make the assumption that these permissions are enabled as well.

2.1. A model of permission-based access control

3 To be specific, runtime permission request requires the compatible version specified in the manifest file to be greater than or equal to API level 23, and running OS should be at least Android 6.0.

2.4. Security types

3.1.1. Permission tracing

3.2.1. Decomposition

7 Rule ( CD-MEGER 0 ) is not necessary but can simplify the constraints as shown in the illustrated example.

8 It should be Λ 1 : : dif ( Λ 1 , Λ 2 ) or Λ 2 : : dif ( Λ 2 , Λ 1 ) . But thanks to Lemmas 3.4 and 3.2, we assume the duplicated promotions and demotions can be removed implicitly and the remaining promotions and demotions can be reordered if needed. Here we write Λ 1 : : Λ 2 for short.

9 https://developer.android.com/reference/android/Manifest.permission.html

10 Our modification generalizes the set of outputs from binary to an arbitrary finite set.

6. Conclusion and future work

Footnotes

Acknowledgments

Proofs for soundness

Proofs for type inference

Proofs for representation

References

¹
Some permissions in Android 6 and above require user approval at runtime, but for the purpose of typing the ‘test’ command, we make the assumption that these permissions are enabled as well.

³
To be specific, runtime permission request requires the compatible version specified in the manifest file to be greater than or equal to API level 23, and running OS should be at least Android 6.0.

⁷
Rule ( ${CD-MEGER}_{0}$ ) is not necessary but can simplify the constraints as shown in the illustrated example.

⁹
https://developer.android.com/reference/android/Manifest.permission.html

¹⁰
Our modification generalizes the set of outputs from binary to an arbitrary finite set.