Formalisation and implementation of Access control models

Access control software must be 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 first present a formalisation of access control models based on the work on an algebra of security models by J.McLean [4]. Then, we describe the implementation of this framework and show how it can be used to obtain a particular security model: the Bell and La Padula security model. Last, as an example, we show how such a program can be integrated for secure databases. All our development is done within the Focal [11] programming environment which provides a language with object-oriented features allowing to write formal specifications, proofs and programs at the same level.

• Type: Conference
• Year: 2005
• Where: ITCC
• Authors: Mathieu Jaume, Charles Morisset
• Keywords: Access Control, Information Technology, ITCC 2005, Policy Model, Security Model