To: seminaire@pauillac.inria.fr
From: Didier.Remy@inria.fr
Subject: SEM - INRIA : Cristal - 02/02/01 - Paris - FR

      Vous pouvez maintenant vous abonner à nos annonces de séminaires
             http://pauillac.inria.fr/seminaires/subscribe.html


                             S E M I N A I R E
                                         . ___ 
                           /   _   _      /   _   /
                          /   / \ / \  / /   __| /
                         |___ |_/ |_/ / |__ |_/ |_
       ___      .                  /    
      /    ___   __  /_  _   /   _/        /| /|  _   __ __ _       _ 
     /    /   / /_  /   __| /             / |/ | / \ /_ /  / \ | / __|
    |___ /   / __/ |_  |_/ |_            /     | |_/__/ |_ |_/ |/ |_/
                                                
                          I N R I A - Rocquencourt
                       Salle de conference du Bat 11

                         Vendredi 2 fevrier, 10h30

            ----------------------------------------------------
            Francois Pottier, Sylvain Conchon et Vincent Simonet
            ----------------------------------------------------

                             INRIA-Rocquencourt

                  ========================================
                  Inférence de flots d'information pour ML
                  ========================================


L'analyse de flots d'information consiste à étudier les dépendances entre
entrées et sorties d'un programme. Elle permet de garantir des propriétés de
sécurité: si une entrée est considérée comme secrète (ou non fiable), on
souhaitera typiquement que certaines sorties n'en dépendent pas, de façon à
pouvoir les publier (ou les considérer comme fiables).

Contrairement à de nombreuses propriétés de sécurité, l'absence de
dépendance n'est pas une propriété de sûreté. Elle est habituellement
énoncée en termes de `non-interférence': on se donne deux exécutions du
programme à partir de valeurs d'entrée distinctes, et on compare les valeurs
de sortie. Si celles-ci sont distinctes, alors il y a dépendance.

Or, le typage est, le plus souvent, employé pour prouver des propriétés de
sûreté (`well-typed programs do not go wrong'). Le but de l'exposé est de
montrer comment réduire la propriété de non-interférence à une propriété de
sûreté, que l'on peut ensuite établir à l'aide d'un système de types. La
première partie de l'exposé concernera le cas d'un langage fonctionnel pur.
Dans ce cadre simple, François Pottier et Sylvain Conchon ont montré que l'on
peut, à partir d'un système de types classique quasi-arbitraire, dériver
automatiquement le système souhaité. La seconde partie concernera l'extension
à ML, c'est-à-dire l'ajout de références et d'exceptions. Vincent Simonet
montrera que la réduction à une propriété de sûreté reste possible, à
condition de se doter d'un langage cible non standard dans lequel on peut
raisonner sur les `points communs' entre deux exécutions distinctes d'un
programme ML.