On Probabilistic Application Compliance

The Security-by-Contract is a paradigm developed to offer a secure environment in which mobile applications can be executed by respecting the security policies of interest. Especially in the Android Apps marketplace, establishing precisely the expected secure app behavior is typically a complex operation that is prone to approximations. Hence, it is worth considering extensions of purely functional approaches that allow the security relevant actions to be quantitatively assessed. This also opens the possibility to balance the application of (expensive) enforcement mechanisms with the security guarantees. With these objectives in view, in this paper we define a probabilistic extension of the Security-by-Contract model, and we show its impact in real-world scenarios through the analysis of several practical Android applications.