| 典型安全网关的形式化设计与证明 |
| |
| 引用本文： | 王瑞云,赵国磊,常朝稳,王雪健. 典型安全网关的形式化设计与证明[J]. 计算机科学, 2017, 44(9): 142-147 |
| |
| 作者姓名： | 王瑞云 赵国磊 常朝稳 王雪健 |
| |
| 作者单位： | 中国人民解放军信息工程大学密码工程学院 郑州450001,中国人民解放军信息工程大学密码工程学院 郑州450001,中国人民解放军信息工程大学密码工程学院 郑州450001,中国人民解放军信息工程大学密码工程学院 郑州450001 |
| |
| 基金项目： | 本文受面向用户的可信云计算环境安全研究(61572517)资助 |
| |
| 摘 要： | 传统上依靠经验设计的安全网关侧重于功能实现,缺少严格的安全模型。对此,针对一种典型安全网关,首先根据其安全需求给出相应的安全策略,然后利用BLP模型对给出的安全策略进行形式化建模并对安全模型的内部一致性进行证明,最后对安全网关的功能规约和安全模型的一致性进行验证。为保证推理过程的正确性,使用定理证明器Isabelle/HOL对上述过程进行描述和推理,保证了安全网关顶层设计的安全性。研究结果为安全网关的形式化设计 提供了一定的借鉴意义。
|
| 关 键 词： | 典型安全网关 形式化设计 BLP模型 功能规约 一致性验证 Isabelle/HOL |
| 收稿时间： | 2017-04-28 |
| 修稿时间： | 2017-06-13 |
Formal Design and Verification for Typical Security Gateway |
| |
| WANG Rui-yun,ZHAO Guo-lei,CHANG Chao-wen and WANG Xue-jian. Formal Design and Verification for Typical Security Gateway[J]. Computer Science, 2017, 44(9): 142-147 |
| |
| Authors: | WANG Rui-yun ZHAO Guo-lei CHANG Chao-wen WANG Xue-jian |
| |
| Affiliation: | Department of Password Engineering,The PLA Information Engineering University,Zhengzhou 450001,China,Department of Password Engineering,The PLA Information Engineering University,Zhengzhou 450001,China,Department of Password Engineering,The PLA Information Engineering University,Zhengzhou 450001,China and Department of Password Engineering,The PLA Information Engineering University,Zhengzhou 450001,China |
| |
| Abstract: | |
| |
| Keywords: | Typical security gateway Formal design BLP model Functional specification Consistency verification Isabelle/HOL |
|
|
点击此处可从《计算机科学》下载全文 |
|
