Abstract Interpretation-Based Static Analysis of Mobile Ambients

Abstract : We use Abstract Interpretation to automatically prove safety properties of mobile ambients with first order communications. We introduce a non-standard semantics in order to distinguish different recursive instances of agents. This allows us to specify explicitly both the link between agents and the ambient names they have declared, and the link between agents and the ambients they have activated. Then we derive from this non-standard semantics an abstract semantics which focuses on interactions between agents. This abstract semantics describes non uniformly which agents can be launched in which ambients and which ambient names can be communicated to which agents. Such a description is required to prove security properties such as non-interference or confinement for instance.
Type de document :
Communication dans un congrès
Cousot Patrick. the 8th International Symposium on Static Analysis (SAS'01), Jul 2001, Paris, France. Springer, 2126, pp.413--431, 2001, Lecture Notes in Computer Science. 〈10.1007/3-540-47764-0_24〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00527929
Contributeur : Jérôme Feret <>
Soumis le : mercredi 20 octobre 2010 - 16:05:36
Dernière modification le : mardi 24 avril 2018 - 17:20:12

Identifiants

Collections

Citation

Jérôme Feret. Abstract Interpretation-Based Static Analysis of Mobile Ambients. Cousot Patrick. the 8th International Symposium on Static Analysis (SAS'01), Jul 2001, Paris, France. Springer, 2126, pp.413--431, 2001, Lecture Notes in Computer Science. 〈10.1007/3-540-47764-0_24〉. 〈inria-00527929〉

Partager

Métriques

Consultations de la notice

252