LIP6 2003/006
- Rapports de recherche
Formalisation du modèle de sécurité de Bell et La padula - E. Gureghian, Th. Hardin, M. Jaume
- 18 pages - 14/11/2003- document en - http://www.lip6.fr/lip6/reports/2003/lip6.2003.007.pdf - 333 Ko
- Contact : Mathieu.Jaume (at) nulllip6.fr
- Ancien Thème : SPI
- Mots clés : modèle de sécurité, modèle de Bell et La Padula, méthodes formelles
- Directeur de la publication : David.Massot (at) nulllip6.fr
Ce rapport décrit une formalisation complète du modèle de sécurité de Bell et Lapadula dans le système Coq, à partir de laquelle une fonction de transition certifiée a été extraite. Cette fonction permet le contrôle des accès d'un ensemble de sujets sur un ensemble d'objets, en garantissant certaines propriétés de sécurité.