Comment protéger les données stockées dans un système informatique contre toute modification ou divulgation indésirable tout en permettant l'accès à ces données à tout programme qui en fera une utilisation légitime ? Une solution prometteuse consiste à analyser préalablement chaque programme. Si l'analyse garantit que son comportement sera acceptable, on peut lui accorder un accès sans restriction. Cette technique, appelée analyse de flots d'information, présente l'intérêt de ne reposer sur aucune notion de confiance -- seule la correction de l'analyse importe et peut être prouvée formellement.
Lors de l'exposé, nous présenterons une telle analyse pour le langage Caml. Elle consiste à enrichir le langage de type existant avec des ``niveaux'' permettant de tracer les flots d'information grâce à une forme de sous-typage. Nous nous intéresserons à la fois à des aspects théoriques, liés en particulier à la formalisation du système et à la preuve de sa correction, ainsi qu'à des aspects pratiques liés à son implémentation. Nous présenterons également quelques exemples de code analysés automatiquement par notre prototype, Flow Caml.