Annotated multisemantics to prove Non-Interference analyses

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 : The way information flows into programs can be difficult to track. As non-interference is a hyperproperty relating the results of several executions of a program, showing the correctness of an analysis is quite complex. We present a framework to simplify the certification of the correction proof of such analyses. The key is capturing the non-interference property through an annotated semantics based on the execution of the program and not simply its result. The approach is illustrated using a small While language. CCS CONCEPTS • Security and privacy → Formal methods and theory of security ;
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [18 references]  Display  Hide  Download
Contributor : Gurvan Cabon <>
Submitted on : Wednesday, December 20, 2017 - 12:16:26 PM
Last modification on : Wednesday, February 20, 2019 - 2:32:01 PM
Document(s) archivé(s) le : Wednesday, March 21, 2018 - 12:12:33 PM


Explicit agreement for this submission



Gurvan Cabon, Alan Schmitt. Annotated multisemantics to prove Non-Interference analyses. PLAS 2017 - ACM SIGSAC Workshop on Programming Languages and Analysis for Security, Oct 2017, Dallas, United States. ACM, PLAS '17 Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security. 〈〉. 〈10.1145/3139337.3139344〉. 〈hal-01656404〉



Record views


Files downloads