Thèse
Année : 2003
Résumé
Mobile programs, like applets, are not only ubiquitous, but also potentially malicious. Therefore, the host system must grant that their execution is not dangerous for its resources. A solution is to execute mobile programs in a secured environment,
which enables controlling information flows between mobile programs and local resources, and accesses from mobile programs to local resources. We give two security criteria for executing mobile code. The first one deals with information flows, ensures confidentiality, is based on the code of the local environment, is accurate and undecidable ; the second one deals with access controls, ensures confinement, is based on the type of the local environment, is approximate and decidable.
which enables controlling information flows between mobile programs and local resources, and accesses from mobile programs to local resources. We give two security criteria for executing mobile code. The first one deals with information flows, ensures confidentiality, is based on the code of the local environment, is accurate and undecidable ; the second one deals with access controls, ensures confinement, is based on the type of the local environment, is approximate and decidable.
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.
Mots clés
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
Admin PASTEL : Connectez-vous pour contacter le contributeur
https://pastel.hal.science/tel-00007549
Soumis le : lundi 29 novembre 2004-16:54:54
Dernière modification le : jeudi 16 mai 2024-15:00:04
Archivage à long terme le : vendredi 2 avril 2010-21:28:05
Dates et versions
- HAL Id : tel-00007549 , version 1
Citer
Hervé Grall. Deux critères de sécurité pour l'exécution de code mobile. Génie logiciel [cs.SE]. Ecole des Ponts ParisTech, 2003. Français. ⟨NNT : ⟩. ⟨tel-00007549⟩
269
Consultations
420
Téléchargements