王榕，張敏，馮登國，李昊

（1. 中國科學(xué)院 軟件研究所 可信計算與信息保障實驗室，北京 100190；2. 中國科學(xué)院大學(xué)，北京 100190；3. 中國科學(xué)院 軟件研究所 計算機科學(xué)國家重點實驗室，北京 100190）

1 引言

數(shù)據(jù)庫管理系統(tǒng)是多數(shù)信息系統(tǒng)的重要基礎(chǔ)平臺，其安全性是信息系統(tǒng)安全中的重要環(huán)節(jié)。近年來，伴隨著國家信息化建設(shè)飛速發(fā)展，我國對數(shù)據(jù)庫系統(tǒng)的安全也逐步重視，已有一批達到國標[1]第三級產(chǎn)品，在軍用、政務(wù)、電力、通信、鐵路等國家重要領(lǐng)域逐漸得到應(yīng)用推廣，取代國外同類產(chǎn)品，發(fā)揮骨干支撐作用。但是隨著國家信息化程度的提高，現(xiàn)有第三級數(shù)據(jù)庫產(chǎn)品已經(jīng)逐漸不能滿足安全需求。因此，迫切需要開展高安全等級數(shù)據(jù)庫構(gòu)建與評估技術(shù)的研究。而本文關(guān)注的安全策略模型建模與分析就是其核心技術(shù)之一。

安全策略模型是獨立于軟件實現(xiàn)的高層概念模型，它來源于需求規(guī)約，描述安全系統(tǒng)的安全保護需求與功能性質(zhì)[2]。安全策略模型的形式化分析是評估第四級系統(tǒng)[1]的重要內(nèi)容之一，在許多應(yīng)用領(lǐng)域都扮演著重要的角色，如建立可信操作系統(tǒng)、可信數(shù)據(jù)庫管理系統(tǒng)等高可信軟件系統(tǒng)。目前，通過一系列形式化方法在工程中的應(yīng)用[3～5]，對系統(tǒng)進行形式化描述和驗證不僅可以發(fā)現(xiàn)系統(tǒng)設(shè)計上的問題、驗證系統(tǒng)設(shè)計的正確性，而且還可以指導(dǎo)開發(fā)、檢驗系統(tǒng)實現(xiàn)的正確性等。然而在數(shù)據(jù)庫安全領(lǐng)域，現(xiàn)有的形式化方法還不能滿足實際需求。此外形式化方法在很大程度上受到其支持工具的限制，一些語言和分析方法由于缺乏原生分析工具的支持，導(dǎo)致驗證效率不能滿足大型復(fù)雜系統(tǒng)的工程需求。如Z語言，在20世紀80年代末到90年代初國際上相繼提出了很多Z語言的擴展，并進行了一些標準化工作，提出了與形式化方法和面向?qū)ο蠓椒ㄏ嘟Y(jié)合的思想[6,7]。然而，雖然基于Z語言的形式化方法和相關(guān)工具得到了發(fā)展，但是仍然無法支持在數(shù)據(jù)庫等大型復(fù)雜系統(tǒng)的工程應(yīng)用。

針對這些問題，本文提出了一種高等級數(shù)據(jù)庫形式化安全策略模型的建模方法，并將其應(yīng)用于實際商用數(shù)據(jù)庫 BeyonDB中進行有效性驗證。該數(shù)據(jù)庫經(jīng)相關(guān)測評機構(gòu)測評已達到第三級，并具備部分第四級安全特性。將本文提出的建模與分析方法應(yīng)用于 BeyonDB安全功能設(shè)計與開發(fā)中，幫助發(fā)現(xiàn)并糾正了系統(tǒng)若干設(shè)計缺陷，取得了良好的實際效果。

2 相關(guān)工作

近年來，國內(nèi)外已逐漸開展了形式化方法在各類模型及實際系統(tǒng)中的安全分析的研究，如操作系統(tǒng)、防火墻等。Qian等[8]采用數(shù)學(xué)形式化方法，使用OSOSM對操作系統(tǒng)進行建模并采用Isabelle驗證，保證了系統(tǒng)的高度安全性。Yang等[9]從完整性模型的實用性角度出發(fā)，提出一種新型的動態(tài)完整性保護模型（DMIP, dynamic integrity protection model），并給出了形式化分析。還有部分工作提出了在形式化安全策略模型驗證的基礎(chǔ)上對目標系統(tǒng)進行測試的方法。數(shù)據(jù)庫的安全策略模型形式化分析，由于其分析規(guī)模和主客體的復(fù)雜性，目前仍然缺少實際商用的安全策略模型的形式化建模與分析方法。

