Skip to Main content Skip to Navigation
Conference papers

Non-Interference through Annotated Multisemantics

Gurvan Cabon 1 Alan Schmitt 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Non-interference can be dened as a program property that give guaranties on the independence of specic (public) outputs of a program from specic (secret) inputs. The notion of non-interference does not depend on one particular execution of the program (unlike illegal memory access for example), but on its global behavior. To develop a certied system verifying information ows, such as non-interference, we propose to only rely on the execution of the program, and thus investigate such properties using directly the derivation tree of an execution. Considering a single execution is clearly not sucient to determine if a program has the non-interference property. Surprisingly, studying every execution independently is also not sucient. This is why we propose a formal approach that builds, from a given semantics, a multisemantics that allows to reason on several executions at once. Adding annotations in this multisemantics lets us capture the dependencies between inputs and outputs of a program. To motivate and demonstrate our approach, we provide a concrete example where it is clear that reasoning on all the executions at once is required, and we show that our approach works on this example. This is a work in progress, partially formalized in Coq. Ultimately, our goal is to automatically build the multisemantics from the semantics, and to prove that the method correctly approximate non-interference, i.e., if a pair of input and output are independent according to the annotations, then changing the input does not result in a dierent output.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Julien Signoles <>
Submitted on : Thursday, April 6, 2017 - 3:41:04 PM
Last modification on : Monday, March 29, 2021 - 2:41:29 PM
Long-term archiving on: : Friday, July 7, 2017 - 3:24:00 PM


Publisher files allowed on an open archive


  • HAL Id : hal-01503094, version 1


Gurvan Cabon, Alan Schmitt. Non-Interference through Annotated Multisemantics. 28ièmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France. ⟨hal-01503094⟩



Record views


Files downloads