Enforcing Mobile Application Security Through Probabilistic Contracts
Enforcing Mobile Application Security Through Probabilistic Contracts
Xxxxx Xxxxxxxxxx0, Xxxxxx Xxxxxxxxx0, Xxxxxx Xxxxxxxx00, and Xxxxxxx Xxxxxxxxx0
1 Dipartimento di Ingegneria dell’Informazione,
Universita` di Pisa, Pisa, Italy
2 Istituto di Informatica e Telematica,
Xxxxxxxxx Nazionale delle Ricerche, Pisa, Italy
Abstract. Security for mobile devices is a problem of capital importance, es- pecially due to new threats coming from malicious applications. Though several security solutions have already been proposed, security requirements have been always considered as binary: allow or deny. We argue that a more realistic vision of security can be given using probabilistic and quantitative requirements.
In this paper, we introduce a probabilistic description of the behavior of an ap- plication that a user is going to execute. We also allow the definition of finer grained user security requirements, by introducing probabilistic clause modifiers. Later, we present a probabilistic version of the Security-by-Contract framework to guarantee probabilistic security requirements.
Keywords: Probabilistic Contract, Probabilistic Policy Compliance, Contract-based Security approaches, Run-Time Enforcement.
1 Overview
New generation mobile devices (e.g., smartphones and tablets) are becoming day-by- day more powerful and popular. The growth in computing power, ubiquitousness and capabilities of these devices has been paralleled by the growth of available applications, specifically developed for smartphones and tablets. However, these applications may be not completely secure. In fact, malicious developers strive to design and deliver applications that may damage both users and devices. In particular some applications may hide a Trojan horse that, even if it looks unharmful, in background it performs malicious actions that the users did not expect to happen.
The current security model, which rules (i) if an application can be safely installed on the device, (ii) what kind of actions the application may execute once installed, still suffers from several weaknesses, in particular in its capacity of expressing proper contracts. Semantics of current security models is too na¨ıve since it is either based upon trust relationships or upon statements of purpose. In the first case, users accept to run an application if they trust the provider. In the second one, providers state the security
relevant actions performed by an application and it is up to the users to decide whether run the application if they consider these operations safe. In the former case the trust level of the trusted entity also determines the code privileges, essentially relegating an application into the “all or nothing” policy, while in the latter case the semantics is too-coarse grained (e.g., Android permissions) or hardly usable. For example, in the Android system, security relevant actions are declared through permissions, which are difficult to understand for average users.
×
In this paper, we introduce probability aspects into the workflow of a contract-based approach developed for mobile devices: the Security-by Contract [1] (S C) framework. This approach integrates several security techniques to build a chain of trust, which, in the end, ensures that the downloaded application will execute only security actions that are allowed by the user’s policy. To this end, we introduce a probabilistic description of the behavior of an application and a more expressive version of the user’s security requirements. Indeed, the current models only permit the definition of a set of allowed actions, e.g., the Android permission system (first box of Figure 1). More expressive policies which take in account a possible action history are modelled through automata that represent allowed executions.
Fig. 1. Graphical representation of the improvement in policies expressiveness.
×
×
We propose a probabilistic automata-based model that enables the developers to de- fine more expressive contracts through probabilistic clauses, e.g., how often a security- relevant action may happen. The same expressiveness is given to users to specify secu- rity policies. Since we include probabilistic clauses in the specification of contracts and policies, the security mechanisms involved into the workflows of S C has to be rede- fined. Hence, we present a new workflow for the S C framework in which each module is updated to support probabilistic functions. The advantage of using probabilities is the possibility of describing more realistic usage scenarios for an application. In fact, many applications depend on user inputs or context information and it is difficult to define realistic policies based upon boolean conditions only. In these models, all the possible execution paths are considered legal. Hence, a low-probability operation is considered valid even if performed several times. For this reason, we introduce probabilities in the
definition of security clauses to define more fine-grained contracts and policies. These descriptions better fit real application use cases and can be defined without alteration of the Security-By-Contract-with-Trust workflow.
The paper is structured as follows. Section 2 introduces the main concepts of contract- based approaches and briefly recalls the Security-by-Contract framework. In Section 3, we propose a probabilistic version of Security-by-Contract. Section 4 briefly concludes proposing a future working line.
2 Contract-based Approaches
× × ×
Contract-based approaches have been developed for mobile devices, such as the Security- by-Contract [1] (S C) and the Security-by-Contract-with-Trust [2,3] (S C T) frame- works. They integrate several security techniques to build a chain of trust by sequen- tially applying them to safely execute applications. The three cornerstones of these se- curity frameworks are application code A, application contract C, and client policy P , where a contract is a formal, complete, and correct specification of an application secu- rity relevant behavior, e.g., security critical virtual machine API call, or critical system calls [4]. A policy is a formal complete specification of the acceptable security-relevant behavior allowed to applications executed on the platform [4]. We assume that both contract and policy are syntactically described by exploiting the same language.
≤
The basic idea of a contract-based approach is the usage of the contract for guaran- teeing that security aspects are satisfied. More in detail, using the contract, it is possible to check at deploy time, i.e., before the application execution, if the application satis- fies the user policy or not. Let denote the compliance between two of the previous elements. A contract-based approach guarantees that
A ≤ C ≤ P ⇒ A ≤ P (1)
×
In the following, we describe the Security-by-Contract (S C) framework as ap- proach that integrates the described techniques to guarantee security at application ex- ecution time.
2.1 Security-by-Contract
The Security-by-Contract paradigm provides a full characterization of the contract- based interaction. It combines different functionalities in an integrated way (see Figure 2). In particular, it includes a module for automatically checking the formal correspon- dence between code and contract (Application-Contract matching). If the result is neg- ative, then the monitor is run to enforce the policy (Policy Enforcement), otherwise a matching between the contract and the policy (Contract-Policy Matching) is performed to establish if the contract is compliant with the policy. In this case, the code is exe- cuted without overhead (Safe Execution), otherwise the policy is enforced again (Policy Enforcement).
The advantages of contract-based frameworks are that they are able to identify un- safe applications before and without running them. In particular, using the contract- policy matching functionality, it checks at deploy-time if the declared behavior of the
Fig. 2. The Security-by-Contract process.
application is compliant with the required policy. This check, along with the assurance that the application code is compliant with the application contract, which is obtained through the application-contract matching module, guarantees that the application sat- isfies the user requirements. Anytime the contract-policy matching finds that a contract is not compliant with the policy, the application is run in a controlled way through the enforcement module. It is worth noticing that the cost, in terms of energy, of running a contract policy matching is much lower than performing the enforcement. Hence, un- safe applications are not run at all by the user and possible unsafe application are run in a controlled way. This leads to an attack risk reduction.
3 Probabilistic Security-by-Contract
×
In this section, we describe a probabilistic version of the S C architecture. It is worth noticing that, in both cases the original workflow is not changed. Only the components are modified in such a way that, on one hand, they are able to cope with probability metrics and, on the other hand, Equation 1 still holds for an appropriate choice of the notion of compliance.
Let us assume that both probabilistic contract and probabilistic policy are expressed through the same formalism.
Probabilistic contract and policy will be modelled as (substochastic) generative probabilistic automata [5,6].
Definition 1. A fully probabilistic or generative automata is a tuple (S, Act, P ) con- sisting of a finite set S of states, a set of actions Act, and a transition probability func- tion
P : S × Act × S → [0, 1]
Fig. 3. Workflow for Probabilistic Security-by-Contract
A generative automata is said to be stochastic if
Σ Σ P (s, a, t) = 1
a∈Act t∈S
∈ ∈
for all s S for all a Act. On the other hand, a generative automata is said to be
semistochastic or substochastic if
Σ Σ P (s, a, t) < 1
a∈Act t∈S
s ∈ S is said to be terminal iff Σa,t P (s, a, t) = 0.
for all s ∈ S for all a ∈ Act. For C ⊆ S, we put P (s, a, C) = Σt∈C P (s, a, t). A state
Hereafter, we consider generative automata such that for each action there is only one possible transition for each action a ∈ Act.
3.1 Probabilistic Security-by-Contract Workflow
Being the Security-By-Contract framework modular, introducing probability metrics implies the substitution of some components with their probabilistic counterpart. The Probabilistic Security-by-Contract workflow is depicted in Figure 3.
×
Probabilistic application contract matching is verified using some static validation techniques able to deal with probabilistic description of behavior. For instance, as proof carrying code [7] is used in S C, here we can use the Probabilistic Proof Carrying Code, e.g., [8,9]. In particular, this method guarantees that, for all possible k-length execution traces whose probability is calculated as Pk =
Q
k i=1
P (si, ai, ti), the application is considered compliant if Pk > θk, where θk
is a given threshold value 0 < θk < 1 dependent from the length of the execution
trace.
×
Probabilistic contract policy matching is performed by checking the compliance be- tween a contract and a policy. According to the level of required accuracy, several relations can be considered in order to verify the compliance between probabilistic contract and policy. In S C, the contract-policy matching function checks if the contract and the policy are similar. This means that for each action described in the contract, we check if there exists the same action described in the policy and the description of the transition are similar again. Hence, we assume that the policy specifies a rule for each security relevant action, which we call SecAction.
Referring to the notion of ε-simulation given in [10], hereafter, we define a slightly different ε-simulation.
Definition 2. A relation R ⊆ S × S is a relation of positive ε-simulation, where
ε ∈ [0, 1] if whenever (s, s′) ∈ R, then ∀a ∈ SecAction, ∀W ∈ S
Σ P (s, a, t) ≤ Σ P (s′, a, t′) ≤ Σ(P (s, a, t) + ε)
t∈W
t'∈R(W )
t∈W
≺ ∈
where R(W ) is the set of all states that are in relation with states in W trough R. We say that s is ε-simulated by s′, written s ε s′, if (s, s′) R for some relation of ε-simulation R on S.
∈ −
The idea is that, while the ε-simulation allows a deviation of a values ε [ 1, 1], here, we are only interested in positive values of ε. Hence, the probabilistic distri- bution of the contract have to be less that the probability distribution of the policy of, at most, a value ε.
It is worth noticing that, according to our assumptions, having a positive ε-simulation R means that whether (s, s′) ∈ R then, for each action a ∈ SecAction,
P (s, a, t) ≤ P (s′, a, t′) ≤ P (s, a, t) + ε
and (t, t′) ∈ R.
Enforcement of Probabilistic Policies is performed when either the application is not compliant with the contract or the contract is not compliant with the policy.
At each step, the enforcement computes the probability that the application per- forms a specific security relevant action a, starting from the current state s, Pp(s, a, t), where t is the destination state of the transition and p is the expected one stated by the policy. This computation exploits history-based concerning the current ex- ecution of the application. The computation of the probability of the execution trace is similar to the one described in the application-contract matching module
k
i=1
k
Pp = Qk Pp(si, ai, ti). The application is considered compliant if Pp > θk,
where θk is the same considered in the application-contract module. The enforce-
ment denies the non compliant operation sequence, ensuring that the policy is cor- rectly enforced.
It is worth noticing that Equation 1 holds. Indeed, the fact that C ≤ε P means that
k
Pk ≤ Pp because
k k
k
Pk = Y P (si, ai, ti) ≤ Y Pp(si, ai, ti) = Pp
i=1 i=1
k
≤ ≤
Hence, θk < Pk Pp Let Θ be the compliance relation used in both application- contract matching and enforcement mechanisms, where Θ denotes the set of threshold values θk for any k-length execution trace, and let us consider to use the positive ε- simulation for the contract-policy matching then the following holds
A ≤Θ C ≤ε P ⇒ A ≤Θ P
4 Conclusion and Future Work
×
In this paper, we have discussed the current limitations of the semantics of the security models for mobile applications. To this end, we have presented a probabilistic version of the Security-by-Contract, which is able to guarantee probabilistic requirements. We have discussed the advantages in terms of expressiveness achieved including proba- bility in the S C framework. Future extensions to this work will be the definition of probabilistic formalisms and languages, which should be used to programmatically de- fine probabilistic contracts and policies, then to verify their compliance. This languages should be equivalent in expressiveness to the probabilistic automata that we have used to express policies and contracts. Furthermore, we are going to include the presented framework in real mobile devices, investigating if it is possible to distribute it as com- mon mobile application, which can give users a way to better control their mobile de- vices.
References
1. Xxxxxxx, X., Xxxxxxxxxx, X., Xxxxxxxx, X., Xxxx, P., Xxxxxxxx, X., Xxxxxx, X., Xxxxxxxxx, E.: Security-by-contract (SxC) for software and services of mobile systems. In: At your service
- Service-Oriented Computing from an EU Perspective., MIT Press (2008)
2. Xxxxx, X., Xxxxxxx, N., Xxxxxxxx, X., Xxxxxxxxxx, F., Xxxxxxxx, F., Xxxxxxxxx, I.: Extend- ing Security-by-Contract with quantitative trust on mobile devices. In: Proceeding of the Fourth International Conference on Complex, Intelligent and Software Intensive Systems, IEEE Computer Society (2010) 872–877
3. Xxxxx, X., Xxxxxxx, N., Xxxxxxx, V., Xxxxxxxx, X., Xxxxxxxxxx, F., Xxxxxxxx, F., Xxxxxxxxx, I., Xxxxx, R.: Security-by-Contract-with-Trust for mobile devices. JOWUA 1(4) (2010) 75–91
4. Xxxxx, X., Xxxxxxxxxx, X., Xxxxxxxxx, I.: A framework for contract-policy matching based on symbolic simulations for securing mobile device application. In: ISoLA. (2008) 221–236
5. Xxxxxxxx, X., Parma, A., Xxxxxx, R., Xxxxxxx, B., Xxxxx, X.: Probabilistic logical charac- terization. Inf. Comput. 209(2) (2011) 154–172
6. Xxxxx, C., Xxxxxxx, B., Majster-Cederbaum, M.: Deciding bisimilarity and similarity for probabilistic processes. Journal of Computer and System Sciences 60(1) (2000) 187–231
7. Xxxxxx, X.X.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL ’97). (1997) 106–119
8. Xxxxxxx, M.I.: Probabilistic Proof-carrying Code. PhD thesis, Carleton University (2012)
9. Xxxxxxx, X.: Interactive and probabilistic proof of mobile code safety. Automated Software Engineering 12(2) (2005) 237–257
10. Xxxxxxxxxx, X., Xxxxxxxxxx, F., Xxxxxx, M.: Approximate analysis of probabilistic processes: Logic, simulation and games. In: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems. QEST ’08, Washington, DC, USA, IEEE Computer Society (2008) 264–273