Bell和LaPadula在1975年提出了BLP經(jīng)典模型[10]，基于該模型提出了保護數(shù)據(jù)機密性的重要思想，為后來數(shù)據(jù)庫管理系統(tǒng)各種安全策略模型的建立奠定了堅實的基礎(chǔ)。SeaView模型[11]基于BLP經(jīng)典模型，詳細提出了 16條完整性約束，分析了包括自主訪問控制（DAC, discretionary access control）和強制訪問控制（MAC, mandatory access control）等安全模型，訪問控制粒度實現(xiàn)元素級，為多級安全數(shù)據(jù)庫的設(shè)計和分析提出了良好的基礎(chǔ)。但是，SeaView模型[11]采用的是 TCB子集架構(gòu)[12]，將數(shù)據(jù)庫管理系統(tǒng)與 TCB分開描述，不能滿足當今大部分采用可信主體架構(gòu)[12]的商用數(shù)據(jù)庫的形式化分析需求。Li等[13]提出了一種基于Z語言的策略模型形式化方法，并且以BLP模型為例進行了驗證。Zhu等[14]擴展了SeaView模型的客體結(jié)構(gòu)，在豐富了客體類型的同時擴展了安全屬性，并用 Gallina語言對其進行了形式化描述，在Coq定理證明器幫助下對模型進行了證明。Sandhu[15]提出了基于角色進行訪問控制的RBAC（role-based access control）模型，該模型將權(quán)限與角色相關(guān)聯(lián)，通過角色獲取的權(quán)限進行訪問控制，極大地簡化了權(quán)限的管理。He等[16]不僅提出了詳細的安全屬性，還將BLP模型和RBAC模型進行了邏輯結(jié)合，采用Z語言對該模型進行形式化描述，實現(xiàn)了多策略的數(shù)據(jù)庫管理系統(tǒng)訪問控制。

上述相關(guān)工作多數(shù)集中于對 DBMS的通用模型部分進行研究，其訪問控制粒度較粗，不滿足高等級系統(tǒng)要求；或提出新的數(shù)據(jù)庫安全策略模型，并進行形式化分析，沒有考慮數(shù)據(jù)庫系統(tǒng)完整性約束等固有屬性，缺少從實際數(shù)據(jù)庫系統(tǒng)建立安全策略模型的方法。更加缺少對實際商用數(shù)據(jù)庫管理系統(tǒng)的安全策略模型進行描述和分析。

基于以上原因，本文提出了一種數(shù)據(jù)庫形式化建模和安全性分析方法，該方法建立的模型能夠提供更加完整的安全屬性描述，更加靈活的可擴展性，保證了建模和驗證的效率，并且應(yīng)用于實際數(shù)據(jù)庫系統(tǒng)，發(fā)現(xiàn)數(shù)據(jù)庫安全功能設(shè)計和實現(xiàn)中的錯誤和缺陷，驗證了其有效性。

3 PVS語言及定理證明器

本文采用了國際上較為流行的 PVS語言和驗證工具作為形式化方法的基礎(chǔ)。該系統(tǒng)由斯坦福研究機構(gòu)開發(fā)，包括PVS規(guī)約語言和PVS定理證明器2部分組成：前者基于高階邏輯，具有豐富的數(shù)據(jù)類型系統(tǒng)，表達能力強；后者采用目標制導(dǎo)的方式工作，即一個證明的構(gòu)造從待證明的定理開始，逐步推理，不斷生成子目標，直至所有子目標均為真。PVS定理證明器擁有強大靈活的命令集。高效的決策過程、高度交互與自動化的定理證明使PVS在當今形式化語言中較有優(yōu)勢。

PVS語言不但擁有強有力的推理機制，而且有豐富的表達手段，目前已在很多領(lǐng)域得到應(yīng)用。典型應(yīng)用包括：我國國內(nèi)可信電子電力系統(tǒng)的建模與證明、軌交控制系統(tǒng)的SCADE開發(fā)和國際上NASA的對基于時間觸發(fā)以太網(wǎng)的時鐘同步協(xié)議的形式化驗證等。

4 安全策略形式化描述方法

國標GB17859-1999[1]中指出：為了滿足結(jié)構(gòu)化保護系統(tǒng)功能的安全性要求，安全策略模型的形式化應(yīng)該至少包含自主訪問控制和強制訪問控制。因此，以BeyonDB系統(tǒng)對BLP模型的實現(xiàn)為例展示本文的建模方法，流程如圖1所示。為使形式化模型與實際數(shù)據(jù)庫保持高度的一致性，將形式化安全策略模型的描述和安全性分析分為3個部分。

1) 模型目標提取：抽取必要的實體與操作。

2) 系統(tǒng)狀態(tài)、操作規(guī)則生成與描述：對數(shù)據(jù)庫相關(guān)實體進行分析、描述、綜合生成系統(tǒng)狀態(tài)；利用系統(tǒng)狀態(tài)中描述的實體等內(nèi)容描述操作規(guī)則。

3) 描述安全定義并進行安全性分析：描述系統(tǒng)安全定義，對模型進行安全分析，交互式證明安全定理。通過安全分析發(fā)現(xiàn)系統(tǒng)安全缺陷，指導(dǎo)修改系統(tǒng)設(shè)計。重復(fù)以上步驟，不斷完善形式化模型。

4.1 模型目標提取

