數(shù)據(jù)庫管理系統(tǒng)安全性形式化分析研究.pdf

1、數(shù)據(jù)庫的應用已經(jīng)滲透到各個領(lǐng)域，數(shù)據(jù)庫中存儲的大量敏感數(shù)據(jù)是攻擊者所覬覦的，數(shù)據(jù)庫的安全問題一直備受關(guān)注。研究并開發(fā)高安全等級的數(shù)據(jù)庫管理系統(tǒng)，對于提高數(shù)據(jù)庫系統(tǒng)的安全性具有重要意義。在開發(fā)四級及以上的高安全等級的數(shù)據(jù)庫管理系統(tǒng)過程中，需要引入形式化分析技術(shù)，對安全模型、頂層規(guī)范甚至系統(tǒng)代碼進行分析，以保障系統(tǒng)在設(shè)計和實現(xiàn)上符合安全模型的要求。
　　針對傳統(tǒng)的數(shù)據(jù)庫形式化安全模型在存儲過程、觸發(fā)器的處理上可能存在的安全缺陷，改進了

2、數(shù)據(jù)庫安全模型，使得該模型能夠安全地處理存儲過程和觸發(fā)器等數(shù)據(jù)庫對象。該模型擴充了狀態(tài)轉(zhuǎn)換規(guī)則，改進了客體兼容性，將實體完整性、參照完整性和客體兼容性作為所有狀態(tài)應滿足的安全性質(zhì)，保證系統(tǒng)狀態(tài)的正確性與一致性。
　　針對新的數(shù)據(jù)庫安全模型，給出了基于定理證明器Coq的安全模型規(guī)范和安全性分析，給出了用于安全性分析的狀態(tài)不變式、相關(guān)公理、引理和推論，以及各狀態(tài)轉(zhuǎn)換規(guī)則的規(guī)范描述和證明步驟，通過形式化分析，修改了新模型存在的不足，表明

3、新模型是安全的。
　　針對多級安全數(shù)據(jù)庫管理系統(tǒng)，給出了基于安全數(shù)據(jù)字典的多級安全數(shù)據(jù)庫管理系統(tǒng)頂層規(guī)范形式化分析。定義了多級安全數(shù)據(jù)字典作為安全數(shù)據(jù)庫管理系統(tǒng)的狀態(tài)的成員，基于該系統(tǒng)狀態(tài)和狀態(tài)不變式、系統(tǒng)操作規(guī)則的形式化規(guī)范描述，給出了基于數(shù)據(jù)字典的頂層抽象規(guī)范的安全性形式化分析，對數(shù)據(jù)庫管理系統(tǒng)頂層規(guī)范進行了基于定理證明器Coq的描述和安全性分析，改進了原有的系統(tǒng)頂層規(guī)范在設(shè)計過程中的缺陷，表明頂層規(guī)范的設(shè)計是符合安全模型要求

4、的。
　　在將BLP模型直接擴展映射到源代碼進行分析的過程中，針對數(shù)據(jù)庫管理系統(tǒng)的特點，對BLP模型中描述系統(tǒng)狀態(tài)的元素可訪問集分析后,發(fā)現(xiàn)在刪除操作的分析中，后狀態(tài)滿足某些安全性質(zhì)時，實際上并不需要滿足刪除操作的任何前提條件，就可以證明得到后狀態(tài)是安全的，證明有被繞過的可能，不能保證證明的完備性和嚴密性。利用完全依賴于安全操作系統(tǒng)實現(xiàn)強制訪問控制的數(shù)據(jù)庫管理系統(tǒng)DMOSMAC代碼規(guī)模小的特點,對DMOSMAC進行了形式化分析和證

5、明，以確保DMOSMAC正確實現(xiàn)了安全策略。給出了這類體系結(jié)構(gòu)下的數(shù)據(jù)庫管理系統(tǒng)進行形式化分析的方法。給出了數(shù)據(jù)庫內(nèi)的信息流定義，在此基礎(chǔ)上給出了一種對系統(tǒng)代碼進行抽取，避免刪除等操作的證明被繞過的可能,保證安全性分析過程的嚴密性。結(jié)果表明該方法能夠有效避免BLP模型直接用于數(shù)據(jù)庫系統(tǒng)安全性形式化分析時可能引起的證明被繞過的問題。
　　通過以上研究，我們在數(shù)據(jù)庫管理系統(tǒng)的形式化安全模型及其安全性分析、頂層規(guī)范以及實現(xiàn)級安全性分析等