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 ;
Type de document :
Communication dans un congrès
PLAS 2017 - ACM SIGSAC Workshop on Programming Languages and Analysis for Security, Oct 2017, Dallas, United States. ACM, pp.49-62, PLAS '17 Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security. 〈http://plas2017.cse.buffalo.edu/〉. 〈10.1145/3139337.3139344〉
Liste complète des métadonnées

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

https://hal.archives-ouvertes.fr/hal-01656404
Contributeur : Gurvan Cabon <>
Soumis le : mercredi 20 décembre 2017 - 12:16:26
Dernière modification le : jeudi 12 avril 2018 - 01:54:51
Document(s) archivé(s) le : mercredi 21 mars 2018 - 12:12:33

Fichier

final_version_plas17_cabon_sch...
Accord explicite pour ce dépôt

Identifiants

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, pp.49-62, 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〉

Partager

Métriques

Consultations de la notice

225

Téléchargements de fichiers

82