(PRIN 2010-11 project)
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.
The methodology we aim at will rely on logically based theories, on game theory, and on the formal semantics of languages. Our framework will offer tools for formally analyzing the behavior of systems, both at design- and at run-time, and tools for securely composing them, monitoring their execution and evaluating/reducing the risk of dysfunctional behavior. The existing analysis tools (developed by the programming languages community and by the formal security one) are not up to this task but instead require significant extensions to take care of the distributed nature of the systems of interest and of the impact that quantitative aspects of their behavior have on the usability of software services and infrastructures.
Our validation activities will show that the project results can be practically and profitably applied also in real-world scenarios. To this aim, we will crucially rely on two case studies, which we plan to model, analyse and implement with the tools developed in the project. The first case study concerns an Internet of Things & Services (IoTS) infrastructure, that can securely host and run services developed by different parties.
The secure-IoTS is a core ICT application in innovative and secure societies, and will play the role of a conceptual and a concrete playground for Security Horizon ideas. The second case study will concern a Healthcare Management System. The case studies will provide the necessary feedback to evaluate the formal tools produced by the project, and they will guide the project investigators in refining and extending the developed theories according to the obtained results.
The project will lead to an advancement in the design and understanding of secure systems, witnessed by the development of usable models and analysis techniques. This will improve the reliability and security of current and future digital societies, by giving users and developers of the underlying systems provable guarantees about the behaviour of these societies.
The eight research units involved in the project can effectively pursue these goals by joining their expertise on many topics related to the fields of security and formal methods, among which programming languages, concurrency theory, static analysis, model checking, logics, game theory, risk analysis. The involved research units cover a significant part of the italian researchers active in the area of interest. They have often collaborated in different national and European projects, but they have never gathered in a single network. We expect that the existing cooperations with our foreign academic partners will be beneficial for all the participants, and will foster the dissemination of the project results.