May 7, 2017
This project targets the design of (certified) mechanisms able to proactively understand the behaviour of platforms that deploy technologies for mobile devices in order to detect/prevent vulnerable states of those platforms. To that end we aim at integrating the use of formal security models and certified proofs of properties that may be used to enforce or violate security policies with methods and techniques capable of collecting and analyzing information residing in mobile devices as well as the events that provoke creation, modification and (potentially unsecure) flow of that information. We focus on the Android platform as the technology reference in which the developed methods and techniques conducted in this project shall be contrasted. Android is an attractive platform for several reasons. In particular Android applications run on smart phones, and these devices manage a tremendous amount of personal information such as passwords, locations, and social network data. In addition, the large number of devices enabled to host this platform makes Android an obvious target for the application of the results of the project.