Skip to Main content Skip to Navigation
New interface
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Frédéric Besson Connect in order to contact the contributor
Submitted on : Monday, May 2, 2016 - 6:17:56 PM
Last modification on : Monday, July 25, 2022 - 3:28:02 AM
Long-term archiving on: : Tuesday, May 24, 2016 - 5:57:24 PM


Files produced by the author(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⟩



Record views


Files downloads