A Security Assurance Framework Combining Formal Verification and Security Functional Testing

Formal specification is usually employed to avoid ambiguity of security requirements. However, it is hard to assure correctness of this formal model and its conformance with security implementation. In this paper, a framework combining formal verification and security functional testing is proposed to support the correctness and conformance check procedure. Formal requirements are verified following integrated steps and formulae. Verified specification is used as the basis for security functional test and a test criterion called strict schema coverage is developed to derive tests. The framework is supported by Z specification Based Security Assurance Toolkit (ZBSAT). Empirical results on Chinese Wall Model (CWM) policy and its implementation demonstrate its feasibility. In addition, comparison results of mutation test explore the efficiency of this test approach.