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
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é.
• 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