Evènement pour le groupe Modélisation et Verification


Date 2009-04-02  11:00-12:15
TitreExtrapol, des systèmes de types dépendants à la sécurité système 
RésuméDans le domaine de la sécurité, l'un des problèmes récurrents est celui de déterminer quels effets l'exécution d'un programme peut avoir sur le système qui l'héberge. Ces effets peuvent prendre la forme de modification de fichiers, de communication avec des processus, d'installation de services web... Dans d'autres cas, c'est l'installation d'un programme ou d'une bibliothèque qui pourra donner à d'autres programmes des points d'entrée pour avoir ce même genre d'effets, de manière potentiellement accidentelle et potentiellement malicieuse. Le plus fréquemment, pour détecter les effets d'un programme ou les points d'entrée d'une bibliothèque, l'administrateur d'un système a le choix entre des outils dynamiques (bacs à sable) et des outils post-mortem (analyse de trace) -- mais pas réellement d'outils d'analyse statique. Au cours de notre exposé, nous présenterons une technique d'analyse statique pour les propriétés de sécurité de code source écrit en langage C. Nous partirons du modèle de sécurité SELinux, tel qu'intégré à de nombreuses distributions de Linux, et nous avancerons progressivement jusqu'à une notion de types avec effets et de types dépendants. La technique a été implantée en OCaml, sous la forme d'un outil de diagnostic automatique, Extrapol. 
Lieu 
OrateurDavid Teller-Rajchenbach 
EmailDavid.Teller@univ-orleans.fr 
Urluniversité d'Orléans 



Aucun document lié à cet événement.

Retour
Retour à l'index