Non local analyses certification with an annotated semantics (Certification d'analyse non locale grâce à une sémantique annotée) Cabon, Gurvan - (2018-12-14) / Universite de Rennes 1 Non local analyses certification with an annotated semantics Accéder au document :  https://ged.univ-rennes1.fr/nuxeo/site/esupversion...

Langue : Anglais Directeur(s) de thèse:  Schmitt, Alan Discipline : Informatique Laboratoire :  INRIA-RENNES Ecole Doctorale : MATHSTIC Classification : Informatique Mots-clés : mutlisémantique annotée, non-interférence, méthodes formelles Analyse des données -- Logiciels  - Thèses et écrits académiques

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. Abstract : Because of the increasing quantity of data processed by software, the need for privacy guarantees is legitimate. The property of non-interference ensures that a program does not leak private data to a public output. We propose a framework to build an annotated multisemantics able to capture the non-interference property to help formally prove analysers. The framework comes with a proved theorem stating that the annotations correctly capture non-interference. The correctness theorem allows to prove an analyser without relying on the definition of non-interference but on the annotations.