本文關(guān)鍵詞：數(shù)據(jù)庫(kù)管理系統(tǒng)強(qiáng)制訪問(wèn)控制形式化分析與明證

  更多相關(guān)文章： 強(qiáng)制訪問(wèn)控制 形式化驗(yàn)證 信息流 定理證明器Coq

【摘要】：強(qiáng)制訪問(wèn)控制是保護(hù)數(shù)據(jù)庫(kù)管理系統(tǒng)安全的有效機(jī)制.DMOSMAC是一個(gè)依賴于安全操作系統(tǒng)實(shí)現(xiàn)強(qiáng)制訪問(wèn)控制機(jī)制的數(shù)據(jù)庫(kù)管理系統(tǒng).在分析該系統(tǒng)實(shí)現(xiàn)的基礎(chǔ)上,對(duì)該系統(tǒng)進(jìn)行了形式化分析.給出了信息流的概念,將信息流集合作為被驗(yàn)證系統(tǒng)狀態(tài)的一部分.信息流集合始終是一個(gè)遞增的集合,利用信息集合流可防止刪除等操作的證明被繞過(guò)的可能,保證驗(yàn)證過(guò)程的嚴(yán)密性.在信息流的基礎(chǔ)上提出了一種對(duì)系統(tǒng)代碼進(jìn)行抽象、抽取的形式化分析方法.即抽象DMOSMAC系統(tǒng)狀態(tài),從源代碼中提取操作規(guī)則,將BLP模型中的狀態(tài)、訪問(wèn)規(guī)則分別與DMOSMAC系統(tǒng)的狀態(tài)、操作規(guī)則建立映射關(guān)系,BLP模型中簡(jiǎn)單安全性和*-特性轉(zhuǎn)換為面向信息流的狀態(tài)不變式,繼承BLP模型的相關(guān)安全公理和定理進(jìn)行分析和證明;最后用定理證明器COQ進(jìn)行安全性證明的方法.
【作者單位】： 華中科技大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院;
【關(guān)鍵詞】： 強(qiáng)制訪問(wèn)控制 形式化驗(yàn)證 信息流 定理證明器Coq
【基金】：國(guó)家核高基重大專項(xiàng)(2010ZX01042-001-003-03)資助
【分類號(hào)】：TP311.13;TP393.08
【正文快照】： 1引言數(shù)據(jù)庫(kù)管理系統(tǒng)已經(jīng)廣泛應(yīng)用于軍事、政務(wù)、醫(yī)療、金融等重要行業(yè)中.這些系統(tǒng)中保存了大量的敏感數(shù)據(jù),成為最吸引攻擊者的目標(biāo).研究高安全等級(jí)的數(shù)據(jù)庫(kù)管理系統(tǒng)關(guān)鍵技術(shù),對(duì)于提高數(shù)據(jù)庫(kù)管理系統(tǒng)的安全性具有重要的意義.為了設(shè)計(jì)并實(shí)現(xiàn)達(dá)到國(guó)標(biāo)5級(jí)[1]甚至是TCSEC的A級(jí)數(shù)據(jù)

【參考文獻(xiàn)】

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前1條

1 史建琦;面向目標(biāo)代碼的實(shí)時(shí)操作系統(tǒng)形式化驗(yàn)證方法研究[D];華東師范大學(xué);2012年

【共引文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前10條

1 宋言偉;馬欽德;張健;;信息安全等級(jí)保護(hù)政策和標(biāo)準(zhǔn)體系綜述[J];信息通信技術(shù);2010年06期

2 池仁隆;張超;張春柳;;信息系統(tǒng)安全等級(jí)保護(hù)建設(shè)與測(cè)評(píng)方法簡(jiǎn)析[J];軟件產(chǎn)業(yè)與工程;2012年02期

3 石文昌,孫玉芳;多級(jí)安全性政策的歷史敏感性[J];軟件學(xué)報(bào);2003年01期

4 卿斯?jié)h,朱繼鋒;安勝安全操作系統(tǒng)的隱蔽通道分析[J];軟件學(xué)報(bào);2004年09期

5 王永吉;吳敬征;曾海濤;丁麗萍;廖曉鋒;;隱蔽信道研究[J];軟件學(xué)報(bào);2010年09期

6 袁杰;吳曉剛;;四川省企業(yè)自備電廠在線監(jiān)測(cè)系統(tǒng)設(shè)計(jì)概要[J];四川電力技術(shù);2011年02期

7 李小滿,蔣建春,卿斯?jié)h;面向?qū)ο蟮陌踩u(píng)估方法[J];計(jì)算機(jī)工程與設(shè)計(jì);2005年01期

8 王明根;一個(gè)Oracle數(shù)據(jù)庫(kù)安全增強(qiáng)器的實(shí)現(xiàn)[J];計(jì)算機(jī)工程與設(shè)計(jì);2005年06期

9 王春元;楊善林;周永務(wù);;信息安全等級(jí)測(cè)評(píng)系統(tǒng)設(shè)計(jì)[J];計(jì)算機(jī)工程與設(shè)計(jì);2006年23期

