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 : Friday, January 11, 2019 - 1:57:37 PM
Last modification on : Friday, September 13, 2019 - 9:48:42 AM
Long-term archiving on : Friday, April 12, 2019 - 3:52:54 PM


Files produced by the author(s)


  • HAL Id : tel-01978292, version 1


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



Record views


Files downloads