A Security Proof Method for Multilevel Security Models

Some variants of BLP model can not prove whether their security policies match multilevel security requirements due to the limitation of security proof method of BLP model. It is pointed out that basic security theorem can only show whether a model match its security properties. So it is necessary to find a new way to formally analyze the improved BLP models instead of using basic security theorem as the original BLP, especially when the security of their improved rules is too complicated to judge directly or when the definition of security properties has been modified, which is considered as the reasoning basics of basic security theorem. In order to accomplish this, a security proof method is developed which takes advantages of a new noninterference model and provides a way to prove the security of multilevel security models from the point of view of information flow. The new noninterference model reclaims the definition of transitive noninterference relationship between system actions, presents a new unwinding theorem, and offers a great help in expressing dynamic policies of multilevel security models. To show practicability of the new noninterference model and the formal method, the security properties of ABLP and DBLP models are examined as examples.