Security Horizons 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.

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 cooperation with our foreign academic partners will be beneficial for all the participants, and will foster the dissemination of the project results.