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

发布时间：2018-05-16 00:01

  本文选题：典型安全网关 + 形式化设计　； 参考：《计算机科学》2017年09期

【摘要】：传统上依靠经验设计的安全网关侧重于功能实现,缺少严格的安全模型。对此,针对一种典型安全网关,首先根据其安全需求给出相应的安全策略,然后利用BLP模型对给出的安全策略进行形式化建模并对安全模型的内部一致性进行证明,最后对安全网关的功能规约和安全模型的一致性进行验证。为保证推理过程的正确性,使用定理证明器Isabelle/HOL对上述过程进行描述和推理,保证了安全网关顶层设计的安全性。研究结果为安全网关的形式化设计提供了一定的借鉴意义。
[Abstract]:Traditionally, the security gateway, which is designed by experience, focuses on function realization and lacks strict security model. Aiming at a typical security gateway, the corresponding security policy is first given according to its security requirements, and then the security policy is formalized by using BLP model and the internal consistency of the security model is proved. Finally, the consistency of the function specification and the security model of the security gateway is verified. In order to ensure the correctness of the reasoning process, the theorem prover Isabelle/HOL is used to describe and infer the above process, which ensures the security of the top-level design of the security gateway. The results provide some reference for the formal design of security gateway.
【作者单位】： 中国人民解放军信息工程大学密码工程学院;
【基金】：面向用户的可信云计算环境安全研究(61572517)资助
【分类号】：TP309;TP393.05

【相似文献】

相关期刊论文 前10条

1 李军;张洁;蒲海波;;基于安全网关的电子政务构架模型研究与分析[J];西南民族大学学报(自然科学版);2007年04期

2 顾剑峰;钱俊;王新刚;柴正一;;数据库信息安全网关的设计与实现[J];计算机安全;2007年11期

3 张超;;SSL VPN客户端实现技术研究[J];电脑知识与技术;2008年S1期

4 石希;陈震;汪东升;闵二龙;;物联网汇聚安全网关关键技术研究[J];信息网络安全;2012年06期

5 ;Check Point全新推出的安全网关虚拟版本简化云安全[J];电子与电脑;2010年10期

6 余勇;林为民;;统一应用安全平台的设计及应用[J];信息技术与标准化;2006年09期

7 王宗斌;;IPSec协议研究及基于Linux的安全网关的实现[J];淮南师范学院学报;2007年03期

8 秦宝龙;;浅谈利用Linux系统实现VLAN间的单臂路由及安全网关的功能[J];计算机光盘软件与应用;2014年01期

9 余勇;林为民;;统一应用安全平台的设计及应用[J];计算机安全;2006年09期

10 张付仁;于洪章;;Linux环境下基于IPSEC的VPN安全网关的设计[J];福建电脑;2007年02期

相关会议论文 前2条

1 曲波;胡n\;;Linux安全网关接口SGI的设计与实现[A];第二十次全国计算机安全学术交流会论文集[C];2005年

2 张增军;肖军模;;一种数据库安全网关系统的研究与设计[A];第二十一届中国数据库学术会议论文集（技术报告篇）[C];2004年

相关重要报纸文章 前5条

1 ;启明星辰推出一体化安全网关[N];人民邮电;2007年

2 本报记者 胡英;安全网关进入百G时代[N];计算机世界;2010年

3 闫冰;业界热播应用交付网络理念[N];网络世界;2009年

4 本报记者 那罡;东软NetEye集成安全网关NISG的绿色环保血统[N];中国计算机报;2010年

5 本报记者 李敬;网御神州 开启防火墙多核AC时代[N];计算机世界;2009年

相关硕士学位论文 前10条

1 宋劲松;病毒及分类网址库过滤自服务系统设计及实现[D];中国科学院大学(工程管理与信息技术学院);2016年

2 唐良;电动物流车信息安全网关的研究与实现[D];中国科学技术大学;2016年

3 杨丽;安全网关在电力二次系统安全防护中的应用研究[D];华北电力大学（河北）;2009年

4 董玢;嵌入式Linux安全网关系统部分功能模块的设计与实现[D];北京交通大学;2012年

5 李跃;基于IPSec协议的Linux VPN安全网关的研究与设计[D];苏州大学;2002年

6 罗秀昌;基于多核网络处理器的SSL安全网关加解密技术实现[D];国防科学技术大学;2012年

7 姜文;Linux下VPN安全网关实现技术研究[D];浙江大学;2005年

8 吴红娟;XML Engine安全网关语义过滤的研究与实现[D];电子科技大学;2009年

9 郭艺辉;IPSEC在嵌入式系统中的实现[D];暨南大学;2003年

10 屈浩然;基于Linux的数据转发平台的研究与应用[D];西北工业大学;2003年

，

本文编号：1894519