About Me

Graduated in Mathematics at the University of Pisa in the 2003 and gaining a Master in "Internet Technology", since July 2004 I work as a researcher in the security group of the Institute of Informatics and Telematics of the CNR in Pisa. This collaboration has been started after a stage of 400 hours during the my Master dealing with formal methods for information security. In April 2008 I have obtained my PhD in Theoretical Computer Science and Logic (LoMIT) at the University of Siena. I currently work as a researcher in the security group of the IIT-CNR in Pisa. My research interests include the study of process algebra based techniques for the analysis and the run-time enforcement of security and privacy properties and quantitative measures for security. I participated in several National and European projects (FP6, FP7, PRIN, H2020) in the area of information security applied to web services, healthcare, and critical infrastructure, and so on.

Automotive Cyber-Security

My research interest on Automotive Cyber-Security focuses on the CAN-bus protocol and, in particular, the security property such as Confidentiality, Integrity and Authentication. Android-based radio system is also part of my research activity in automotive. In particular, we exploit Android Radio to remotely access the car and read data coming from car's sensors. These involve the parking-camera, the internal microphone, GPS, and other CAN-bus information, like engine RMP, fuel, brakes and others.
For furthre details, see the Automotive tab or the sowhat R&D group webpage.

Critical Infrastructure Protection

This activity is developed within the project PRIN TENACE and it has the objective of defining techical solution and methodologies to protect Critical Infrastructures, with the specific target of developing an unifying metodology and understanding the underground economics fuelling an attacker. Within this activity, the main goal is the identification of specific CI vulnerabilities and related attacks in order to drive the development of algorithms, models, architectures and tools to enable the effective protection of such critical infrastructures enhancing their degree of security and dependability by considering a continuously evolving adversary.
See publications for further details.

Privacy policy for Data-Sharing: Specification, Analysis, and Refinement

As part of the project MobiCare, a project that is internally funded by the Registro.it of the IIT-CNR, research activities are made in two directions: 1) the development of an expertise-driven authoring tool for setting privacy policies on medical data; 2) a detection and resolution strategy for conflicts occurring among policies written by different entities having rights on the same data.
Within the European project FP7-Consequence, I studied methods of qualitative analysis of security policies for data sharing. Furthermore, in both projects FP7-Consequence and FP7-Coco CLoud I developed an action refinements theory to data sharing policies to ensure that security requirements are preserved by a system through the various levels of abstraction. Indeed, the considered concept of refinement consists in the passage among several abstraction levels of the specification of a given security property from the specification level to the implementation (or however, a low-level representation) one. I also supervised the implementation of a DSA Mapper tool able to translate DSA policies from a Controlled Natural Language to XACML-based enfoceable policies.
See publications for further details.

Logic and formal methods for Qualitative and Quantitative Security

This activity extends a research stream on formal method and open system paradigm for the specification, analysis, and synthesis of secure systems. Modal logics are used for expressing security properties that systems have to satisfy to be secure. The considered security policies are safety, non-interference, and fault tolerant properties. According to the chosen approach, these policies are specified in a language based on process algebra.

The synthesis activity aims at generating mechanisms to monitor and, if necessary, force the behavior of those components of the system that could be malicious. The behavior of the component of the system is described through process algebra operators and the security requirements are expressed through modal logic. The proposed synthesis method is then used in several areas, such as web services, security of mobile devices and distributed systems. Investigations were carried out within the European project FP6-S3MS and project FP7-CONNECT.

Recently I go further on these activities by considering not only the qualitative aspects of security but also considering security as a "quantitative" property, by taking into account probability, dependability, and risk aspects. As part of the SESAMO project, the trade off of possible synergies between security and safety has been investigated.
See publications for further details.

Software development for an automatic generation of controllers and service composition.

As part of the project FP6-S3MS, software has been developed for the generation of secure systems. In particular, there was implements a procedure for the automatic generation of automata that satisfy a given safety property. This application was developed in O’caml. The project FP6-S3MS has driven the implementation of application able to compare two policies w.r.t. the concept of symbolic simulation (contract-policy matching). This application was developed in Java2ME. As part of the project FP7-Aniketos, a method and a prototype implementation of compliance checking is provided in such a way that it performs a static analysis for guaranteeing that the behaviors of a service or of a composition of services respects what they promise to do. These studies have given rise to a prototype implementation that has been integrated in the platform developed within the project.
See publications for further details.