Université de Rennes 1 Non local analyses certification with an annotated semantics Certification d'analyse non locale grâce à une sémantique annotée mutlisémantique annotéenon-interférenceméthodes formelles annotated multisemanticsnon-interferenceformal method Analyse des données -- LogicielsThèses et écrits académiques 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. 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. Electronic Thesis or DissertationText en application/pdf1 : 828 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/88e7baf6-ceba-4d2c-8b20-17ddeac8a56a Cabon Gurvan 1991-02-02 FR 235389862 gurvan.cabon@hotmail.fr 2018REN1S078 http://www.theses.fr/2018REN1S078 2018-12-14 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiSchmittAlanintervenant_1135454840 MATHSTICecoleDoctorale_1 204770424 Universite Bretagne LoirepartenaireRecherche_1 191639044 INRIA-RENNES partenaireRecherche_2 133175863 ddc:004 SchmittAlanUniversite de Rennes 1Sciences et technologie, medecine, pharmacie, odontologie, droit, economie, gestion, philosophieMATHSTICÉcole doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes)Universite Bretagne Loire Communaute des etablissements d enseignement superieur et de recherche (ComuE) INRIA-RENNES ASCII PDF 848276