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 metadatas

Cited literature [13 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01503094
Contributor : Julien Signoles <>
Submitted on : Thursday, April 6, 2017 - 3:41:04 PM
Last modification on : Friday, September 13, 2019 - 9:48:42 AM
Long-term archiving on : Friday, July 7, 2017 - 3:24:00 PM

File

cabon_schmitt.pdf
Publisher files allowed on an open archive

Identifiers

  • HAL Id : hal-01503094, version 1

Citation

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

Share

Metrics

Record views

1076

Files downloads

116