计算机科学 ›› 2017, Vol. 44 ›› Issue (9): 142-147.doi: 10.11896/j.issn.1002-137X.2017.09.028
王瑞云,赵国磊,常朝稳,王雪健
WANG Rui-yun, ZHAO Guo-lei, CHANG Chao-wen and WANG Xue-jian
摘要: 传统上依靠经验设计的安全网关侧重于功能实现,缺少严格的安全模型。对此,针对一种典型安全网关,首先根据其安全需求给出相应的安全策略,然后利用BLP模型对给出的安全策略进行形式化建模并对安全模型的内部一致性进行证明,最后对安全网关的功能规约和安全模型的一致性进行验证。为保证推理过程的正确性,使用定理证明器Isabelle/HOL对上述过程进行描述和推理,保证了安全网关顶层设计的安全性。研究结果为安全网关的形式化设计 提供了一定的借鉴意义。
[1] VIAPLANA A R.IpsecVPN[EB/OL].[2017-4-10].http://upcommons.upc.edu/handle/2099.2/2117. [2] PHIFER L.Tunnel Vision:Choosing a VPN-SSL VPN vs IPSec VPN[EB/OL].http:/search security.techtarget.com/feature/Tunel-vision-Choosing-a-VPN-SLL-VPN-vs-IPSec-VPN. [3] WU T,KUANG X H,FU Z L.Analysis and Suggestion of the Heartbleed [J].National Defense Science & Technology,2014,5(5):27-30.(in Chinese) 吴彤,匡兴华,傅中立.“心脏出血”漏洞的特点分析和对策建议[J].国防科技,2014,5(5):27-30. [4] BIEBER P.Formal techniques for an ITSEC-E4 secure gateway[C]∥Computer Security Applications Conference,1996.IEEE,1996:236-245. [5] BELL D E,LAPADULA L J.Secure computer system:mathematical foundation:MTR2527 [R].Belford:Mitrecorp,1973. [6] ABRIAL J R.Modeling in Event-B:System and Software Engineering[M].Cambridge university Press,2010. [7] COMMUNITY E E.Information Technology Security Evaluation Criteria (ITSEC)[R].Commission,1990. [8] 沈晴霓.操作系统安全设计[M].北京:机械工业出版社,2013. [9] BIBA K J.Integrity Considerations for Secure Computing Systems:Mitre Report MTR 3153[R].Belford:Mitrecorp,1975. [10] DENNING D E.A lattice model of secure information flow[J].Communications of the ACM,1976,6(5):236-243. [11] GOGUEN J A,MESEGUER J.Unwinding and Inference Control[C]∥1984 IEEE Symposium on Security and Privacy.IEEE,1984:75. [12] NIPKOW T,PAULSON L C,WENZEL M.Isabelle/HOL:A proof assistant for higher-order logic[M].Springer,2002. [13] CHAPMAN D B,ZWICKY E D.Building Internet firewalls[M]∥O’Reilly & Associates,Inc.,1995. [14] COMER D E.Internetworking with TCP/IP[M].Beijing:Posts & Telecom Press,2002. |
No related articles found! |
|