Who: Matteo Maffei\
When: Thursday, {{ page.date | date_to_long_string }}, 13:30-14:30\
Where: Room 3364\
Title: {{ page.title }}
Abstract:\
In this talk, I will present two ongoing projects on the formal
verification of security properties for mobile and web
applications.
In the first part, I will present HornDroid, a novel technique for the static analysis of information flow properties in Android applications. The core idea underlying HornDroid is to use Horn clauses for soundly abstracting the semantics of Android applications and to express security properties as a set of proof obligations that are automatically discharged by SMT solving. This approach makes it possible to fine-tune the analysis in order to achieve a high degree of precision while still relying on off-the-shelf verification tools, thereby automatically leveraging the recent advances in this field. As a matter of fact, HornDroid outperforms in precision state-of-the-art Android static analysis tools on benchmarks proposed by the community, besides being orders of magnitude faster. Moreover, HornDroid is the first static analysis tool for Android to come with a formal proof of soundness: besides yielding correctness assurances, this proof allowed us to identify some critical corner-cases that affect the soundness guarantees provided by some of the previous static analysis tools for Android.
In the second part, I will present Michrome, a security enforcement tool for web applications based on micro-policies. Micro-policies, originally proposed to implement hardware-level security monitors, constitute a flexible and general enforcement technique, based on assigning security tags to system components and taking security actions based on dynamic checks over these tags. In this work, we present the first application of micro-policies to web security, by proposing a core browser model supporting them and studying its effectiveness at securing web sessions. In our view, web session security requirements are expressed in terms of a simple, purely declarative information flow policy, which is then automatically translated into a micro-policy implementing it. This leads to a browser-side enforcement mechanism which is elegant, sound and flexible, while being accessible to web developers. We show how a large class of attacks against web sessions can be uniformly and effectively prevented by the adoption of this approach. Since we carefully designed micro-policies with ease of deployment in mind, we are also able to implement our proposal as a Google Chrome extension, Michrome: our experiments show that Michrome can be easily configured to enforce strong security policies without breaking the websites functionality.
Biographical Note
Matteo Maffei is professor at Saarland University and CISPA, where he leads the Secure and Privacy-preserving Systems group. He received his Ph.D. in Computer Science from the University of Venice in 2006. Matteo’s research interests are in the area of formal methods for security analysis, with a focus on cryptographic protocols, mobile security, and web security, as well as privacy-enhancing technologies, in particular zero-knowledge proofs, oblivious RAM, and differential privacy. He was granted the Emmy Noether fellowship from the German research foundation in 2009, he served in the programme committee of more than 40 conferences, and he is currently the regular columnist on security and privacy of the ACM SIGLOG newsletter.ill be summarized and I will discuss future research directions on data anonymization.
{: .t60 } {% include list-posts tag=‘csstalk’%}