10 潘學(xué)儉;袁春陽(yáng);梁洪亮;呂洪利;;FreeBSD中內(nèi)核級(jí)安全審計(jì)系統(tǒng)的構(gòu)建[J];計(jì)算機(jī)工程與設(shè)計(jì);2007年05期

中國(guó)重要會(huì)議論文全文數(shù)據(jù)庫(kù) 前10條

1 李梅娟;蔡勉;常偉華;賈佳;;操作系統(tǒng)安全等級(jí)測(cè)評(píng)技術(shù)研究[A];2006北京地區(qū)高校研究生學(xué)術(shù)交流會(huì)——通信與信息技術(shù)會(huì)議論文集（下）[C];2006年

2 中國(guó)移動(dòng)通信集團(tuán)湖北有限公司課題組;傅國(guó);鄧峰;;信息化環(huán)境下IT風(fēng)險(xiǎn)導(dǎo)向?qū)徲?jì)初探[A];全國(guó)內(nèi)部審計(jì)理論研討優(yōu)秀論文集（2010）[C];2011年

3 張笑笑;張艷;顧健;;等級(jí)測(cè)評(píng)中主機(jī)安全配置檢查方法研究[A];全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集·第二十五卷[C];2010年

4 吳麗輝;張海霞;連一峰;;科研信息化安全保障體系建設(shè)方案[A];全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集·第二十五卷[C];2010年

5 徐云峰;;基于AHP理論的信息系統(tǒng)安全評(píng)估方法[A];第26次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)論文集[C];2011年

6 周鳴;常霞;;基于3G網(wǎng)絡(luò)的增值業(yè)務(wù)系統(tǒng)的安全防護(hù)策略[A];2010年全國(guó)通信安全學(xué)術(shù)會(huì)議論文集[C];2010年

7 舒萌;李永輝;張國(guó)強(qiáng);;等級(jí)測(cè)評(píng)項(xiàng)目實(shí)施問(wèn)題思考[A];第二屆全國(guó)信息安全等級(jí)保護(hù)測(cè)評(píng)體系建設(shè)會(huì)議論文集[C];2012年

8 秦超;;面向等保體系的邊界訪問(wèn)控制及實(shí)現(xiàn)技術(shù)研究[A];第二屆全國(guó)信息安全等級(jí)保護(hù)測(cè)評(píng)體系建設(shè)會(huì)議論文集[C];2012年

9 唐剛;朱信銘;程曉妮;;數(shù)據(jù)加密有效性測(cè)試的探究[A];第二屆全國(guó)信息安全等級(jí)保護(hù)測(cè)評(píng)體系建設(shè)會(huì)議論文集[C];2012年

10 范淵;;應(yīng)用層等級(jí)保護(hù)測(cè)評(píng)工具應(yīng)用實(shí)例分析[A];第二屆全國(guó)信息安全等級(jí)保護(hù)測(cè)評(píng)體系建設(shè)會(huì)議論文集[C];2012年

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前10條

1 蔡智勇;高安全等級(jí)網(wǎng)絡(luò)中信息隱蔽分析和實(shí)用抵抗模型[D];浙江大學(xué);2009年

2 楊天路;網(wǎng)絡(luò)威脅檢測(cè)與防御關(guān)鍵技術(shù)研究[D];北京郵電大學(xué);2010年

3 劉昌平;可信計(jì)算環(huán)境安全技術(shù)研究[D];電子科技大學(xué);2011年

4 范艷芳;重要信息系統(tǒng)強(qiáng)制訪問(wèn)控制模型研究[D];北京交通大學(xué);2011年

5 李勇;基于可信計(jì)算的應(yīng)用環(huán)境安全研究[D];解放軍信息工程大學(xué);2011年

6 吳世忠;基于風(fēng)險(xiǎn)管理的信息安全保障的研究[D];四川大學(xué);2002年

7 梁洪亮;支持多安全政策的安全操作系統(tǒng)的研究與實(shí)施[D];中國(guó)科學(xué)院研究生院（軟件研究所）;2002年

8 朱魯華;安全操作系統(tǒng)模型和實(shí)現(xiàn)結(jié)構(gòu)研究[D];中國(guó)人民解放軍信息工程大學(xué);2002年

9 劉文清;《結(jié)構(gòu)化保護(hù)級(jí)》安全操作系統(tǒng)若干關(guān)鍵技術(shù)的研究[D];中國(guó)科學(xué)院研究生院（軟件研究所）;2002年

10 劉海峰;安全操作系統(tǒng)若干關(guān)鍵技術(shù)的研究[D];中國(guó)科學(xué)院研究生院（軟件研究所）;2002年

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù) 前10條

1 朱春雷;兵員管理系統(tǒng)安全機(jī)制研究[D];哈爾濱工程大學(xué);2010年

2 王曉宇;用戶數(shù)據(jù)的多重保護(hù)技術(shù)研究與應(yīng)用[D];大連海事大學(xué);2010年

3 徐磊;甘肅移動(dòng)數(shù)據(jù)網(wǎng)安全評(píng)估與對(duì)策研究[D];蘭州大學(xué);2010年

