Vous êtes ici

Certification d’Analyses Non Locales avec une Sémantique Annotée

Vous êtes cordialement invités à venir assister à la soutenance de thèse de Gurvan Cabon (équipe Celtique) qui se tiendra le vendredi 14 décembre à 14h30 en salle Michel Métivier ainsi qu'au pot qui suivra en salle Sein.

Titre: Certification d’Analyses Non Locales avec une Sémantique Annotée


Résumé:

La quantité croissante de données traitées par les logiciels rend légitime le besoin de garanties de confidentialité.
La propriété de non-interférence assure qu'un programme ne fuite pas de données privées vers une sortie publique.

Nous proposons une méthode pour construire une multisémantique annotée capable de capturer la propriété de non-interférence pour aider à prouver formellement des analyseurs.
Nous fournissons un théorème prouvé indiquant que les annotations capturent correctement la non-interférence.

Le théorème de correction permet de prouver un analyseur sans s'appuyer sur la définition de non-interférence mais sur les annotations.

Orateur: 
Gurvan Cabon (CELTIQUE)
Date: 
Vendredi, 14. décembre 2018 - 14:30 - 18:00
Lieu: 
IRISA Rennes - Salle Michel Métivier
Type soutenance: 
Composition du Jury: 
  • Tamara REZK, Chargée de recherche INRIA Sophia Antipolis-Méditerranée
  • Daniel HIRSCHKOFF, Maître de conférences LIP Lyon
  • Sophie PINCHINAT, Professeure Université de Rennes 1
  • Arthur CHARGUERAUD, Chargé de recherche Inria Nancy Grand Est
  • Sylvain CONCHON, Professeur Université Paris-Sud
  • Alan SCHMITT, Directeur de recherche INRIA Rennes Bretagne Atlantique