Precise Dynamic Verification of Noninterference

Abstract : Confidentiality is maybe the most popular security property to be formally or informally verified. Noninterference is a baseline security policy to formalize confidentiality of secret information manipulated by a program. Many static analyses have been developed for the verification of noninterference. In contrast to those static analyses, this paper considers the run-time verification of the respect of confidentiality by a single execution of a program. It proposes a dynamic noninterference analysis for sequential programs based on a combination of dynamic and static analyses. The static analysis is used to analyze some unexecuted pieces of code in order to take into account all types of flows. The static analysis is sensitive to the current program state. This sensitivity allows the overall dynamic analysis to be more precise than previous work. The soundness of the overall dynamic noninterference analysis with regard to confidentiality breaches detection and correction is proved.
Type de document :
Rapport
[Research Report] 2008, pp.40
Liste complète des métadonnées


https://hal.inria.fr/inria-00162609
Contributeur : Gurvan Le Guernic <>
Soumis le : vendredi 18 juillet 2008 - 15:53:13
Dernière modification le : vendredi 16 septembre 2016 - 15:14:57
Document(s) archivé(s) le : samedi 26 novembre 2016 - 00:19:19

Fichier

contextSensitiveNIA.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00162609, version 3

Collections

Citation

Gurvan Le Guernic. Precise Dynamic Verification of Noninterference. [Research Report] 2008, pp.40. <inria-00162609v3>

Partager

Métriques

Consultations de
la notice

136

Téléchargements du document

123