Automated Detection of Information Leakage in Access Control

Anderson Santana de Oliveira 1 Charles Morisset 2
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 SPI - Sémantiques, preuves et implantation
LIP6 - Laboratoire d'Informatique de Paris 6
Abstract : The prevention of information flow is an important concern in several access control models. Even though this property is stated in the model specification, it is not easy to verify it in the actual implementation of a given security policy. In this paper we model-check rewrite-based implementations of access control policies. We propose a general algorithm that allows one to automatically identify information leakage. We apply our approach to the well-known security model of Bell and LaPadula and show that its generalization proposed by McLean does not protect a system against information leakage.
Type de document :
Communication dans un congrès
Monica Nesi. Second International Workshop on Security and Rewriting Techniques - SecReT 2007, Jun 2007, Paris, France. 2007
Liste complète des métadonnées

https://hal.inria.fr/inria-00185713
Contributeur : Anderson Santana de Oliveira <>
Soumis le : mardi 6 novembre 2007 - 18:45:13
Dernière modification le : jeudi 22 novembre 2018 - 14:09:46

Identifiants

  • HAL Id : inria-00185713, version 1

Citation

Anderson Santana de Oliveira, Charles Morisset. Automated Detection of Information Leakage in Access Control. Monica Nesi. Second International Workshop on Security and Rewriting Techniques - SecReT 2007, Jun 2007, Paris, France. 2007. 〈inria-00185713〉

Partager

Métriques

Consultations de la notice

213