Typage et Sécurité
Proposition de stage de Master 2ème année
Encadrement:
Gérard
Boudol
Adresse:
INRIA
2004 route des Lucioles, BP
93
06902 Sophia-Antipolis Cedex
Contact:
Gérard Boudol
téléphone : 04 92 38 79 40
Laboratoire d'accueil:
INRIA Sophia-Antipolis - Projet
MIMOSA
Pré-requis :
Fort intérêt pour les langages fonctionnels et impératifs ;
connaissance du typage à la ML; notions de sémantique
opérationnelle des langages de programmation ; notions sur la
programmation concurrente et la programmation synchrone.
Objectifs:
Etendre les résultats obtenus sur le typage pour la confidentialité dans
un langage à la ML avec déclassification. Plusieurs
directions sont envisagées : typage pour l'intégrité, polymorphisme,
inférence de type, typage avec des niveaux de sécurité dynamiques.
Description du sujet:
Le projet MIMOSA a débuté la conception et l'implantation d'un langage
pour la programmation mobile, appelé ULM [1]. Ce langage repose sur un
noyau fonctionnel et impératif, à la ML, auquel sont ajoutées les
constructions de la programmation
réactive, proches
de celles du langage synchrone ESTEREL, et une construction permettant
la migration de code. Une implantation prototype de ce noyau,
plongé dans le langage SCHEME, a été réalisée [2], en utilisant
le compilateur
Bigloo
développé dans le cadre du projet MIMOSA.
Le code mobile pose de nombreux problèmes, et tout spécialement du
point de vue de la sécurité. Nous avons commencé à travailler sur ces
problèmes, et en particulier sur l'aspect de la
confidentialité. Nous avons adopté une approche maintenant bien
établie de ``sécurité par typage'', qui consiste à définir, pour le
langage de programmation considéré, un système de types qui garantit
la propriété dite de ``non-interférence'' (voir [3]). C'est l'approche
adoptée pour Flow
CAML. Toutefois, nous avons très récemment étendu ce modèle [4],
de façon à accepter des programmes qui déclassifient leurs
données, comme par exemple une procédure de vérification de mot de
passe. Il est en effet largement reconnu que cette approche de
``sécurité par typage'' ne sera utilisable dans la pratique que si
elle incorpore d'une manière acceptable les programmes
``déclassifiants''. Ce travail sur la déclassification ouvre de
nombreuses perspectives, et nécessite des développements. Par exemple,
il devrait être relativement facile de traiter de façon similaire
l'aspect ``intégrité'' des préoccupations de sécurité,
puisqu'on peut le voir comme le dual de l'aspect
``confidentialité''. Le point de vue que nous adoptons pour traiter la
déclassification est que la politique de sécurité doit pouvoir varier
au cours du temps. Il serait par conséquent très intéressant de voir
comment ceci peut être combiné à la notion de niveau de sécurité
dynamique, telle qu'elle a par exemple été introduite dans [5],
qui semble importante dans la pratique. Une autre dimension à explorer
est celle du polymorphisme et de l'inférence de
type. C'est une dimension plus ``classique'' -- qui par exemple
est au cœur du système Flow CAML --, mais elle est indispensable
à une mise en œuvre des concepts, et notamment dans
l'implantation du langage ULM. Le stage proposé a pour objectif de
commencer à explorer ces perspectives et développements. Il est conçu
pour être prolongé par un travail de thèse de doctorat, qui
s'effectuera en particulier dans le cadre du projet CRISS
de l'ACI Sécurité Informatique.
Bibliographie:
[1] G. Boudol, ``ULM, a core programming model for global computing'',
ESOP'04, LNCS 2986 (2004)
pdf.
[2] S. Epardaud, ``Mobile reactive programming in ULM'', Scheme Workshop
(2004)
pdf.
[3] A. Sabelfeld and A. Myers, ``Language-based information-flow
security'', IEEE J. on Selected Areas in Communications Vol 21 No 1 (2003)
pdf.
[4] G. Boudol and A. Matos, ``On declassification and the non-disclosure
property'',
to appear in the proceedings of the Computer Security Foundations
Workshop, June 2005. A .pdf
is available.
[5] S. Tse and S. Zdancewic, ``Run-time principals in information-flow type
systems'', IEEE Symp. on Security and Privacy (2004)
pdf.