4 王建紅;基于網(wǎng)絡(luò)的安全評(píng)估技術(shù)研究與設(shè)計(jì)[D];中原工學(xué)院;2011年

5 賀國(guó)強(qiáng);多級(jí)安全關(guān)系數(shù)據(jù)庫(kù)管理系統(tǒng)研究[D];西安電子科技大學(xué);2011年

6 李源;基于虛擬組織的網(wǎng)格安全模型研究[D];西安電子科技大學(xué);2009年

7 郭鴻雁;基于數(shù)據(jù)挖掘的自適應(yīng)網(wǎng)絡(luò)安全審計(jì)系統(tǒng)的研究與實(shí)現(xiàn)[D];山東師范大學(xué);2011年

8 呂桃霞;基于Agent技術(shù)的網(wǎng)絡(luò)安全審計(jì)模型研究與實(shí)現(xiàn)[D];山東師范大學(xué);2011年

9 逯楠楠;數(shù)據(jù)庫(kù)安全審計(jì)分析技術(shù)研究與應(yīng)用[D];湖北工業(yè)大學(xué);2011年

10 楊司祺;基于共享資源矩陣法的Linux內(nèi)核隱蔽通道搜索研究[D];北京交通大學(xué);2011年

【相似文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前10條

1 武海鷹;王小明;丁劍鋒;閔祥參;;基于強(qiáng)制訪問(wèn)控制的電子軍務(wù)模型[J];電子科技;2006年05期

2 范艷芳;蔡英;耿秀華;;具有時(shí)空約束的強(qiáng)制訪問(wèn)控制模型[J];北京郵電大學(xué)學(xué)報(bào);2012年05期

3 林宏剛,戴宗坤,李煥洲;BLP模型的時(shí)域安全研究[J];計(jì)算機(jī)應(yīng)用;2005年12期

4 張大剛;;數(shù)據(jù)倉(cāng)庫(kù)基于角色強(qiáng)制訪問(wèn)控制研究[J];計(jì)算機(jī)與現(xiàn)代化;2011年05期

5 阮越;楊學(xué)兵;周建欽;紀(jì)濱;;基于LSM的分布式強(qiáng)制訪問(wèn)控制的設(shè)計(jì)與實(shí)現(xiàn)[J];計(jì)算機(jī)技術(shù)與發(fā)展;2006年12期

6 唐為民;彭雙和;韓臻;沈昌祥;;一種基于角色的強(qiáng)制訪問(wèn)控制模型[J];北京交通大學(xué)學(xué)報(bào);2010年02期

7 霍建同;李云春;楊秀梅;;HPC機(jī)群分布式強(qiáng)制訪問(wèn)控制技術(shù)可行性研究[J];計(jì)算機(jī)科學(xué)與探索;2014年05期

8 潘海雷;吳曉平;廖巍;;XML文檔的細(xì)粒度強(qiáng)制訪問(wèn)控制研究[J];計(jì)算機(jī)工程;2012年20期

9 洪帆,何緒斌,徐智勇;基于角色的訪問(wèn)控制[J];小型微型計(jì)算機(jī)系統(tǒng);2000年02期

10 梁彬 ,孫玉芳 ,石文昌 ,孫波;一種改進(jìn)的以基于角色的訪問(wèn)控制實(shí)施BLP模型及其變種的方法[J];計(jì)算機(jī)學(xué)報(bào);2004年05期

中國(guó)重要報(bào)紙全文數(shù)據(jù)庫(kù) 前1條

1 本報(bào)記者 陳巍巍;為“系統(tǒng)層”把好安全關(guān)[N];計(jì)算機(jī)世界;2011年

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前1條

1 范艷芳;重要信息系統(tǒng)強(qiáng)制訪問(wèn)控制模型研究[D];北京交通大學(xué);2011年

中國(guó)碩士學(xué)位論文全文數(shù)據(jù)庫(kù) 前5條

1 朱祥彬;安全數(shù)據(jù)庫(kù)強(qiáng)制訪問(wèn)控制的研究與實(shí)現(xiàn)[D];吉林大學(xué);2010年

2 竺林;鐵路信息系統(tǒng)網(wǎng)關(guān)設(shè)備中強(qiáng)制訪問(wèn)控制的研究與實(shí)現(xiàn)[D];北京交通大學(xué);2014年

3 周述文;達(dá)夢(mèng)數(shù)據(jù)庫(kù)強(qiáng)制訪問(wèn)控制機(jī)制研究[D];華中科技大學(xué);2008年

4 單華松;達(dá)夢(mèng)安全數(shù)據(jù)庫(kù)對(duì)象特性強(qiáng)制訪問(wèn)控制的研究[D];華中科技大學(xué);2006年

5 肖峰;Linux平臺(tái)下基于動(dòng)態(tài)屬性的強(qiáng)制訪問(wèn)控制的設(shè)計(jì)與實(shí)現(xiàn)[D];中山大學(xué);2014年

，

本文編號(hào)：1040122