Tag Archives: Static Analysis

09/03/2016 – Talk by Stefano Calzavara

Title:  HornDroid: Practical and Sound Static Analysis of Android Applications by SMT Solving
Time: 13:30
Location: Meeting room, building Zeta
Type: Research Result
Speaker: Stefano Calzavara
Abstract:
We present HornDroid, a new tool 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 an off-the-shelf SMT solver. This approach makes it possible to fine-tune the analysis in order to achieve a high degree of precision while still using off-the-shelf verification tools, thereby leveraging the recent advances in this field. As a matter of fact, HornDroid outperforms state-of-the-art Android static analysis tools on benchmarks proposed by the community. Moreover, HornDroid is the first static analysis tool for Android to come with a formal proof of soundness, which covers the core of the analysis technique: 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.

25/01/2016 – Talk by Pierpaolo Degano

Title:  Context-aware Security: Linguistic Mechanisms and Static Analysis
Time: 14:00
Location: Meeting room, building Zeta
Type: Research Result
Speaker: Pierpaolo Degano
Abstract:
Adaptive systems improve their efficiency by modifying their behaviour to respond to changes in their operational environment. Also, security must adapt to these changes and policy enforcement becomes dependent on the dynamic contexts. We study these issues within (the core of) an adaptive declarative language proposed recently. A main characteristic of this language is to have two components: a logical one for handling the context and a functional one for computing. We extend it with security policies that are expressed in logical terms. They are of two different kinds: context and application policies. The first, unknown a priori to an application, protect the context from unwanted changes. The others protect the applications from malicious actions of the context, can be nested and can be activated and deactivated according to their scope. An execution step can occur only if all the policies in force hold, under the control of an execution monitor. Beneficial to this is a type and effect system, which safely approximates the behaviour of an application, and a further static analysis, based on the computed effect. The last analysis can only be carried on at load time, when the execution context is known, and it enables us to efficiently enforce the security policies on the code execution, by instrumenting applications. The monitor is thus implemented within the language itself, and it is only activated on those policies that may be infringed and switched off otherwise.

Short bio
Pierpaolo Degano has been

  • since 1/11/1990 full Professore in computer science, since 1993 at Dipartimento di Informatica, Università di Pisa
  • 1993-96 head of the Dipartimento di Informatica, Università di Pisa
  • 2000-2003 Chairman of GRIN, the Italian Association of the Professors of Computer Science
  • since 2001 member of the scientific committee of the Scuola di Dottorato di Eccellenza “Galileo Galilei”, since 2009 vice-chairman
  • since 2006 head of the PhD programme in Computer Science
  • since 2007 chairman of the Italian Committee of PhD programmes in Computer Science
  • since 2005 member of the scientific committee of CoSBi, the Microsoft Research – University of Trento Centre for Computational and Systems Biology

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
Abstract: 
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.

25/02/2015 Talk by Stefano Calzavara

Title: Compositional Typed Analysis of ARBAC Policies
Time: 14:00
Location: Meeting room
Type: Research Result
Speaker: Stefano Calzavara
Abstract:

Model-checking is a popular approach to the security analysis of ARBAC policies, but its effectiveness is hindered by the exponential explosion of the ways in which different users can be assigned to different role combinations. In this talk we propose a paradigm shift, based on the observation that, while verifying ARBAC by exhaustive state search is complex, realistic policies often have rather simple security proofs, and we propose to use types as an effective tool to leverage this simplicity. Concretely, we present a static type system to verify the security of ARBAC policies, along with a sound and complete type inference algorithm used to automate the verification process. We then introduce compositionality results, which identify sufficient conditions to preserve the security guarantees obtained by the verification of different sub-policies when these sub-policies are combined together: this compositional reasoning is crucial when policy administration is highly distributed and naturally supports the security analysis of evolving ARBAC policies. We evaluate our approach by implementing TAPA, a static analyser for ARBAC policies based on our theory, which we test on a number of relatively large, publicly available policies from the literature.

30/09/2013 – Talk by Giulia Costantini

Title: Lexical and Numerical Domains for Abstract Interpretation
Time: 10:00
Location: Meeting room
Type: PhD program result
Speaker: Giulia Costantini
Abstract:

The goal of this thesis is to contribute to the field of formal methods employed for the static verification of computer program properties. The context is the Abstract Interpretation framework, one of the various possible techniques to perform static analyses. In particular, we focus on the design of novel abstract domains to analyze the basic building blocks of computer programs: lexical and numerical variables, as well as relationships between variables. In order to provide experimental evidence of their actual applicability, we implemented our domains and we applied them to a suite of case studies.