對于形式化模型中應(yīng)該具體描述的實體，抽取途徑主要是通過系統(tǒng)中頂層的訪問控制接口、安全需求以及數(shù)據(jù)庫系統(tǒng)實際的系統(tǒng)表，采用基于操作接口的目標提取方法來獲取描述目標，即對于一個指定的訪問控制接口，統(tǒng)一以操作者、操作目標、操作成功判斷條件的形式對每一個操作接口進行描述和分析。如表1所示，在BeyonDB數(shù)據(jù)庫中，根據(jù)實際操作接口 Insert，結(jié)合實際存在的系統(tǒng)表iiuser，將操作者抽象為模型中的主體：User；根據(jù)操作的對象實體表格，抽象出客體：Realtable；同時在實際的強制訪問控制和自主訪問控制中需要判斷實關(guān)系表和操作者的標簽支配關(guān)系，所以需要對標簽（Label）和標簽支配判斷函數(shù)（dom?）進行描述并定義。按此方法對系統(tǒng)中所有接口進行描述，分類總結(jié)出系統(tǒng)的基本元素，為下一步的形式化語言描述提供必要基礎(chǔ)。

圖1 形式化建模與安全分析流程

表1 操作Insert的描述目標提取

4.2 系統(tǒng)狀態(tài)生成與描述

完成了上述基于操作接口的目標提取后，使用PVS語言對提取出的元素進行描述，描述內(nèi)容包括實體、與數(shù)據(jù)完整性相關(guān)的約束元素、訪問控制相關(guān)元素、系統(tǒng)狀態(tài)、操作規(guī)則。在描述中，為了使形式化模型具有較高的可讀性和驗證的效率，充分應(yīng)用 PVS語言中一些內(nèi)置類型、類型構(gòu)造器及函數(shù)。例如采用PVS語言中的集合類型來描述實體，在判斷某一類型的實體時，利用PVS語言內(nèi)置函數(shù)member能夠方便判斷某一元素是否存在于某一指定的集合當中。如系統(tǒng)狀態(tài)，為了快速提取狀態(tài)中某一內(nèi)容，采用記錄類型對狀態(tài)進行描述，同時也提高了代碼的可讀性。

4.2.1 實體描述

1) 主體存在

本文使用集合類型對各類實體進行描述，優(yōu)點是可以直接利用PVS定理證明器內(nèi)置的member和subset函數(shù)來判斷某一個元素是否在一個集合中或一個集合是否是另外一個集合的子集。同時為了增加語言的可讀性和使用的靈活性，采用記錄類型描述所有主體集合（主體存在Subject_Exist），每一類主體集合作為記錄中的一個域，例如 UserExist是主體的集合，RoleExist是角色的集合。主體存在描述具體如圖2所示。

圖2 主體存在描述

2) 主體映射

主體映射描述了數(shù)據(jù)庫中相關(guān)聯(lián)主體間的對應(yīng)關(guān)系，如用戶與組、用戶與輪廓以及用戶與角色等。各類對應(yīng)關(guān)系均采用PVS語言中的函數(shù)類型來描述，如引入函數(shù)類型映射 UsertoType:TYPE=[USER->USER_TYPE]描述用戶到用戶類型，再將各類與主體相關(guān)的函數(shù)映射組織成記錄類型Subject_Map（如圖3所示），Subject_Map的生成為自主訪問控制和強制訪問控制提供了方便的依據(jù)。

圖3 主體映射描述

3) 客體存在

將除數(shù)據(jù)庫客體以外的其他客體分為2類，一類是具有層次結(jié)構(gòu)的客體，如實關(guān)系表、元組、視圖；另一類是不具有層次關(guān)系的客體，如事件、序列、過程。模型中，將客體組織成如下樹形結(jié)構(gòu)，如圖4所示。為了描述數(shù)據(jù)庫中復(fù)雜的客體和繁多的完整性關(guān)系，使用記錄格式ObjectExist描述模型中不同類型的客體，每一類客體集合作為記錄一個域，分別包括數(shù)據(jù)庫、實關(guān)系表、視圖和元組。

圖4 數(shù)據(jù)庫客體層次結(jié)構(gòu)

4) 客體映射

客體映射是各客體間的層次關(guān)系的抽象描述。通常采用的描述方法是，參照BeyonDB設(shè)計文檔，依據(jù)系統(tǒng)中各類系統(tǒng)表，將相關(guān)系統(tǒng)表關(guān)聯(lián)并抽象定義。例如，將設(shè)計文檔中iintegrity與iikey這2張系統(tǒng)表進行關(guān)聯(lián)并抽象，得到關(guān)系表與其引用表的映射 Realtable_Reftable。為方便描述數(shù)據(jù)庫系統(tǒng)的引用完整性這一固有屬性，要對必要的實體間映射進行描述，包括關(guān)系表與被引用表的映射RefTable_RealTable、元組與主鍵的映射Tuple_PKey、元組與外鍵的映射Tuple_FKey?？腕w間的映射函數(shù)應(yīng)至少包含上述內(nèi)容，映射關(guān)系如圖5所示。以上映射函數(shù)的描述為下文安全屬性定義提供基礎(chǔ)。

