Security Horizons

Post date: 24-Oct-2012 18:07:33

The PRIN 2010-11 project "Security Horizons" has been funded by the MIUR, with D. D. 23.10.2012 n. 719.

National coordinator: Pierpaolo Degano

Local coordinator: Massimo Bartoletti

Abstract.

Society increasingly depends on complex ecosystems of interacting software components. The number and variety of security-critical applications that rely on these systems has also grown over the years, and this trend will foreseably continue in the future. Despite of the applications being security-critical, they are still far from being secure: every day security researchers (and, more dangerously, hackers) discover new attacks to these systems. While perfect security is not a reachable goal, the current situation where security is intended as a marketing word and not as a concrete guarantee, can and must be improved.

Unfortunately, the problem of realizing software components that securely interact in an insecure environment is extremely hard to solve. This has many causes, among which the heterogeneity of the software components, the fact that they are controlled by different entities with possibly conflicting goals, the fact that attacks may take an unpredictable variety of different forms, etc.

A reasonable goal is to focus on some specific security properties, and prove that they are enjoyed by the application, even in the presence of attackers. This requires the development of new techniques to design, analyse, and implement software components. We are confident that Security Horizons will lead to an important advancement in that direction.

This project aims at developing a rigorous methodology and a language-based framework that will provide formal methods to support software engineers when they design, implement and maintain secure systems. This support will span all the software development phases: specification, design, implementation, validation, including verification and testing. To this end, we will study models and specification languages that allow one to formally express the many facets of online services and of their hosting infrastructures.