Abstract interpretation of mobile systems Jérôme Feret

Jérôme Feret

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

• Abstract interpretation

Informations

• Publié par: pefav
• Nombre de lectures: 14
• Langue: English

Extrait

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 a META -language; 2. design of static analysis at the level of the META -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