Ph.D. Thesis Defense
Analysis of mobile systems by abstract interpretation
Jérôme Feret
Defended the 25th of February 2005
École Polytechnique
This thesis has been done at Laboratoire d'Informatique of the École Normale Supérieure (Paris)
- PhD advisor
- President
- Reviewers
- M. Luca Cardelli
- M. David Schmidt
- Examiners
- M. Vincent Danos
- M. Roberto Giacobazzi
- M. Jean Goubault-Larrecq
A mobile system is a pool of agents that
may interact with each other.
These interactions dynamically change the system by controlling both creation and destruction of links between agents. These interactions also control the creation of new agents.
The size of a mobile system evolves during its computation. This size may be unbounded.
A mobile system may describe telecommunication networks, reconfigurable systems, client-server applications, cryptographic protocols, or biological systems.
Several models are available according to the application field and the granularity of the observation level.
In this thesis, we propose an unifying framework to discover and prove automatically and statically some properties of mobile systems. We propose a meta-language to encode the most current models for mobility (the pi-calculus, the ambients, the join-calculus, the spi-calculus, the bio-ambients, and so on). The meta-language provides an operational semantics for each encoded model. In these semantics, each agent is identified with the history of its creation, so that this semantics avoids the use of alpha-conversion.
We then use the Abstract Interpretation framework to derive abstract semantics, which are sound, decidable, but approximate.
In this thesis, we give three generic semantics that we set according to the expected trade-off between accuracy and efficiency.
The first analysis focuses on dynamic properties: it captures relations about the creation histories of the agents of the system. This analysis is precise enough to distinguish recursive instances of each agent, even when there is an unbounded number of instances. Thus, we can prove in the case of a client-server application that the server always returns data to the right client.
The second analysis focuses on concurrency properties: it counts the number of occurrences of agents inside the system. This analysis detects mutual exclusion and it bounds the number of agents.
The third analysis mixes concurrency and dynamic properties. It gathers the agents of the system in several computation units. Then, it abstracts the number of occurrences of agents in each computation unit. For instance, we can prove the absence of race in the specification of a shared-memory with dynamic allocation that is written in the pi-calculus.
Final version can be downloaded at:
https://www.di.ens.fr/~feret/thesis/thesis.pdf
- Slides of the 45mn presentation are available in various format:
- postscript (ps)
- compressed postscript (ps.gz)
- portable document (pdf)
- Slides of the presentation at PPS concurrency working group
- First session 10/03/2005
- postscript (ps)
- compressed postscript (ps.gz)
- portable document (pdf)
- Second session 31/03/2005
- postscript (ps)
- compressed postscript (ps.gz)
- portable document (pdf)
- Third session 16/06/2005
- postscript (ps)
- compressed postscript (ps.gz)
- portable document (pdf)
Natacha's Photos
Xavier's Photos
David's Photos
Prototypes can be used on line (Computation are made on a Pentium III, 500 MHz, with 128 Mb RAM. There is a time out (after a couple of minutes).
Context-free analysis is only implemented in the pi-calculus analyzer.
Analysis examples (These results have been computed on a amd Opteron 248, with 8 Gb of RAM)
Chap. 2: the pi-caluclus
Analysis results are computed with default parameters (non-uniform analysis (
Loc1) and occurrence counting analysis (distinguishing each kind of transition label / affine equalities + intervals))
Chap. 3: the ambient calculus
Analysis results are computed with default parameters (non-uniform analysis (
Loc1) and content analysis (distinguishing each kind of transition label / affine equalities + intervals))
Chap. 8: environment analysis
Only environment analysis is computed, with default parameters (non-uniform analysis (
Loc1)). Occurrence counting analysis is disabled.
Analyses in Sect 8.3 are not implement yet.
Chap. 9: occurrence counting analysis
Only occurrence counting analysis is computed (with our product between of affine equality domain and interval domain).
We partition transtion labels into a linear (with respect to the size of the initial state) number of classes.
We also use a uniform control flow analysis.
Chap. 10: thread partitioning
(not implementet yet)
Only implemented for mobile ambients. For the pi-calculus, we give results of environment analysis.
- Example 10.1.1: shared memory
The confidentiality proof requires the analyses proposed in
Sect. 8.3, which are not implemented yet. Confidentiality can be
infered for the simplified version of the example by using analyses
proposed in Sect. 8.2. The absence of race conditions requires analyses
proposed in Chap. 10, which are not implemented yet.
- original
- without context
- simplified
- Example 10.2.2: token-server in ambients