tel-00007549, version 1

Deux critères de sécurité pour l'exécution de code mobile

Hervé Grall () ¹

Ecole des Ponts ParisTech (2003-12-15), Cot Norbert (Dir.)

• 1:  Centre d'Enseignement et de Recherche en Mathématiques, Informatique et Calcul Scientifique (CERMICS)
• http://cermics.enpc.fr/
  INRIA – Ecole des Ponts ParisTech 6 et 8 avenue Blaise Pascal Cité Descartes - Champs sur Marne 77455 Marne la Vallée Cedex 2 France

Bibliographic reference

• Type of document: Thesis
• title: Deux critères de sécurité pour l'exécution de code mobile
• defence date: 2003-12-15
• 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.
• abstract in english: 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.
• subject:

  Computer Science/Software Engineering

  Mathematics

• institution: Ecole des Ponts ParisTech
• Alternative location: http://pastel.paristech.org/archive/00000713/
• language: French
• thesis advisor: Cot Norbert
• keyword(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
• comment: Membre du Jury: Leroy, Xavier et Cot, Norbert et Caucal, Didier et Jensen, Thomas et Lalement, René

Attached file list to this document: 

• tel-00007549, version 1
• http://tel.archives-ouvertes.fr/tel-00007549
• oai:tel.archives-ouvertes.fr:tel-00007549
• From: Admin PASTEL <>
• Submitted on: Monday, 29 November 2004 16:54:54
• Updated on: Sunday, 18 December 2005 13:45:17