Skip to Main content Skip to Navigation
Conference papers

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
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Gurvan Cabon <>
Submitted on : Wednesday, December 20, 2017 - 12:16:26 PM
Last modification on : Monday, March 29, 2021 - 2:41:29 PM
Long-term archiving on: : 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. ⟨10.1145/3139337.3139344⟩. ⟨hal-01656404⟩



Record views


Files downloads