Driven by rapidly changing requirements and business needs, software systems and applications are undergoing a paradigm shift towards Service-Oriented Computing, where protocols and services are distributed over the communication network, which may be reconfigured dynamically in a demand-driven way. Exposing services in such dynamic network infrastructures entails a wide range of trust and security issues, leading to new subtle and dangerous vulnerabilities due to interference between component services and the security policies they abide by, the shared communication layer, and application functionality. Moreover, one also must consider the underlying cryptography as services and applications might suffer from attacks that depend on the concrete cryptographic algorithms and mechanisms employed.
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.