Research & Projects

Research activity

Security of Mobile Operating Systems

Mobile Operating Systems (e.g. Android, IoS, WindowsPhone) are software stacks built upon native OS kernels. The interactions between stack layers and the kernel may hide unexpected security weaknesses that can be overlooked by the available security mechanisms. This calls for new approaches to the security assessment and enforcement of mobile OSs. We are developing static analysis techniques and empirical studies to assess the security of mobile OSs that have already allowed us to unveil a number of security holes in Android, including a vulnerability associated with the Zygote process (affecting all Android-based devices in 2011) and other security flaws affecting the privacy of the user and the usability of the device (July 2012). Our proposed solutions have been officially adopted in Android.

Specification and Automatic Enforcement of BYOD Policies

It is common knowledge that mobile applications can carry viruses and malwares. Modern application stores do not provide actual guarantees about the behavior of the applications they host and, as a consequence, several malicious applications have been discovered in the last years. The concerns about the security of mobile devices risk to discourage the adoption of some emerging technologies as the Bring Your Own Device (BYOD). We research and implement technologies allowing for dealing with the security issues of mobile applications under these assumptions. In particular, we are investigating the notion of secure meta-market, i.e. web services specifically dedicated to applying BYOD security policies to a group of federated mobile devices. Further details about the development of the meta-market can be found here.

Model Checking of Security Protocols and Security-critical Systems.

SATMC is a SAT-based bounded model checker for security-critical systems that stems from a successful combination of encoding techniques originally developed for planning with others developed for the analysis of reactive systems. SATMC has been successfully applied in variety of application domains (security protocols, security-sensitive business processes, and cryptographic APIs) and for different purposes (design-time security analysis and security testing). SATMC strikes a balance between general purpose model checkers and security protocol analyzers as witnessed by a number of important success stories including the discovery of a serious man-in-the-middle attack on the SAML-based Single Sign-On (SSO) for Google Apps, an authentication flaw in the SAML 2.0 Web Browser SSO Profile, and a number of attacks on PKCS#11 Security Tokens. SATMC is integrated and used as back-end in a number of research prototypes (e.g. the AVISPA Tool, Tookan, the SPaCIoS Tool) and industrial-strength tools (e.g. the Security Validator plugin for SAP NetWeaver BPM).

Tools: SATMC.
Projects: AVISS, AVISPA, [email protected], AVANTSSAR, SPaCIoS.

Software Model-Checking.

The sophistication of software systems and the safety requirements posed by the increasingly complex environments they operate in call for higher and higher degrees of reliability. These requirements must be achieved precisely (i.e. not only at the design level, but also in the actual implementation). This calls for automated and effective verification techniques in the software development cycle. In this context Software Model Checking has recently become one of the leading approaches to automatic program analysis.

We contributed to the development of two software model checking techniques and tools: Symbolic model checking based of programs manipulating numeric data and arrays SMT-based bounded model checking of programs

Tools: Eureka, SMT-CBMC.
Projects: Decision Procedures for Software Model Checking

Synthesis, integration and combination of decision procedures.

Decision procedures are key components of verification tools. We have contributed to the development of a number of techniques for the synthesis, integration and combination of decision procedures for a variety of (decidable) theories of practical interest.

Tools: Constraint Contextual Rewriting, TSat++.
Projects: Deduction-based decision procedures for program analysis, Calculemus.