07/04/2014: Talk by Pietro Ferrara (IBM Research)

Title: MorhpDroid: Fine-grained Privacy Verification
Time: 14:00
Location: Meeting Room, building Zeta
Type: Research result
Speaker: Pietro Ferrara
Mobile devices are rich in sensors, such as a Global Positioning System (GPS) tracker, microphone and camera, and have access to numerous sources of personal information, including the device ID, contacts and social data. This richness increases the functionality of mobile apps, but also creates privacy threats. As a result, different solutions have been proposed to verify or enforce privacy policies. A key limitation of existing approaches is that they reason about privacy at a coarse level, without accounting for declassification rules, such that the location for instance is treated as a single unit of information without reference to its many fields. As a result, legitimate app behaviors — such as releasing the user’s city rather than exact address — are perceived as privacy violations, rendering existing analyses overly conservative and thus of limited usability.

In this talk, I will present MorphDroid, a novel static analysis algorithm that verifies mobile applications against fine-grained privacy policies. Such policies define constraints over combinations
of fine-grained units of private data. Specifically, through a novel design, MorphDroid tracks flows of fine-grained privacy units while addressing important challenges, including (i) detection of
correlations between different units (e.g. longitude and latitude) and (ii) modeling of semantic transformations over private data (e.g. conversion of the location into an address).
We have implemented MorphDroid, and present a thorough experimental evaluation atop the 500 top-popular Google Play applications in 2014.
Our experiments involve a spectrum of 5 security policies, ranging from a strict coarse-grained policy to a more realistic fine-grained policy that accounts for declassification rules. Our experiments show that the gap is dramatic, with the most conservative policy detecting violations in 171 of the applications (34%), and the more realistic policy flagging only 4 of the applications as misbehaved (< 1%). In addition, MorphDroid exhibits good performance with an average analysis time of < 20 seconds, where on average apps consist 1.4M lines of code. Short Bio: 
Pietro has been an IBM Research Staff Member in the group of Mobile Enterprise Software led by Marco Pistoia since July 2013. His main research interest is sound static analysis via abstract interpretation. In particular, he is currently working on various security (mostly confidentiality) properties of mobile (mostly Android) programs. Before joining IBM Research, Pietro was a lecturer at ETH of Zurich in the Programming methodology group under the supervision of Peter Mueller from April 2009 to July 2013. In this period, he developed Sample, a generic static analyzer developed in Scala that has been applied to a large variety of properties and programming languages. Previously (from October 2005 to May 2009), he was a PhD student at the Ecole Polytechnique of Paris and the Università Ca’ Foscari of Venice, under the join supervision of Radhia Cousot and Agostino Cortesi.