典型安全网关的形式化设计与证明

作     者：王瑞云 赵国磊 常朝稳 王雪健 WANG Rui-yun;ZHAO Guo-lei;CHANG Chao-wen;WANG Xue-jian

作者机构：中国人民解放军信息工程大学密码工程学院郑州450001 

基　　金：面向用户的可信云计算环境安全研究(61572517)资助 

出 版 物：《计算机科学》 (Computer Science)

年 卷 期：2017年第44卷第9期

页      码：142-147页

摘      要：传统上依靠经验设计的安全网关侧重于功能实现,缺少严格的安全模型。对此,针对一种典型安全网关,首先根据其安全需求给出相应的安全策略,然后利用BLP模型对给出的安全策略进行形式化建模并对安全模型的内部一致性进行证明,最后对安全网关的功能规约和安全模型的一致性进行验证。为保证推理过程的正确性,使用定理证明器Isabelle/HOL对上述过程进行描述和推理,保证了安全网关顶层设计的安全性。研究结果为安全网关的形式化设计提供了一定的借鉴意义。

主 题 词：典型安全网关 形式化设计 BLP模型 功能规约 一致性验证 Isabelle/HOL 

学科分类：08[工学] 0839[0839] 081201[081201] 0812[工学-测绘类] 

D　O　I：10.11896/j.issn.1002-137X.2017.09.028

馆 藏 号：203262219...