發(fā)布時(shí)間：2018-05-16 00:01

  本文選題：典型安全網(wǎng)關(guān) + 形式化設(shè)計(jì)��； 參考：《計(jì)算機(jī)科學(xué)》2017年09期

【摘要】：傳統(tǒng)上依靠經(jīng)驗(yàn)設(shè)計(jì)的安全網(wǎng)關(guān)側(cè)重于功能實(shí)現(xiàn),缺少嚴(yán)格的安全模型。對(duì)此,針對(duì)一種典型安全網(wǎng)關(guān),首先根據(jù)其安全需求給出相應(yīng)的安全策略,然后利用BLP模型對(duì)給出的安全策略進(jìn)行形式化建模并對(duì)安全模型的內(nèi)部一致性進(jìn)行證明,最后對(duì)安全網(wǎng)關(guān)的功能規(guī)約和安全模型的一致性進(jìn)行驗(yàn)證。為保證推理過程的正確性,使用定理證明器Isabelle/HOL對(duì)上述過程進(jìn)行描述和推理,保證了安全網(wǎng)關(guān)頂層設(shè)計(jì)的安全性。研究結(jié)果為安全網(wǎng)關(guān)的形式化設(shè)計(jì)提供了一定的借鑒意義。
[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.
【作者單位】： 中國人民解放軍信息工程大學(xué)密碼工程學(xué)院;
【基金】：面向用戶的可信云計(jì)算環(huán)境安全研究(61572517)資助
【分類號(hào)】：TP309;TP393.05

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 李軍;張潔;蒲海波;;基于安全網(wǎng)關(guān)的電子政務(wù)構(gòu)架模型研究與分析[J];西南民族大學(xué)學(xué)報(bào)(自然科學(xué)版);2007年04期

2 顧劍峰;錢俊;王新剛;柴正一;;數(shù)據(jù)庫信息安全網(wǎng)關(guān)的設(shè)計(jì)與實(shí)現(xiàn)[J];計(jì)算機(jī)安全;2007年11期

3 張超;;SSL VPN客戶端實(shí)現(xiàn)技術(shù)研究[J];電腦知識(shí)與技術(shù);2008年S1期

4 石希;陳震;汪東升;閔二龍;;物聯(lián)網(wǎng)匯聚安全網(wǎng)關(guān)關(guān)鍵技術(shù)研究[J];信息網(wǎng)絡(luò)安全;2012年06期

5 ;Check Point全新推出的安全網(wǎng)關(guān)虛擬版本簡化云安全[J];電子與電腦;2010年10期

6 余勇;林為民;;統(tǒng)一應(yīng)用安全平臺(tái)的設(shè)計(jì)及應(yīng)用[J];信息技術(shù)與標(biāo)準(zhǔn)化;2006年09期

7 王宗斌;;IPSec協(xié)議研究及基于Linux的安全網(wǎng)關(guān)的實(shí)現(xiàn)[J];淮南師范學(xué)院學(xué)報(bào);2007年03期

8 秦寶龍;;淺談利用Linux系統(tǒng)實(shí)現(xiàn)VLAN間的單臂路由及安全網(wǎng)關(guān)的功能[J];計(jì)算機(jī)光盤軟件與應(yīng)用;2014年01期

9 余勇;林為民;;統(tǒng)一應(yīng)用安全平臺(tái)的設(shè)計(jì)及應(yīng)用[J];計(jì)算機(jī)安全;2006年09期

10 張付仁;于洪章;;Linux環(huán)境下基于IPSEC的VPN安全網(wǎng)關(guān)的設(shè)計(jì)[J];福建電腦;2007年02期

相關(guān)會(huì)議論文 前2條

1 曲波;胡n\;;Linux安全網(wǎng)關(guān)接口SGI的設(shè)計(jì)與實(shí)現(xiàn)[A];第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集[C];2005年

2 張?jiān)鲕?肖軍模;;一種數(shù)據(jù)庫安全網(wǎng)關(guān)系統(tǒng)的研究與設(shè)計(jì)[A];第二十一屆中國數(shù)據(jù)庫學(xué)術(shù)會(huì)議論文集（技術(shù)報(bào)告篇）[C];2004年

相關(guān)重要報(bào)紙文章 前5條

1 ;啟明星辰推出一體化安全網(wǎng)關(guān)[N];人民郵電;2007年

2 本報(bào)記者 胡英;安全網(wǎng)關(guān)進(jìn)入百G時(shí)代[N];計(jì)算機(jī)世界;2010年

3 閆冰;業(yè)界熱播應(yīng)用交付網(wǎng)絡(luò)理念[N];網(wǎng)絡(luò)世界;2009年

4 本報(bào)記者 那罡;東軟NetEye集成安全網(wǎng)關(guān)NISG的綠色環(huán)保血統(tǒng)[N];中國計(jì)算機(jī)報(bào);2010年

5 本報(bào)記者 李敬;網(wǎng)御神州 開啟防火墻多核AC時(shí)代[N];計(jì)算機(jī)世界;2009年

相關(guān)碩士學(xué)位論文 前10條

1 宋勁松;病毒及分類網(wǎng)址庫過濾自服務(wù)系統(tǒng)設(shè)計(jì)及實(shí)現(xiàn)[D];中國科學(xué)院大學(xué)(工程管理與信息技術(shù)學(xué)院);2016年

2 唐良;電動(dòng)物流車信息安全網(wǎng)關(guān)的研究與實(shí)現(xiàn)[D];中國科學(xué)技術(shù)大學(xué);2016年

3 楊麗;安全網(wǎng)關(guān)在電力二次系統(tǒng)安全防護(hù)中的應(yīng)用研究[D];華北電力大學(xué)（河北）;2009年

4 董玢;嵌入式Linux安全網(wǎng)關(guān)系統(tǒng)部分功能模塊的設(shè)計(jì)與實(shí)現(xiàn)[D];北京交通大學(xué);2012年

5 李躍;基于IPSec協(xié)議的Linux VPN安全網(wǎng)關(guān)的研究與設(shè)計(jì)[D];蘇州大學(xué);2002年

6 羅秀昌;基于多核網(wǎng)絡(luò)處理器的SSL安全網(wǎng)關(guān)加解密技術(shù)實(shí)現(xiàn)[D];國防科學(xué)技術(shù)大學(xué);2012年

7 姜文;Linux下VPN安全網(wǎng)關(guān)實(shí)現(xiàn)技術(shù)研究[D];浙江大學(xué);2005年

8 吳紅娟;XML Engine安全網(wǎng)關(guān)語義過濾的研究與實(shí)現(xiàn)[D];電子科技大學(xué);2009年

9 郭藝輝;IPSEC在嵌入式系統(tǒng)中的實(shí)現(xiàn)[D];暨南大學(xué);2003年

10 屈浩然;基于Linux的數(shù)據(jù)轉(zhuǎn)發(fā)平臺(tái)的研究與應(yīng)用[D];西北工業(yè)大學(xué);2003年

，

本文編號(hào)：1894519