Static Analysis

Verifying the security of modern applications is an important and complex challenge, which has attracted the interest of a growing research community in the last few years. Static analysis is a prominent approach in the area, based on the computation of a sound over-approximation of the program behavior which accounts for all the possible executions: if the computed over-approximation enjoys the expected security guarantees, then all the possible program runs will also do it. Static analysis provides a tractable solution to many normally intractable software verification problems.

Static analysis is efficient and excellent at ensuring the coverage of the full state space of the program to analyse. It is particularly important when runtime security monitors cannot be deployed, for instance for performance or backward compatibility reasons. Also, a few security properties may be hard or even impossible to guarantee at runtime, because the detection of a security violation may only occur too late: for instance, halting a program to stop an information leakage may actually reveal that the program was computing something over confidential data, which may turn out to be a privacy concern by itself.

The ACADIA Center has a long-standing tradition on static analysis research, providing significant contributions in many sub-area of this rich field, ranging from type systems to abstract interpretation techniques. Example application areas include mobile security and access control systems.

Selected publications

  1. A. Cortesi, P. Ferrara, R. Halder, M. Zanioli – Combining symbolic and numerical domains for information leakage analysis, in Transactions on Computational Science (2018)
  2. S. Calzavara, I. Grishchenko, A. Koutsos, M. Maffei – A sound flow-sensitive heap abstraction for the static analysis of Android applications, in IEEE Computer Security Foundations Symposium (2017)
  3. S. Chakraborty, A. Cortesi, N. Chaki – A uniform representation of multi-variant data in intensive-query databases, in Innovations in Systems and Software Engineering (2016)
  4. S. Calzavara, A. Rabitti, E. Steffinlongo, M. Bugliesi – Static detection of collusion attacks in ARBAC-based workflow systems, in IEEE Computer Security Foundations Symposium (2016)
  5. S. Calzavara, I. Grishchenko, M. Maffei – HornDroid: Sound and practical static analysis of Android applications by SMT solving, in IEEE European Symposium on Security and Privacy (2016)
  6. R. Halder, A. Jana, A. Cortesi – Data leakage analysis of the Hibernate query language on a propositional formulae domain, in Transactions on Large-Scale Data- and Knowledge-Centered Systems (2016)
  7. S. Calzavara, A. Rabitti, M. Bugliesi – Compositional typed analysis of ARBAC policies, in IEEE Computer Security Foundations Symposium (2015)
  8. S. Calzavara, M. Bugliesi, S. Crafa, E. Steffinlongo – Fine-grained detection of privilege escalation attacks on browser extensions, in European Symposium on Programming (2015)
  9. M. Bugliesi, S. Calzavara, F. Eigner, M. Maffei – Affine refinement types for secure distributed programming, in ACM Transactions on Programming Languages and Systems (2015)
  10. A. Cortesi, P. Ferrara, M. Pistoia, O. Tripp – Datacentric semantics for verification of privacy policy compliance by mobile applications, in International Conference on Verification, Model Checking, and Abstract Interpretation (2015)
  11. G. Costantini, P. Ferrara, A. Cortesi – A suite of abstract domains for static analysis of string values, in Software, Practice and Experience (2015)
  12. A. Cortesi, G. Costantini, P. Ferrara – The abstract domain of trapezoid step functions, in Computer Languages, Systems & Structures (2015)