Formal modeling in a generalized framework for access control

The author reports preliminary results of formal modeling for computer security guided by the generalized framework for access control developed in the MITRE research project known as unified access control. This formal modeling approach differs from the traditional Bell-La Padula model in the way it defines and uses access control rules. This approach has one key new element compared to traditional approaches: the rules for access control are an entity that is separate from, although necessarily related to, the model of the TCB (trusted computing base) interface. This new approach allows greater flexibility in choosing and specifying security policies for a secure system