Research on formal security policy model specification and its formal analysis

Abstract

Formal method is one of the kernel technologies of developing high security level computer system.But by current formal development method,assurance of security policy model correctness cannot be provided directly using machine proof which is stricter than manual proof,correspondence between security policy model and security functional specification is also hard to achieve.To solve these problems,a new and effective method was proposed for specification constructing and proving by extending the specification technique of security functional specification into the specifica-tion of security policy model.Also,BLP model was specified and analyzed as an example.

Keywords

• security policy model
• formal specification
• formal analysis
• theorem prove
• Bell-LaPadula model