圖5 客體關(guān)系映射

4.2.2 策略相關(guān)元素描述

自主訪問控制和強制訪問控制的形式化證明是國家相關(guān)標準要求中的必要內(nèi)容。以 BeyonDB為例，自主訪問控制通過以下步驟進行：首先獲得該用戶擁有的權(quán)限，其次判斷指定權(quán)限是否在其中。按照系統(tǒng)設(shè)計文檔對該步驟進行細化，分別定義主體權(quán)限、客體權(quán)限、數(shù)據(jù)庫權(quán)限。為了滿足系統(tǒng)的可信主體權(quán)限最小化原則，將主體權(quán)限細分為系統(tǒng)權(quán)限、審計權(quán)限、安全權(quán)限，相應(yīng)定義了用戶到其擁有的不同類型權(quán)限的函數(shù)映射，并組織為記錄類型DAC_Table。強制訪問控制的核心操作是標簽支配判斷，首先分別獲得主客體標簽，然后進行標簽對比判斷。由此定義2個函數(shù)：主體到主體標簽的函數(shù)映射和客體到客體標簽的函數(shù)映射。最后，根據(jù)斷言dom？如圖6所示定義來進行標簽支配判斷（如下規(guī)約描述，返回一個BOOL 類型）。

圖6 dom?規(guī)約描述

同時為了增加系統(tǒng)的靈活性，能夠在會話當中動態(tài)調(diào)節(jié)主客體的標簽，根據(jù)系統(tǒng)中描述的最低、最高安全等級，最小、最大范疇，定義模型中安全等級范圍和范疇范圍，如圖7所示，均采用記錄類型描述，這樣便于對極限值的獲取。另外，為了記錄登錄用戶和數(shù)據(jù)庫的相關(guān)信息，定義一個會話記錄，通過會話記錄（下面表達式中的session）可以方便提取與登錄用戶和數(shù)據(jù)庫相關(guān)的內(nèi)容。在安全約束屬性描述中，為了給安全定義中的狀態(tài)屬性的證明提供依據(jù)，對當前用戶的合法操作進行記錄，定義一個記錄類型的動作記錄 Action_ID，再根據(jù)訪問控制不同分別用 Cur_Perms_DAC和 Cur_Perm_MAC 表示記錄的集合。

圖7 級別、范疇規(guī)約描述

4.2.3 系統(tǒng)狀態(tài)描述

一個數(shù)據(jù)庫的系統(tǒng)狀態(tài)應(yīng)該包含所有評估者關(guān)心的數(shù)據(jù)，僅對模型各單位元素進行描述是不充分的。本文使用記錄類型描述系統(tǒng)狀態(tài) system_state，并將不同類型的實體、關(guān)系映射、訪問控制等內(nèi)容組織成系統(tǒng)狀態(tài)中的一個域。這樣可以根據(jù)操作的需要從系統(tǒng)狀態(tài)中提取出相關(guān)的信息。system_state通過具體操作、安全屬性集合及實體關(guān)系集合進行獲取生成，具體算法如下。

系統(tǒng)狀態(tài)獲取算法

算法GetSystemState

輸入：操作集合OPERATIONS ，安全屬性集合INVARIANTS，實體或關(guān)系集合VARS

輸出：系統(tǒng)狀態(tài)SYSTEM_STATE

4.2.4 操作規(guī)則

操作規(guī)則（operation rules）描述了模型是如何具體實施安全策略的，揭示了2個連續(xù)狀態(tài)的狀態(tài)轉(zhuǎn)換過程中狀態(tài)變量之間的關(guān)系。針對不同操作，操作規(guī)則包括操作發(fā)生條件與操作執(zhí)行影響 2部分。操作發(fā)生條件即操作成功判斷條件，如強制訪問控制的標簽支配判斷、自主訪問控制授權(quán)檢查。操作執(zhí)行影響主要描述的是操作執(zhí)行后系統(tǒng)狀態(tài)變量的改變。操作規(guī)則的產(chǎn)生是將操作判斷條件和操作執(zhí)行后系統(tǒng)狀態(tài)變量的改變進行邏輯組合，具體算法如下所示。

操作規(guī)則生成算法

算法 Operation Rules Generation

輸入：系統(tǒng)狀態(tài)SS0，基于操作接口的目標提取方法中的各項操作成功判斷條件的邏輯與集合CONS，初始操作規(guī)則序列Rules

輸出：操作規(guī)則序列Rules

5 形式化策略模型安全分析

5.1 安全定義

