|
Evènement pour le groupe Modélisation et Verification
Date | 2009-04-02 11:00-12:15 |
Titre | Extrapol, 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 | |
Orateur | David Teller-Rajchenbach |
Email | David.Teller@univ-orleans.fr |
Url | université d'Orléans |
Aucun document lié à cet événement. RetourRetour à l'index
| |