Biba實用模型的自動化形式驗證

徐亮　劉宏

摘要：通過給傳統(tǒng)的Biba模型增加相應(yīng)的敏感級函數(shù)， 完善其主客體完整性標(biāo)簽， 并對其安全操作規(guī)則進行相應(yīng)的改進， 使其適應(yīng)實際的應(yīng)用需求. 采用完全形式化的方法對改進后模型中的各元素、模型必須滿足的不變式以及模型遷移規(guī)則進行描述， 并在此基礎(chǔ)上利用定理證明器Isabelle完成對該模型的自動化形式驗證， 從而實現(xiàn)高等級安全操作系統(tǒng)研發(fā)過程中對安全策略模型的形式化需求.

關(guān)鍵詞：Biba模型；形式化方法；定理證明；自動化形式驗證；安全策略

中圖分類號：TP301.2 文獻標(biāo)識碼：A

安全操作系統(tǒng)的完整性指的是數(shù)據(jù)或數(shù)據(jù)源的可信性.“完整性”經(jīng)常在阻止不恰當(dāng)及未授權(quán)的改變時涉及到.信息源與它的精確性和可信性以及人們對該信息的信任程度有關(guān).完整性的可信性方面對于系統(tǒng)的正常運作至關(guān)重要.完整性的目標(biāo)有3個_[1]：

1）防止未授權(quán)用戶的修改；

2）防止授權(quán)用戶的不當(dāng)修改；

3）維護數(shù)據(jù)的內(nèi)部和外部一致性.

常見的完整性模型有Biba模型_[2]、ClarkWilson模型_[3]、DTE模型_[4]、Sutherland模型_[5]以及Biba改進模型_[6-7]等.DTE模型和Sutherland模型只是其中的某些特性可以達到完整性保護的目的，而并不是作為完整性模型提出的；ClarkWilson模型沒有用形式化的語言來描述；Biba模型是專門為完整性保護提出的，使用了嚴(yán)格的形式化語言來描述，可以有效保護系統(tǒng)數(shù)據(jù)的完整性，但降低了系統(tǒng)的可用性；Biba改進模型對傳統(tǒng)的Biba模型進行了改進并給出了具有形式化語言的描述，符合GB/T20272-2006_[8]中對結(jié)構(gòu)化保護級安全策略模型開發(fā)要求，但在該模型中并沒有對模型的正確性給出自動化的形式證明，同時，其主客體完整性的基本操作也相對簡單.

在操作系統(tǒng)的形式化驗證工作中，微軟的SLAM_[9]主要是對C語言進行模型檢測；NICTA的L4.Verified_[10-11]則只針對seL4微內(nèi)核進行了從規(guī)范到代碼的驗證分析，都沒有嚴(yán)格意義上對某一具體安全策略模型進行驗證.本文針對安全策略模型中的完整性模型，為模型引入了多安全標(biāo)簽，以及適合實際系統(tǒng)的安全模型操作規(guī)則共十條，并在此基礎(chǔ)上，采用定理證明的方法[12-13]，將組成模型的各元素、操作規(guī)則和不變式用Isabelle_[14]定理證明器能接受的完全形式化的語言進行描述，并對其進行正確性的自動化證明，從而滿足GB/T20272-2006中關(guān)于最高等級安全操作系統(tǒng)——訪問驗證保護級操作系統(tǒng)研發(fā)中對形式化安全策略模型的要求.

3.4BLP模型的狀態(tài)遷移規(guī)則及其安全證明腳本

系統(tǒng)要始終保持在安全狀態(tài)運行，除了初始狀態(tài)要滿足安全要求以外，系統(tǒng)的所有遷移規(guī)則也必須滿足安全要求，也即由安全狀態(tài)經(jīng)過任意一條遷移規(guī)則以后到達的狀態(tài)仍然是安全狀態(tài).接下來就是對系統(tǒng)中各條遷移規(guī)則的安全性自動化證明腳本.

4結(jié)語

本文以研究設(shè)計符合GB/T20272-2006中對最高等級安全操作系統(tǒng)——訪問驗證保護級安全操作系統(tǒng)要求的完全形式化的安全策略模型為目標(biāo)，提出了一種具有實際可行性的Biba模型，并詳細(xì)定義了模型的不變量和安全遷移規(guī)則，使得該模型能夠滿足系統(tǒng)實際操作的需要.于此同時，我們還以定理證明工具Isabelle為依托，對模型的安全狀態(tài)、安全性質(zhì)、初始化狀態(tài)進行完全形式化的描述，參照文中對3條遷移規(guī)則的具體描述和驗證方法，可以給出全部11條安全遷移規(guī)則的自動化正確性驗證腳本，從而完成了對模型的自動化形式驗證工作.

參考文獻

[1]BISHOP M. Computer security： art and science[M]. Boston： Addison Wesley， 2003： 3-6.

[2]BIBA K J. Integrity considerations for secure computer systems[R]. Washington： US Air Force Electronic System Division， 1977.

[3]CLARK D D， WILSON D R. A comparison of commercial and military computer security policies[C]//Proceedings of IEEE Symposium Security and Privacy. Oakland： IEEE， 1987： 184-195.

[4]BADGER L， STERNE D F， SHERMAN D L， et al. A domain and type enforcement UNIX prototype[C]// Proceedings of the Fifth USENIX UNIX Security Symposium. Utah： USENIX， 1996： 127-140.

[5]SUTHERLAND D. A model of information[C]//Proceedings of the 9th National Computer Security Conference. Gaithersburg： U.S. Government Printing Office， 1986： 126-132.

[6]郭榮春， 劉文清， 徐寧，等. Biba改進模型在安全操作系統(tǒng)中的應(yīng)用[J]. 計算機工程， 2012， 38（13）： 96-98.

[7]張明西， 韋俊銀， 程裕強，等. 具有歷史特征的Biba模型嚴(yán)格完整性策略[J]. 鄭州大學(xué)學(xué)報：理學(xué)版， 2011， 43（1）： 85-89.

[8]GB/T 20272-2006 信息安全技術(shù)操作系統(tǒng)安全技術(shù)要求[S]. 北京： 中國國家標(biāo)準(zhǔn)化管理委員會， 2006.

GB/T 20272-2006 Information Security TechnologySecurity Techniques Requirement for Operating System[S]. Beijing： China National Standardization Management Committee， 2006.（In Chinese）

[9]SLAM[EB/OL]. （20120714）[20120812]. http：//research.microsoft.com/en-us/projects/slam/.

[10]KEVIN E， GERWIN K， RAFAL K. Formalising a highperformance microkernel[C]//Proceedings of Workshop on Verified Software： Theories， Tools， and Experiments. Seattle： Springer， 2006： 1-7.

[11]GERWIN K， MICHAEL N， KEVIN E， et al. Verifying a highperformance microkernel[R]. Baltimore： 7th Annual HighConfidence Software and Systems Conference， 2007.

[12] GENESERETH M R， NILSSON N J. Logical foundations of artificial intelligence [M]. California： Morgan Kaufmann， 1987： 87-90.

[13] DAVIS M， LOGEMANN G， LOVELAND D. A machine program for theorem proving [J]. Communications of the ACM， 1962， 5（7）： 394-397.

[14]ISABELLE[OL]. （20120712）[20120812]. http：//www.cl.cam.ac.uk/research/hvg/isabelle/.