Bell-LaPadula model

A formal, mathematical, state-transition model of confidentiality policy for multilevel-secure computer systems [Bell]. (Compare: Biba model, Brewer-Nash model.)

Tutorial: The model, devised by David Bell and Leonard LaPadula at The MITRE Corporation in 1973, characterizes computer system elements as subjects and objects. To determine whether or not a subject is authorized for a particular access mode on an object, the clearance of the subject is compared to the classification of the object. The model defines the notion of a "secure state", in which the only permitted access modes of subjects to objects are in accordance with a specified security policy. It is proven that each state transition preserves security by moving from secure state to secure state, thereby proving that the system is secure. In this model, a multilevel-secure system satisfies several rules, including the "confinement property" (a.k.a. the "*-property"), the "simple security property", and the "tranquility property".