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 metadatas

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 : Friday, September 13, 2019 - 9:48:42 AM
Long-term archiving on : 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. ⟨10.1145/3139337.3139344⟩. ⟨hal-01656404⟩

Share

Metrics

Record views

694

Files downloads

211