在國標[1]對第四級的信息系統(tǒng)明確要求了自主訪問控制和強制訪問控制，此外針對不同的信息系統(tǒng)，還有其他特別的安全需求。對具體的數(shù)據(jù)庫系統(tǒng)來說，安全屬性的定義應(yīng)該從2個方面進行該考慮，首先是為滿足國家標準的安全屬性內(nèi)容，主要是以經(jīng)典安全策略模型作為基礎(chǔ)（自主訪問控制、強制訪問控制）；其次是針對不同系統(tǒng)的具體安全需求。例如，數(shù)據(jù)庫需要添加的固有的一些安全屬性（如實體完整性、引用完整性、用戶自定義完整性）。通過將要求的安全需求內(nèi)容與實際系統(tǒng)安全需求內(nèi)容結(jié)合定義出多條安全屬性。在安全屬性基礎(chǔ)之上，根據(jù)形式化驗證目標將不同安全屬性通過PVS中的邏輯運算符“and”進行連接來定義狀態(tài)安全，如圖8所示。具體地，針對BeyonDB，本文將數(shù)據(jù)庫安全屬性分為6條，包括主體標簽支配會話標簽，客體間標簽支配（關(guān)系標簽支配數(shù)據(jù)庫標簽，元組標簽支配關(guān)系標簽），自主訪問控制，簡單安全，*安全以及引用安全屬性。

圖8 安全定義與安全性分析

安全屬性1（主體標簽支配）：會話的發(fā)起者即當前用戶必須支配當前會話的安全標簽。

圖9 主體標簽支配描述

安全屬性2（客體間標簽支配）：為了達到更細粒度的標簽控制，需要滿足以下條件：關(guān)系的安全等級支配其所屬數(shù)據(jù)庫的安全等級；元組的安全等級支配其所屬的實關(guān)系表的安全等級（如圖10所示）。

圖10 客體標簽支配描述

安全屬性 3（自主安全）：根據(jù) cur_perms_DAC，如果當前用戶對某些客體進行過操作合法，那么該用戶必然是當前客體的屬主或者對該客體具有相應(yīng)的客體權(quán)限（如圖11所示）。

圖11 自主安全描述

安全屬性4（引用完整性）：數(shù)據(jù)完整性對數(shù)據(jù)庫來說至關(guān)重要，數(shù)據(jù)庫中的數(shù)據(jù)是否滿足完整性關(guān)系到其能否真實反映出現(xiàn)實世界，能否在數(shù)據(jù)庫中保護數(shù)據(jù)的正確性、有效性和相容性。尤其對于引用完整性，BeyonDB系統(tǒng)中采用了3種不同的策略，級聯(lián)刪除、受限刪除、置空刪除?？梢愿鶕?jù)需要采用不同的默認策略，這里限于篇幅原因描述受限刪除時的系統(tǒng)引用完整性如圖12所示，要求某一元組的外鍵要么全空，要么全部非空（此種情況必定存在相應(yīng)的一個被引用的表的元組，使其主鍵等于該元組的外鍵并且安全等級應(yīng)該支配被引用表的安全等級）。

圖12 引用完整性描述

安全屬性5（簡單安全性）：根據(jù)具體的數(shù)據(jù)庫的要求將BLP模型調(diào)整為：如果一個用戶對某客體進行了讀的操作，那么當前用戶的安全標簽應(yīng)該支配該客體的安全標簽從而達到不上讀的要求（如圖13所示）。

圖13 簡單安全性描述

安全屬性 6（*安全性）：如果一個用戶對某客體進行了寫操作，那么該客體的安全標簽一定支配當前用戶的安全標簽以達到不下寫的安全要求，如圖14所示。

圖14 *安全

5.2 安全性分析

僅僅定義出模型的各種元素是不充分的，必須對模型進行形式化的分析，即驗證模型描述的系統(tǒng)的安全性，系統(tǒng)處于安全的狀態(tài)。

因此系統(tǒng)狀態(tài)安全定義應(yīng)該是上述安全屬性、數(shù)據(jù)庫特有屬性約束和類型約束的組合。形式化定義如圖15所示。

圖15 形式化定義

該安全定義是以PVS斷言的and連接生成，可以靈活地添加各類數(shù)據(jù)庫屬性作為安全狀態(tài)的描述。由于 PVS能夠?qū)σ炎C明的片段進行保存，并可將已存的證明片段用于整體的證明過程。故以該方式定義的狀態(tài)安全在保證不影響已分析過的內(nèi)容的同時，增加新的安全斷言，從而使建模和分析的效率更高。

本文提出的安全性分析的思路是：首先使用do_init 函數(shù)對系統(tǒng)狀態(tài)進行初始化，得到初始狀態(tài) init_ss0，然后根據(jù)狀態(tài)安全定義 State_Safe?分析初始狀態(tài) init_ss0是否為安全狀態(tài)；然后，根據(jù)狀態(tài)安全的定義判斷任意狀態(tài) SS0是否安全，如果SS0安全則通過狀態(tài)轉(zhuǎn)移規(guī)則函數(shù)對SS0進行操作得到狀態(tài)SS1，則SS1也是安全的；重復(fù)上述操作直至所有可達狀態(tài)判斷完畢，如果所有可達狀態(tài)都是安全的那么數(shù)據(jù)庫系統(tǒng)就是安全的。由此，需要的安全定理包括：初始狀態(tài)安全定理和狀態(tài)轉(zhuǎn)換安全定理。

