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.
Type de document :
Communication dans un congrès
28ièmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.archives-ouvertes.fr/hal-01503094
Contributeur : Julien Signoles <>
Soumis le : jeudi 6 avril 2017 - 15:41:04
Dernière modification le : lundi 16 octobre 2017 - 11:02:57
Document(s) archivé(s) le : vendredi 7 juillet 2017 - 15:24:00

Fichier

cabon_schmitt.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : hal-01503094, version 1

Collections

Citation

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

Partager

Métriques

Consultations de
la notice

287

Téléchargements du document

54