王瑞云,赵国磊,常朝稳,王雪健.典型安全网关的形式化设计与证明[J].计算机科学,2017,44(9):142-147
典型安全网关的形式化设计与证明
Formal Design and Verification for Typical Security Gateway
投稿时间:2017-04-28  修订日期:2017-06-13
DOI:10.11896/j.issn.1002-137X.2017.09.028
中文关键词:  典型安全网关,形式化设计,BLP模型,功能规约,一致性验证,Isabelle/HOL
英文关键词:Typical security gateway,Formal design,BLP model,Functional specification,Consistency verification,Isabelle/HOL
基金项目:本文受面向用户的可信云计算环境安全研究(61572517)资助
作者单位E-mail
王瑞云 中国人民解放军信息工程大学密码工程学院 郑州450001 wry0068@126.com 
赵国磊 中国人民解放军信息工程大学密码工程学院 郑州450001 glz0371@163.com 
常朝稳 中国人民解放军信息工程大学密码工程学院 郑州450001 ccw@xdja.com 
王雪健 中国人民解放军信息工程大学密码工程学院 郑州450001 1368154434@qq.com 
摘要点击次数: 239
全文下载次数: 138
中文摘要:
      传统上依靠经验设计的安全网关侧重于功能实现,缺少严格的安全模型。对此,针对一种典型安全网关,首先根据其安全需求给出相应的安全策略,然后利用BLP模型对给出的安全策略进行形式化建模并对安全模型的内部一致性进行证明,最后对安全网关的功能规约和安全模型的一致性进行验证。为保证推理过程的正确性,使用定理证明器Isabelle/HOL对上述过程进行描述和推理,保证了安全网关顶层设计的安全性。研究结果为安全网关的形式化设计 提供了一定的借鉴意义。
英文摘要:
      Security gateway which is designed in experience usually focuses on function implementation and is usually not designed according to security model.To solve this problem,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 its top-level design and plays certain referential significance on formal design of security gateway.
查看全文  查看/发表评论  下载PDF阅读器