Vendredi 27 septembre 2002
Contact: Jean Goubault-Larrecq
La vérification de propriétés de sécurité est devenue un thème porteur ces dernières années. On pense ici notamment à la vérification de protocoles cryptographiques, et aux diverses propriétés de sécurité afférentes: secret, authentication, non-duplication, fraîcheur, non-répudiation, anonymat, quant-à-soi, etc. On pense parfois moins au fait que, même si les protocoles sont corrects (ce qu'ils sont rarement), les implémentations le sont parfois moins.
Dans le but d'évaluer les propriétés de sécurité de code, et non simplement de protocoles, des méthodes automatiques sont nécessaires, fondées sur le typage, l'interprétation abstraite, notamment.
Dans ce cadre, c'est toute une hiérarchie de propriétés qu'il
s'agit de vérifier, depuis la non-corruption de la mémoire jusqu'à
la vérification de politiques de sécurité (comme celles définies
par les security profiles du JDK 2 de l'architecture Java
de Sun), en passant par les propriétés de non-interférence.
But de la journée
Le but de la journée est d'offrir aux chercheurs et aux étudiants l'occasion de se regrouper afin de croiser leurs expériences et leurs compétences, de connaître l'état de l'art et de découvrir les nouvelles applications, et de reconnaître les axes de recherches futurs concernant la vérification de propriétés de sécurité sur du code, et sur l'architecture Java en particulier.
Accessoirement, il s'agit d'une série d'exposés de la part des membres du jury de la thèse d'Eva Rose, qui soutiendra sa thèse en fin de journée, sur le thème:
Le programme de la journée sera composé des exposés suivants (version préliminaire):
Il n'y a pas de frais d'inscription. Tout le monde est le bienvenu, dans la limite des places disponibles, et à condition de s'inscrire au préalable en m'envoyant un mail. Contrairement à la salle initialement prévue, la salle Condorcet est grande. Il y aura donc de la place pour tous!