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, 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 [18 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 : mercredi 21 novembre 2018 - 09:08:54
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, 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

517

Téléchargements de fichiers

122