Hybrid Monitoring of Attacker Knowledge

Frédéric Besson 1 Nataliia Bielova 2 Thomas Jensen 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 INDES - Secure Diffuse Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Enforcement of noninterference requires proving that an attacker's knowledge about the initial state remains the same after observing a program's public output. We propose a hybrid monitoring mechanism which dynamically evaluates the knowledge that is contained in program variables. To get a precise estimate of the knowledge, the monitor statically analyses non-executed branches. We show that our knowledge-based monitor can be combined with existing dynamic monitors for non-interference. A distinguishing feature of such a combination is that the combined monitor is provably more permissive than each mechanism taken separately. We demonstrate this by proposing a knowledge-enhanced version of a no-sensitive-upgrade (NSU) monitor. The monitor and its static analysis have been formalized and proved correct within the Coq proof assistant.
Type de document :
Communication dans un congrès
29th IEEE Computer Security Foundations Symposium, 2016, Lisboa, Portugal
Liste complète des métadonnées

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

Contributeur : Frédéric Besson <>
Soumis le : lundi 2 mai 2016 - 18:17:56
Dernière modification le : jeudi 7 février 2019 - 15:25:32
Document(s) archivé(s) le : mardi 24 mai 2016 - 17:57:24


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01310572, version 1


Frédéric Besson, Nataliia Bielova, Thomas Jensen. Hybrid Monitoring of Attacker Knowledge. 29th IEEE Computer Security Foundations Symposium, 2016, Lisboa, Portugal. 〈hal-01310572〉



Consultations de la notice


Téléchargements de fichiers