Modelli e tecniche di analisi formale per la sicurezza dei sistemi software (PRIN 2007)
Profile Card Research projectShare this record with your favourite social network:
- Starting date
- September 22, 2008
- Duration (months)
- Computer Science
- Person in charge
- Vigano' Luca
Identifying all these different kinds of vulnerabilities is extremely hard due to the complexity of reasoning about trust and security of services and the way they possibly interact in dynamic, service-oriented networks. As we illustrate in more detail in the section on the state of the art, the approaches that are currently available are not up to the task and new techniques must be devised to tackle this complexity. In this project, we will tackle it by formalizing and developing a panoply of different methodologies and technologies for the analysis of security and trust aspects of protocols and services in distributed networks. In particular, we aim to:
- Develop formal models of trust for ad-hoc networks, and integrate these models in a process calculus to allow for the analysis of security properties of such networks.
- Develop a distributed temporal logic for communicating agents that provides an intuitive but expressive language for formalizing both agent-specific and system-wide properties of distributed communicating processes.
- Develop formal languages and techniques based on abstract model-checking to support the formal specification of security services and requirements, their formal analysis, and their automated and validated composition.
- Extend the abstract non-interference framework in order to deal with, not only more powerful attackers, able to exploit probabilistic information, but also with attackers able to transform the program semantics for stealing the maximal amount of confidential information that is possible, also on data bases.
- Develop formal models and techniques for hierarchical compositional analysis of complex protocols that achieve security via cryptographic primitives, ensuring a faithful representation of computational aspects of protocols, as well as general abstraction techniques to reduce computational reasoning to high level symbolic arguments.
- Ministero dell'Istruzione dell'Università e della Ricerca
Funds: assigned and managed by the department
Syllabus: COFIN - Progetti di Ricerca di Interesse Nazionale
- Isabella Mastroeni
- Associate Professor
- Massimo Merro
- Associate Professor
- Augusto Parma
- Roberto Segala
- Full Professor