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

https://hal.archives-ouvertes.fr/hal-01656404
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

File

final_version_plas17_cabon_sch...
Explicit agreement for this submission

Identifiers

Citation

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. 〈http://plas2017.cse.buffalo.edu/〉. 〈10.1145/3139337.3139344〉. 〈hal-01656404〉

Share

Metrics

Record views

597

Files downloads

137