A Framework for Contract-Policy Matching based on Symbolic Simulations for securing Mobile Device Application

There is a growing interest on programming models based on the notion of contract. In particular, in the security realm one could imagine the situation where either downloaded code or software service exposes their security-relevant behavior in a contract (that must to be fulfilled). Assuming to have already a mechanism to ensure that the program/service adheres to the contract, it just remains to check that the contract matches with the user security policy. We refer to this testing procedure as contract-policy matching. We specialize this framework in the ambit of mobile devices. The contract and the user policy are formally expressed by using (symbolic) transition systems. Then, contract-policy matching amounts to simulation checking, i.e., a contract transition system is simulated by a policy one. This means that we check if for each transition corresponding to a certain security action of the contract (and so possibly performed by the program), the policy system has a similar transition and resulting contract system is again simulated by the resulting policy one. Showing some running examples, we eventually present an implementation of simulation-matching algorithm, developed in J2ME and suitable to run also on smart phones.