Skip to Main content Skip to Navigation

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 :
Complete list of metadatas

Cited literature [38 references]  Display  Hide  Download
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


Files produced by the author(s)


  • HAL Id : tel-01978292, version 2


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



Record views


Files downloads