初始狀態(tài)安全定理 系統(tǒng)進行初始化操作后得到的狀態(tài)滿足安全狀態(tài)的定義。即要證明的基本安全定理如圖16所示。

圖16 初始狀態(tài)安全定理

狀態(tài)轉(zhuǎn)換安全定理 針對每一個操作，都應(yīng)保證對于一個安全狀態(tài)進行操作OP之后得可達狀態(tài)仍然是安全的。即操作運行之前處于安全狀態(tài)操作運行之后仍然處與安全狀態(tài)。

表達式為：狀態(tài)SS0安全and操作OP則可達狀態(tài)SS1也安全。即需要證明的狀態(tài)轉(zhuǎn)換安全定理如圖17所示。

圖17 安全定理

若能夠證明 InitialSafe和任意操作后的SecurityTheorem則系統(tǒng)就是安全的。本文采用PVS交互式證明對如上2個定理進行證明。并且發(fā)現(xiàn)了BeyonDB的一些缺陷。

在安全證明中，通常情況下很難一次證明成功，下面結(jié)合一些例子，舉出3類典型的錯誤原因。

原因一：模型與設(shè)計不統(tǒng)一，如 BeyonDB中要求一張引用表只能應(yīng)用到一張被引用表，則在形式化描述模型中引用表到被引用的映射關(guān)系（單向）則應(yīng)該是一對一的關(guān)系。如果遇到此類問題，需要檢查描述的模型，將模型與系統(tǒng)的實際設(shè)計嚴格對應(yīng)，防止不一致的問題發(fā)生。

原因二：模型未消除設(shè)計中的二義性，模型內(nèi)部存在矛盾和不一致性。如模型變量需要常量化時，需要保證該常量符與其他位置同一變量的常量符一致。這種問題的發(fā)生是因為對PVS證明機制沒有清楚了解，所以針對證明過程中使用的命令，需要明確命令的證明過程，尤其涉及到變量常量化的命令。

原因三：模型與設(shè)計相符，且描述方面沒有問題，仍然無法證明，則發(fā)現(xiàn)了系統(tǒng)設(shè)計中的確存在缺陷。

5.3 系統(tǒng)存在缺陷

將本文提出的方法對實際的商用數(shù)據(jù)庫BeyonDB進行分析，發(fā)現(xiàn)其一些典型的問題，并給而解決方案（如表 2所示），此時需要在系統(tǒng)中進行試驗確定系統(tǒng)漏洞，從而發(fā)現(xiàn)實際系統(tǒng)的安全缺陷，指導(dǎo)修改系統(tǒng)設(shè)計。

發(fā)生問題的主要類型有：系統(tǒng)設(shè)計本身不完整；操作執(zhí)行時不滿足安全屬性。

1) 策略設(shè)計不完整：制定策略時，忽略一些細節(jié)，尤其像對 procedure這種實體進行操作時容易出現(xiàn)問題。因為 procedure實體涉及到若干個不同安全等級的客體，如果僅僅考慮用戶主體安全標簽與 procedure安全標簽的標簽支配是不充分的。例如一個低等級用戶的安全標簽等級支配 procedure的安全標簽等級，系統(tǒng)中要求執(zhí)行者具有exec的權(quán)限。不關(guān)注用戶和所有涉及其他客體等級支配關(guān)系。當 procedure中包含高于用戶等級的客體時，用戶執(zhí)行該procedure，則低安全等級用戶間接訪問了高安全等級的客體，在操作執(zhí)行后會對操作所涉及的所有客體進行記錄，記錄（exec,object1），（exec,object2）等。在進行安全證明時，如果低等級用戶“讀”訪問了高安全等級的客體object1，則證明無法通過簡單安全屬性，返回系統(tǒng)，修改系統(tǒng)策略，要求在執(zhí)行 procedure的過程中，用戶的標簽安全等級需要支配 procedure所包含的所有客體的安全等級。

2) 實體設(shè)計不完整：設(shè)計系統(tǒng)實體時，存在安全隱患。當一個表格在沒有設(shè)置主鍵的情況下，允許插入內(nèi)容完全相同的記錄，且沒有序列號區(qū)分，例如安全等級為L1的用戶創(chuàng)建一個等級為L1的表格T1，插入一條等級為L1的元組R1，并且對該元組執(zhí)行了 select操作，系統(tǒng)會記錄該操作（select,R1）。然后提高了用戶自身的等級為L2，并且向L1表中插入等級為L2的相同內(nèi)容元組R1'，此時當系統(tǒng)進行證明時，當遇到相同內(nèi)容不同等級的R1和R1'時，無法進行判斷，不滿足簡單安全屬性。為了更加符合數(shù)據(jù)庫的完整性要求，所以在沒有主鍵的數(shù)據(jù)庫表格中系統(tǒng)要默認插入一列ID，不允許相同內(nèi)容的元組存在。

3) 策略執(zhí)行不滿足安全屬性：策略設(shè)計本身沒有問題。但是需要一定的前提條件，必須在滿足前提條件的情況下才滿足安全屬性。

