Security for mobile devices is a problem of capital importance, especially 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 application 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.
New generation mobile devices (e.g., smartphones and tablets) are becoming day-byday 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 [
The paper is structured as follows. Section 2 introduces the main concepts of contractbased 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 have been developed for mobile devices, such as the
Securityby-Contract [
The basic idea of a contract-based approach is the usage of the contract for guaranteeing 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 satisfies 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 approach that integrates the described techniques to guarantee security at application execution time. 2.1
The Security-by-Contract paradigm provides a full characterization of the contractbased interaction. It combines different functionalities in an integrated way (see Figure 2). In particular, it includes a module for automatically checking the formal correspondence between code and contract (Application-Contract matching). If the result is negative, 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 executed 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 unsafe applications before and without running them. In particular, using the contractpolicy matching functionality, it checks at deploy-time if the declared behavior of the 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 satisfies 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, unsafe 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
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 [
Definition 1. A fully probabilistic or generative automata is a tuple (S; Act; P ) consisting of a finite set S of states, a set of actions Act, and a transition probability function
P : S
Act
S ! [0; 1] for all s 2 S for all a 2 Act. On the other hand, a generative automata is said to be semistochastic or substochastic if
X X P (s; a; t) = 1 a2Act t2S X X P (s; a; t) < 1 a2Act t2S for all s 2 S for all a 2 Act. For C S, we put P (s; a; C ) = Pt2C P (s; a; t). A state s 2 S is said to be terminal iff Pa;t P (s; a; t) = 0.
Hereafter, we consider generative automata such that for each action there is only one possible transition for each action a 2 Act. 3.1
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.
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 = Qik=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 between 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 " 2 [0; 1] if whenever (s; s0) 2 R, then 8a 2 SecAction, 8W 2 S
X P (s; a; t) t2W
X t02R(W )
P (s0; a; t0)
X (P (s; a; t) + ") t2W 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 s0, written s " s0, if (s; s0) 2 R for some relation of "-simulation R on S.
The idea is that, while the "-simulation allows a deviation of a values " 2 [ 1; 1], here, we are only interested in positive values of ". Hence, the probabilistic distribution 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; s0) 2 R then, for each action a 2 SecAction, P (s; a; t)
P (s0; a; t0)
P (s; a; t) + " and (t; t0) 2 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 performs a specific security relevant action a, starting from the current state s, P p(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 execution of the application. The computation of the probability of the execution trace is similar to the one described in the application-contract matching module Pkp = Qik=1 P p(si; ai; ti). The application is considered compliant if Pkp > k, where k is the same considered in the application-contract module. The enforcement denies the non compliant operation sequence, ensuring that the policy is correctly enforced.
Pk
It is worth noticing that Equation 1 holds. Indeed, the fact that C
Pkp because " P means that k Pk = Y P (si; ai; ti) i=1 k Y P p(si; ai; ti) = Pkp i=1 Hence, k < Pk Pkp Let be the compliance relation used in both applicationcontract 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
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 probability 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 define 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 common mobile application, which can give users a way to better control their mobile devices. 7. Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Langauges (POPL ’97). (1997) 106–119 8. Sharkey, M.I.: Probabilistic Proof-carrying Code. PhD thesis, Carleton University (2012) 9. Tsukada, Y.: Interactive and probabilistic proof of mobile code safety. Automated Software
Engineering 12(2) (2005) 237–257 10. Desharnais, J., Laviolette, F., Tracol, 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