PoS - Proceedings of Science
Volume 299 - The 7th International Conference on Computer Engineering and Networks (CENet2017) - Session IV - Cloud Science
Formal Design and Verification for A Typical Security Gateway
R. Wang*, G. Zhao, C. Chang and X. Wang
Full text: pdf
Pre-published on: July 17, 2017
Published on: September 06, 2017
Abstract
To ensure the security of the top-level design of the security gateway, we proposed a method of formally designing and verifying 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 top-level design and exerts certain referential significance on formal design of security gateway.
DOI: https://doi.org/10.22323/1.299.0076
How to cite

Metadata are provided both in "article" format (very similar to INSPIRE) as this helps creating very compact bibliographies which can be beneficial to authors and readers, and in "proceeding" format which is more detailed and complete.

Open Access
Creative Commons LicenseCopyright owned by the author(s) under the term of the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.