Ask a(n)droid to tell you the odds: probabilistic security-by-contract for mobile devices

Security-by-contract is a paradigm proposed for the secure installation, usage, and monitoring of apps into mobile devices, with the aim of establishing, controlling, and, if necessary, enforcing security-critical behaviors. In this paper, we extend this paradigm with new functionalities allowing for a quantitative estimation of such behaviors, in order to reveal in real time the more and more challenging subtleties of new-generation malware and repackaged apps. The novel paradigm is based on formal means and techniques ranging from statistical analysis to probabilistic model checking. The framework, deployed in the Android environment, is evaluated by examining both its effectiveness with respect to a benchmark of real-world malware and its effect on the execution of genuine, secure apps.