Local coordinator: Massimo Bartoletti
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.