The specification and modeling of computer security

A description is given of computer security models in general and the model of D. Bell and L. LaPadula (Tech. Rep. MTR-2997, Mitre Corp., 1976) in particular. The Bell and LaPadula (BLP) model is the backbone of the National Computer Security Center´s evaluation process for trusted computer systems. Although discretionary access control is briefly addressed, the focus is on mandatory access control (MAC) in national security. However, the issues addressed are relevant to any setting in which MAC-like restrictions arise. It is shown that security is a fruitful research area for those interested in software specification, since some of the most difficult issues in specifying security have analogs in other domains. The limitations of the BLP model are examined. For example, it has little relevance for systems in which users can change their own security levels or those of their files, and it is inadequate for expressing requirements that certain operations cannot be performed by a single individual working alone. It is shown how BLP´s limitations can be remedied by a framework of models, making it more useful to those interested in industrial security.<>