The Bell-LaPadula Model Reexamined
Ninghui Li,
Purdue University
4pm Wed, 2 March, 2005
SC 3405
The Bell-LaPadula model (BLP) is among the most fundamental works in
computer security and is taught to almost everyone who studies
computer security. BLP aims at providing a way to prove that a
computer system is free of illegal information flow through
reading/writing objects (i.e., overt rather than covert channels). Bell
and LaPadula use an abstract state machine to model computer systems and
define a system to be secure if every reachable state satisfies three
security properties. They then prove a Basic Security Theorem that
intends to show that determining whether a system is secure or not can
be done by analyzing the description of a system without running the
system.
We argue that the the BLP notion of security is neither necessary nor
sufficient to achieve its objective of stopping overt illegal
information flow channels. We argue that the state-based approach of
defining security in BLP is fundamentally flawed and discuss how to
remedy this problem by clearly separating policy objectives and
enforcement mechanisms. We also show that the Basic Security Theorem
fails to achieve its objective of providing a necessary and sufficient
condition for proving a system is BLP-secure.