A Framework for Probabilistic Contract Compliance

We propose PICARD (ProbabIlistic Contract on AndRoiD), a framework to detect repackaged applications for Android smartphones based upon probabilistic contract matching. A contract describes the sequences of actions that an application is allowed to perform at run-time, i.e. its legal behavior. In PICARD, contracts are generated from the set of traces that represent the usage profile of the application. Both the contract and the application's run-time behavior are represented through clustered probabilistic automata. At run-time, a monitoring system verifies the compliance of the application trace with the contract. This approach is useful in detecting repackaged applications, whose behavior is strongly similar to the original application but it differs only from small paths in the traces. In this paper, we discuss the framework of PICARD for describing and generating contracts through probabilistic automata and introduce the notion of ActionNode, a cluster of related system calls. Then, we present a first set of results using a prototype implementation of PICARD for Android smartphones to prove the efficacy of the framework in detecting two classes of applications, repackaged and trojanized ones.