PROFUNDIS: Proofs of Functionality for Mobile Distributed Systems

[ Overview | Meetings | Visits | Events | Publications | Tools | Internal information ]


The objective of PROFUNDIS is to advance the state of the art of formal modelling and verification techniques to the point where key issues in mobile distributed systems, such as security protocols, authentication, access rights and resource management can be treated rigorously and with considerable automatic support. In particular we shall verify properties typical in so called open systems, where the behaviour of some parts (like intruders or adversaries) is unknowable, in extensible systems, where parts may be added or removed as the system executes, and in mobile systems where physical and logical connectivity between parts may change. We shall implement automatic and partly automatic analysis methods for ascertaining correct behaviour of such systems. For this purpose we shall integrate and focus several strands of ongoing theoretical work.

Description of work

The work builds on recent advances in key theories for process behaviours, logics and types. We shall develop automata theoretic models suitable for our applications, with a particular interest in how they can be represented efficiently and used by automatic tools, and we shall determine how they are best used in connection with advanced forms of modal logics. The logics themselves will be developed, both in terms of their expressiveness for properties related to space and structure, and in terms of their accessibility and ease of use through suitable high-level representations.

We shall identify and develop analysis techniques related to these models and logics. This involves traditional behavioural equivalences and preorder checking, systematic simulation, and verification in interactive proof assistants. Here type systems will play an important role. Recent results show that types may themselves be used as crude but tractable correctness properties and therefore type inference is highly relevant, moreover, we shall explore how advanced type information can assist the other analysis techniques.

The ideas will to a large extent be implemented in a common tool set. Key issues here will be development and adaption of algorithms for analysis, and determining the best way of using them for practical examples. We shall in particular consider examples on security properties in systems for electronic commerce.

Expected results

The results from the project will be of two kinds. First there will be a set of tools that automatically or with some manual assistance can treat the verification problems in the objectives above. The tools will be accompanied with a pragmatics, i.e., a guide for how they are effective for particular problems. Second the theories underpinning the tools will be demonstrated in scientific publications.

Structure: Work packages

PROFUNDIS consists of three technical Work Packages (WPs) outlined below. A fourth WP is devoted to project management. The project is divided among four sites: Uppsala (UU), Lisbon (FFCT), INIRIA Sophia Antipolis and Pisa. Each site is active in all work packages, to a degree that varies between sites and over years. Each work package has an appointed leader. The Steering Committee consists of the co-ordinator and all site and work package leaders. The technical work packages are:
WP1: Models (leader Ugo Montanari)
The objectives of the work package consist of the development of a HD-Automata model, suitable for finite-state verification, enhanced with additional capabilities like name fusions and substitutions. Also, versions of mobile calculi should be defined, e.g. for the symbolic analysis of security protocols. A verification environment should be designed and implemented, equipped with a general, open architecture and consisting of new tools realizing the models and the verification methods above. Several case studies should show the flexibility and effectiveness of our approach.
WP2: Specifications (leader Luis Monteiro)
The objectives of the work package are to develop new logics to support the verification of structural (spatial) and behavioural properties of concurrent mobile systems, and to develop proof systems for these logics based on sequent calculi. A tool for the logical framework should be built, integrated in the verification environment developed together with other tasks. The usefulness of the approach should be illustrated by several case studies.
WP3: Types (leader Davide Sangiorgi)
The objectives are to develop new type systems to control interferences among processes and the resources used by the processes; to integrate the type techniques with operational and logic techniques; to investigate the robustness of the type techniques and their algorithmic definitions; to assess the applicability of the techniques by means of case studies, and to implement some of the type algorithms and proof techniques.

Valid HTML 4.01! Web page: Björn Victor, latest update Tue, 07-Jan-2003 18:02 MET