a) 表級、行級開關(guān)：在BeyonDB中為了增加系統(tǒng)的靈活性，所以設(shè)置了表級還有行級的不同粒度的強制訪問控制開關(guān)。如果只開啟表級的強制訪問控制開關(guān)未開啟行級訪問控制開關(guān)，如果一位支配表級安全標簽等級的主體用戶就可以訪問該表的所有記錄，包含行級安全等級高于用戶的記錄。給出的解決方法是：表級、行級強制訪問控制開關(guān)必須同時開啟。

b) 在會話中，允許用戶修改會話標簽，用戶安全標簽修改后，則操作記錄中的部分記錄會違背安全屬性。比如用戶對客體O進行了讀操作（用戶安全標簽等級支配 O），若該用戶提高了自身的安全標簽等級且支配O，則不滿足“簡單安全屬性”和“星”安全屬性。給出的解決方法是：在會話過程中不允許用戶修改安全標簽。

表2 錯誤類型以及系統(tǒng)缺陷

5.4 方法對比

本文提出的方法與以往方法比較，描述的粒度是記錄級別，并且給出了數(shù)據(jù)庫固有的完整性方面的約束，并給出證明；沒有采用 TCB子集架構(gòu)，這樣更符合商用數(shù)據(jù)庫可信系統(tǒng)的要求。將本文方法與其他方法在實際系統(tǒng)相符性、安全屬性完整性、可擴展性、建模與驗證效率等幾個方面進行比較，如表3所示。

表3 方法對比

與實際系統(tǒng)設(shè)計相符性：提供了通過系統(tǒng)的變量以及系統(tǒng)表等內(nèi)容獲得實體與關(guān)系的方法，不僅僅局限于訪問控制的理論模型，而是將實際系統(tǒng)的設(shè)計細節(jié)反映在模型中，如針對客體定義Owner獲取客體的屬主，定義ProcedureToObject描述過程與客體的映射，定義Tuple_Fkey描述客體元組到外鍵的映射。針對主體，定義UserToRole，UserToGroup來描述用戶到角色，用戶到群組的映射?？紤]實際操作系統(tǒng)，定義出更加詳細的內(nèi)容。因此實用性更強，這是傳統(tǒng)理論模型分析方法中[7]并沒有涉及到的內(nèi)容。文獻[7]中只將客體簡單描述為單一客體O_Single并未詳細的考慮客體間、主體間的詳細內(nèi)容，僅僅針對DBLP涉及的內(nèi)容進行描述，局限性較強，并不適合實際的系統(tǒng)。文獻[16]中只對粗粒度的Database和Table進行描述，并未對細粒度的Tuple等進行討論。

安全屬性更加完備：安全屬性除了需要滿足安全測評相關(guān)標準對訪問控制的需求外，還需結(jié)合實際數(shù)據(jù)庫系統(tǒng)，將實體完整性等考慮在內(nèi)，而文獻[16]和文獻[7]并沒有考慮完整性。文獻[7]關(guān)注BLP模型文獻[16]關(guān)注RBAC和BLP模型，僅考慮系統(tǒng)中數(shù)據(jù)的機密性，忽略數(shù)據(jù)庫完整性。

可擴展性：作為結(jié)構(gòu)化建模方法的保證，采用了可擴展性的構(gòu)架，在系統(tǒng)狀態(tài)、安全定義、操作描述等方面采用PVS中的邏輯“與”描述使結(jié)構(gòu)相對于其他方法更加易于擴展，文獻[16]描述了不同的不變式，但是受到定理證明器的限制無法將不變式進行邏輯組合，導(dǎo)致部分不變式需要手工證明。

建模與驗證效率：迭代式的建模與證明過程使模型修改容易，迭代代價較小，并且PVS原生工具的支持使本文方法在實際工程中有更高的效率。其他文獻中，早期是采用手工證明，或者采用Z語言描述，但相應(yīng)證明器不能提供有效的推理支持，所以在大量需要展開的模式時效率非常低，這就要求在模型描述的時候進行優(yōu)化，但Z語言描述的模型在修改方面非常困難，故證明的工作量也會增加許多。文獻[7]中指出，當展開大量的模式時，定理的證明速度明顯放慢。而文獻[16]中針對部分的不變式無法采用機器證明，故采用人工證明，大大降低了證明的效率。

綜上，本文方法對于大型復(fù)雜系統(tǒng)在實際設(shè)計開發(fā)中應(yīng)用，能給與足夠的支持，幫助發(fā)現(xiàn)系統(tǒng)漏洞，指導(dǎo)系統(tǒng)開發(fā)并且在系統(tǒng)安全性建模和驗證效率方面都擁有更大優(yōu)勢。

6 結(jié)束語

