L'analyse de flots d'information consiste à déterminer si un programme
satisfait certaines propriétés de confidentialité ou d'intégrité
vis-à-vis des données qu'il manipule, en analysant les dépendances
entre ses entrées et ses sorties : par exemple, si une entrée est
considérée secrète, on souhaitera généralement que des
sorties publiques n'en dépendent pas. Une solution naturelle
consiste à effectuer cette analyse à l'aide d'un système de types
annotés par des niveaux d'information, afin de pouvoir s'assurer du
bon comportement d'un programme avant son exécution.
Lors de l'exposé, nous nous intéresserons au développement d'un telle
analyse par typage statique pour le langage Caml.
Nous présenterons tout d'abord sa formalisation, ainsi que la preuve
de sa correction, sur le noyau du langage, Core ML (c'est-à-dire un
lambda-calcul doté d'un let polymorphe, de références, d'exceptions
et de primitives). Il s'agit d'un système de types à la ML avec
contraintes et doté de sous-typage. Sa correction, exprimée par un
énoncé de non-interférence, est ramenée à la preuve d'une propriété
de subject-reduction pour un langage non standard dans lequel on
peut raisonner sur les points communs entre deux exécutions distinctes
d'un programme.