The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
De nos jours, les technologies les plus avancées disponibles pour
garantir la sûreté d'un système Linux vis-à-vis de processus malicieux
ou bogués sont SELinux, AppArmor et quelques autres techniques
comparables de pare-feux internes. Dans chacun des cas, l'approche
consiste à surveiller dynamiquement les interactions entre processus ou
entre processus et objets du système et à interdire celles qui ne sont
pas explicitement autorisées par une "politique de sécurité". Si l'idée
est intéressante, son implantation se révèle souvent trop complexe pour
la mise en oeuvre, notamment en raison de la difficulté à valider une
nouvelle politique de sécurité sans devoir tester exhaustivement tous
les logiciels installés.
C'est à ce point qu'entre en jeu l'analyse statique : comment, à partir
d'une politique de sécurité, vérifier statiquement la compatibilité avec
les logiciels déjà installés sur le système, ou avec de nouveaux
logiciels à installer ? C'est sur ce problème que nous travaillons dans
le cadre d'Extrapol : à partir du modèle de sécurité imposé par SELinux,
des systèmes de types à la Hindley-Milner et des types dépendants, nous
définissons un mécanisme d'extraction de politiques de sécurité à partir
de bibliothèques et de fonctions écrites en langage C.
Au cours de cet exposé, nous présenterons le modèle de sécurité de
SELinux, la transformation de ce modèle en un jeu de contraintes sur le
langage C et le processus d'extraction.