本文提出了一種數(shù)據(jù)庫形式化安全策略模型建模與分析方法，為當前第四級安全數(shù)據(jù)庫管理系統(tǒng)的安全策略模型建模與分析提供參考。該方法基于設(shè)計文檔分析，抽象提取出安全定義和操作規(guī)則：前者體現(xiàn)系統(tǒng)關(guān)鍵安全需求，定義模型中狀態(tài)與狀態(tài)轉(zhuǎn)移間的約束；后者體現(xiàn)實施安全需求的方式。該方法在 BeyonDB數(shù)據(jù)庫安全策略模型分析中獲得了很好的效果，顯示出該模型安全屬性上的可擴展性和靈活性。采用的 PVS 語言以及其原生的定理證明器使該方法效率得到保障，證明該方法具有良好的可行性。

[1] 國家質(zhì)量監(jiān)督檢驗檢疫總局.GB17859-1999計算機信息系統(tǒng)安全保護等級劃分準則[S].北京:中國標準出版社,1999.General Administration of Quality Supervision, Inspection and Quarantine of P.R.C. GB17859-1999 Classified Criteria for Security Protection of Computer Information System[S]. Beijing:Standards Press of China, 1999.

[2] 張敏, 馮登國, 陳馳.基于安全策略模型的安全功能測試用例生成方法[J].計算機研宄與發(fā)展,2009,46(10):1686-1692.ZHANG M,FENG D G, CHEN C. A security function test suite generation method based on security policy model[J].Journal of Computer Research and Development, 2009, 46(10):1686-1692.

[3] 官尚元,伍衛(wèi)國,董小社.自動信任協(xié)商的形式化描述與驗證研究[J].通信學(xué)報,2011,32(3):86-99.GUAN S Y, WU W G. DONG X S. Research on formal description and verification of automated trust negotiation[J]. Journal on Communications, 2011, 32(3):86-99.

[4] LUO X Y, TAN Z, SU K L.A verification approach for web service compositions based on epistemic model checking[J].Chinese Journal of Computers, 2011,34(6):1041-1061.

[5] 肖芳雄, 黃志球, 曹子寧. Web 服務(wù)組合功能與 QoS 的形式化統(tǒng)一建模和分析[J]. 軟件學(xué)報, 2011, 22(11): 2698-2715.XIAO F X, HUANG Z Q, CAO Z N. Unified formal modeling and analyzing both functionality and QoS of Web services composition[J].Journal of Software, 2011, 22(11): 2698-2715.

[6] 陳小峰. 可信平臺模塊的形式化分析和測試[J]. 計算機學(xué)報, 2009,32(4): 646-653.CHEN X F. The formal analysis and testing of trusted platform module[J]. Chinese Journal of Computers, 2009, 32(4): 646-653.

[7] 何建波, 卿斯?jié)h, 王超. 對一類多級安全模型安全性的形式化分析[J]. 計算機學(xué)報, 2006, 29(8): 1468-1479.HE J B, QING S H, WANG C. Formal safety analysis of a class of multilevel security models[J]. Chinese Journal of Computers, 2006,29(8): 1468-1479.

[8] 錢振江, 黃皓, 宋方敏. 操作系統(tǒng)形式化設(shè)計與安全需求的一致性驗證研究[J]. 計算機學(xué)報, 2014, 37(5): 1082-1099.QIAN Z J, HUANG H, SONG F M. Research on consistency verification of formal design and security requirements for operating system[J]. Chinese Journal of Computers, 2014, 37(5):1082-1099.

[9] 楊濤, 王永剛, 唐禮勇. 一種實用動態(tài)完整性保護模型的形式化分析[J]. 計算機研究與發(fā)展, 2013, 50(10): 2082-2091.YANG T, WANG Y G, TANG L Y. A practical dynamic integrity protection model[J]. Journal of Computer Research and Development,2013, 50(10): 2082-2091.

[10] BELL D E, LA PADULA L J. Secure computer system: Unified exposition and multics interpretation[R]. MITRE CORP BEDFORD MA, 1976.

[11] LUNT T F, DENNING D E, SCHELL R R,et al. The sea view security model[J]. Software Engineering, IEEE Transactions, 1990,16(6): 593-607.

[12] 張敏, 徐震, 馮登國. 數(shù)據(jù)庫安全[M].北京:科學(xué)出版社, 2005.ZHANG M, XU Z, FENG D G. Database Security[M]. Beijing:Science Press, 2005.

[13] 李麗萍, 卿斯?jié)h,周洲儀. 安全策略模型規(guī)范及其形式分析技術(shù)研究[J]. 通信學(xué)報, 2006, 27(6): 94-101.LI L P, QING S H, ZHOU Z Y. Research on formal security policy model specification and its formal analysis[J]. Journal on communications,2006, 27(6): 94-101.

[14] HONG Z, YI Z, L C Y,et al. Formal specification and verification of an extended security policy model for database systems[A]. Trusted Infrastructure Technologies Conference[C]. 2008. 132-141.

[15] SANDHU R S, COYNE E J, FEINSTEIN H L,et al. Role-based access control models[J]. Computer, 1996, 29(2): 38-47.

[16] HE Y Z, HAN Z, FU H,et al. The formal model of DBMS enforcing multiple security polices[J]. Journal of Software, 2010, 5(5): 514-521.