Abstract interpretation of mobile systems Jérôme Feret

138

pages

English

Documents

Écrit par
Jérôme Feret

Publié par
pefav

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

138

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

pefav

Nombre de lectures

Langue

English

Università di Bologna Abstract interpretation of mobile systems Jérôme Feret Laboratoire d'Informatique de l'École Normale Supérieure INRIA, ÉNS, CNRS feret Wednesday, April the 20th

laboratoire d'informatique de l'ecole normale

abstract interpretation

process creation

mobile system

links between

Voir

Publié par

pefav

Nombre de lectures

Langue

English

Abstract interpretation

Università di Bologna

Abstract interpretation of mobile systems

Jérôme Feret Laboratoire d'Informatique de l'École Normale Supérieure INRIA, ÉNS, CNRS http://www.di.ens.fr/∼feret

Wednesday, April the 20th

1. 2. 3. 4. 5. 6. 7. 8.

Overview

Overview Mobile systems Non standards semantics Abstract Interpretation Environment analyses Occurrence counting analysis Thread partitioning Conclusion

Jérôme Feret

Wednesday, April the 20th

Mobile system

A pool of processes which interact and communicate: Interactions control: •process synchronization; •update of link between processes (communication, migration); •process creation. The number of processes may be unbounded ! Applications: •communication protocols, •cryptographic protocols, •reconﬁgurable systems, •biological systems, •. . . .

Jérôme Feret

Wednesday, April the 20th

Outline We design abstract semantics: •sound,automatic,decidable, •butapproximate(indecidability).

Our approach is model-independent: 1. design of aMETA-language; 2. design of static analysis at the level of theMETA-language.

Three family of analyses: 1. static analysis ofthe dynamic links between components: (conﬁnment,conﬁdentiality. . ), . 2.counting the number of components: (mutual exclusion,non-exhaustion of resources. . ), . 3. static analysis of computation units: (race detection,authentication,update integrity,. . . ).

Jérôme Feret

Wednesday, April the 20th

Static analysis of the dynamic links between components Which components may interact with each other?

client creation

clients

server instances

server

The analysis distinguishes between recursive components Abstract domain:relations among words. Publications: Feret — SAS'00, SAS'01, ESOP'02, JLAP'05

Jérôme Feret

Wednesday, April the 20th

Jérôme Feret

Static analysis of the number of component Bound the number of components

instances du serveur

clients

Wednesday, April the 20th

création des clients

Abstract domain:numerical relations (afﬁne and interval invariants). Publication : Feret — GETCO'00, JLAP'05

serveur deux ports

client rouge en attente...

Thread partitioning

Idea: •gather components in computation units, =⇒thanks to the analysis of linkage between components ; •count the number of components within each computation unit, =⇒thanks to the occurrence counting analysis. Advantage: •each session is isolated,

which enables the analysisto focus to each session.

Jérôme Feret

Wednesday, April the 20th

1. 2. 3. 4. 5. 6. 7. 8.

Overview

Overview Mobile systems Non standards semantics Abstract Interpretation Environment analyses Occurrence counting analysis Thread partitioning Conclusion

Jérôme Feret

Wednesday, April the 20th

Mobile system

A pool of processes which interact and communicate:

Interactions control:

•process synchronization; •update of link between processes (communication, migration); •process creation.

The number of processes may be unbounded !

Jérôme Feret

Wednesday, April the 20th

Jérôme Feret

Dynamic linkage of agents

��