• Home
  • Page : 'rapport_recherche' inconnue (menus.php)

LIP6 2003/006

  • Reports
    Formalisation du modèle de sécurité de Bell et La padula
  • E. Gureghian, Th. Hardin, M. Jaume
  • 18 pages - 11/14/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
  • Information access control programs are based on a security policy model. Flaws in them may come from a lack of precision or some incoherences in the policy model or from inconsistencies between the model and the code. In this paper, we build a full mechanized formalization of the well-known Bell and LaPadula policy model, checking all the steps of the proofs. Then, we derive automatically a program for the access controls considered in this model. Such a program implements a transition function which has been formally proved sound according to the three security properties involved in the Bell and La Padula model. All the work is done within Coq, a theorem prover based on a very strong type theory.
  • Keywords : security policy, Belle and Lapadula model, formal methods
  • Publisher : David.Massot (at) nulllip6.fr
Mentions légales
Site map