09/01/2003
Cédric Lhoussaine (University of Sussex)
Un système de types dépendants pour les ambients mobiles

Nous présenterons un travail en cours concernant un système de types permettant la vérification de propriétés de sécurité pour les ambients mobiles. Après une introduction du modèle des ambients, nous montrerons brièvement un système de types garantissant l'absence d'attaques de type « cheval de Troie » proposé par Merro & Sassone. Ce système utilise la notion de « groupe ». Un groupe est un constructeur de types qui apparaît explicitement dans le calcul. Nous présenterons une version de ce système de types qui utilise des types dépendants et qui permet de s'abstenir des groupes. Ce nouveau système présente l'avantage d'utiliser des types plus simples et de pouvoir traiter le problème de l'inférence de types qui est crucial pour les systèmes à grande échelle. Il offre aussi une forme de dynamicité au typage.