Skip to Main content Skip to Navigation
Theses

Non Local Analyses Certification With an Annotated Semantics

Gurvan Cabon 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Document type :
Theses
Complete list of metadatas

Cited literature [38 references]  Display  Hide  Download

https://hal.inria.fr/tel-01978292
Contributor : Alan Schmitt <>
Submitted on : Monday, February 25, 2019 - 11:04:52 AM
Last modification on : Friday, July 10, 2020 - 4:02:22 PM
Long-term archiving on: : Sunday, May 26, 2019 - 1:38:03 PM

File

last_final_version.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01978292, version 2

Citation

Gurvan Cabon. Non Local Analyses Certification With an Annotated Semantics. Programming Languages [cs.PL]. Université Rennes 1, 2018. English. ⟨tel-01978292v2⟩

Share

Metrics

Record views

103

Files downloads

238