Monday 25 January 2010
14h30, Room 0C8, ground floor
175 rue du Chevaleret, Paris, 75013
Sûreté des abstractions et Sessions sécurisées dans les langages distribués
Pierre-Malo Deniélou
Résumé :
Les systèmes répartis, ou systèmes distribués, tiennent aujourd’hui un rôle critique dans notre société et dans notre industrie. Cette thèse explore deux approches permettant aux programmeurs d’obtenir des garanties fortes de sûreté et de sécurité pour leurs programmes distribués. Dans un premier temps, nous étudions la généralisation des types abstraits de données à la programmation distribuée. Nous partons d’un système de typage préexistant que nous rendons plus flexible par l’ajout de sous-typage. Ceci permet de prendre en compte certains phénomènes comme les mises à jour de programmes et de bibliothèques. Nos propriétés de sûreté sont garanties lorsque tous les participants sont bien typés et le réseau est fiable. Notre système permet alors de s’assurer que les propriétés locales des types abstraits sont préservées dans le contexte distribué. Notre seconde partie s’intéresse aux sessions, une construction permettant de chorégraphier les interactions entre de multiples participants. Nous proposons un langage de programmation distribué avec sessions, et un compilateur dont l’objet est de générer automatiquement pour chaque session un protocole cryptographique. Ce protocole garantit à un programmeur d’une des parties indépendantes d’un système distribué de ne pas être vulnérable aux actions que le réseau ou d’autres participants corrompus pourraient effectuer pour dévier du comportement prévu par la session.
Le jury sera composé de :
Giuseppe Castagna (président)
Jean-Jacques Levy (directeur)
James J. Leifer (directeur)
Joshua Guttman (rapporteur)
Cosimo Laneve (rapporteur)
Hubert Comon-Lundh
Cédric Fournet
Nobuko Yoshida
Le manuscrit est ici.