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
Liste complète des métadonnées

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01310572
Contributor : Frédéric Besson <>
Submitted on : Monday, May 2, 2016 - 6:17:56 PM
Last modification on : Thursday, February 7, 2019 - 3:25:32 PM
Document(s) archivé(s) le : Tuesday, May 24, 2016 - 5:57:24 PM

Files

hybrid_monitoring_of_attacker_...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01310572, version 1

Citation

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

Share

Metrics

Record views

2135

Files downloads

133