tel-00007549, version 1
Deux critères de sécurité pour l'exécution de code mobile
Ecole des Ponts ParisTech (2003-12-15), Cot Norbert (Dir.)
Abstract: Les programmes mobiles, comme les applettes, sont utiles mais potentiellement hostiles, et il faut donc pouvoir s'assurer que leur exécution n'est pas dangereuse pour le système hôte. Une solution est d'exécuter le programme mobile dans un environnement sécurisé, servant d'interface avec les ressources locales, dans le but de contrôler les flux d'informations entre le code mobile et les ressources, ainsi que les accès du code mobile aux ressources. Nous proposons deux critères de sécurité pour l'exécution de code mobile, obtenus chacun à partir d'une analyse de l'environnement local. Le premier porte sur les flux d'informations, garantit la confidentialité, est fondé sur le code de l'environnement, et est exact et indécidable ; le second porte sur les contrôles d'accès, garantit le confinement, s'obtient à partir du type de l'environnement, et est approché et décidable. Le premier chapitre, méthodologique, présente l'étude d'objets infinis représentés sous la forme d'arbres. Nous avons privilégié pour les définir, une approche équationnelle, et pour raisonner sur eux, une approche déductive, fondée sur l'interprétation co-inductive de systèmes d'inférence. Dans le second chapitre, on montre dans le cas simple du calcul, comment passer d'une sémantique opérationnelle à une sémantique dénotationnelle, en utilisant comme dénotation d'un programme son observation. Le troisième chapitre présente finalement en détail les deux critères de sécurité pour l'exécution de code mobile. Les techniques développées dans les chapitres précédents sont utilisées pour l'étude de la confidentialité, alors que des techniques élémentaires suffisent à l'étude du confinement.
- 1:
- INRIA – Ecole des Ponts ParisTech
- Domain : Computer Science/Software Engineering
Mathematics - Keywords : Logique mathématique – Systèmes d'inférence – Définitions inductives et co-inductives – treillis – informatique théorique – équations récursives – arbres – Lambda-calcul – langages de programmation – sémantiques opérationnelle et dénotationnelle – sécurité informatique – mobilité – flux d'informations – confidentialité – contrôles d'accès – confinement
- Comment : Membre du Jury: Leroy – Xavier et Cot – Norbert et Caucal – Didier et Jensen – Thomas et Lalement – René
- tel-00007549, version 1
- http://tel.archives-ouvertes.fr/tel-00007549
- oai:tel.archives-ouvertes.fr:tel-00007549
- From:
- Submitted on: Monday, 29 November 2004 16:54:54
- Updated on: Sunday, 18 December 2005 13:45:17




Associated documents

Export