Abstract interpretation of mobile systems Jérôme Feret

Abstract interpretation of mobile systems Jérôme Feret

-

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

Description

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


Sujets

Informations

Publié par
Ajouté le 19 juin 2012
Nombre de lectures 14
Langue English
Signaler un abus
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
2
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, reconfigurable systems, biological systems, . . . .
Jérôme Feret
3
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: (confinment,confidentiality. . ), . 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
4
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
5
Wednesday, April the 20th
Jérôme Feret
6
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 (affine 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
7
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
8
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
9
Wednesday, April the 20th
Jérôme Feret
Dynamic linkage of agents
A

C
10

B

Wednesday, April the 20th