47 / 2017-05-18 20:18:45

Formal Design and Verification for a Typical Security Gateway

Typical security gateway, Formal design, BLP model, Functional specification, Consistency verification, Isabelle/HOL

Using formal methods to analyze and verify the security model and functional specifications of information security products is the first step to ensure their realization security. To ensure the security of the top-level design for security gateway, we proposed a method to formally design and verify a typical security gateway. Firstly, we designed the typical security gateway’s security policy according to its security requirements. Secondly, we formally modeled the security policy and verified the security model’s internal consistency by means of BLP model. In the end, we verified the consistency between the security gateway’s functional specifications and its security model. To make sure the reasoning procedure’s correctness, we used the theorem prover Isabelle/HOL to formally describe the above work and help us deduce. Our work ensures the security of a typical security gateway in terms of its top-level design and plays certain referential significance on formal design of security gateway.