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