模式驅動的系統安全性設計的驗證*

鄭小宇，劉冬梅，杜益寧，周子健，邱玫媚，朱 鴻

(1.南京理工大學計算機科學與工程學院，江蘇 南京 210094；2.Oxford Brookes大學工程、計算和數學學院，英國 牛津 OX33 1HX)

1 引言

隨著系統安全性研究的日益深入和安全性技術的不斷成熟，研究人員提出了一組可以廣泛使用的安全設計模式[1]，以模式組合為基本特征的系統安全性工程已經逐漸成熟[2-4]。其基本思想是，根據實際應用場景中的身份驗證、訪問控制、數據完整性等安全需求，開發人員識別適用的安全模式，并將這些模式進行組合，形成整個系統的安全解決方案。通常，整個系統的安全解決方案包括多種安全機制，每個機制又可能由多個適合不同應用場景和條件的模式組成。因此，系統的安全性解決方案往往是許多模式的組合。由于系統安全性需求的復雜性和安全機制之間關系的復雜性，是否正確地選擇了安全機制、是否正確地使用了實現安全機制的模式、是否正確地將模式組合在一起以達到安全機制的功能等已成為安全性工程亟待解決的問題。針對這些問題，本文提出一個以代數規約為基礎的安全解決方案的設計和驗證方法。

目前，對安全解決方案進行驗證的主要思路是先將UML模型轉換成通信演算系統CCS(Calculus of Communicating Systems)[5]、Petri網和代數規約[6]、Alloy[7]等形式化規約，再使用模型檢測工具進行驗證。這類方法能夠較好地驗證單個安全模式是否滿足給定的安全需求，但缺少對模式組合細節的描述，難以驗證組合的正確性。雖然也可將系統的安全解決方案看做一個整體，應用這些方法來驗證系統的安全性，但是系統的規模和復雜度限制了這些方法的實用性，而且當發現錯誤時難以迅速定位缺陷。此外，模型檢測工具只能用于驗證模型屬性，無法進一步對系統實現進行安全性測試。

代數規約是一種支持自動化軟件測試的形式化方法，已被廣泛應用于面向對象的軟件、軟件構件、Web服務描述和測試中[8 - 10]。大量案例研究表明[11 - 13]，相對于其他形式化方法，代數規約具有簡短精確、易學易理解、高度模塊化等特點，更適合描述復雜的系統。文獻[14]提出了代數規約的組合方法，使用由抽象規約和實現規約組成的雙元結構描述服務組合，其中抽象規約描述服務組合結果的需求，實現規約描述如何將已知服務組合在一起。文獻[14]還闡明了如何用已知服務的代數規約和組合描述的雙元結構形式化地證明服務組合的正確性。本文中的案例表明，該雙元結構也適用于描述安全模式的組合，其中抽象規約描述系統的安全需求，實現規約描述安全解決方案中如何將安全模式進行組合以滿足需求。此外，本文在已有工作的基礎上，進一步研究對代數規約組合的自動驗證，應用模型檢測工具自動分析并驗證安全解決方案規約的正確性。

本文提出的方法可以概括為4個步驟:(1)首先使用模塊化設計思想對安全解決方案的結構進行分解，確定方案中包含的基本模塊和模塊間的依賴關系，以及各個模塊所使用的模式。(2)使用代數規約語言以代數為基礎的面向服務的形式化語言SOFIA(Service-Oriented Formalism In Algebras)描述每個基本模塊中包含的數據結構和操作，確定模塊是如何將模式實例化的，并驗證基本模塊的形式化規約是否滿足安全需求。(3)使用SOFIA抽象規約和實現規約分別描述組合模塊的對外功能和內部實現，并驗證模塊是否正確組合了其使用的模式且滿足安全需求。(4)通過基于代數規約的自動測試檢查系統實現的正確性。由于篇幅所限，本文僅討論安全性的形式化驗證，對于自動測試的研究將另文報告。

2 系統安全性設計與驗證流程

如圖1所示，模式驅動的系統安全性建模和驗證流程包括設計流程、形式化建模流程和驗證流程。

Figure 1 Pattern-driven system security design and verification flow圖1 模式驅動的系統安全性設計和驗證流程

設計流程根據安全性需求將安全解決方案分解為相對獨立的模塊，并確定各個模塊使用的安全解決方案設計模式，然后結合模塊間的相互關系構造方案的設計結構圖，采用拓撲排序確定模塊的建模和驗證順序。

形式化建模流程根據設計方案中使用的安全模式構造各個基本模塊的代數規約，然后使用抽象規約和實現規約組成的雙元結構描述組合模塊。

驗證流程將SOFIA語言書寫的代數規約轉換成Alloy語言的規約后，依次驗證基本模塊和組合模塊規約的正確性。對于基本模塊，需要驗證其是否滿足公理中定義的功能和安全需求；對于組合模塊，首先驗證其是否正確組合了使用的安全模式，然后驗證模塊是否滿足抽象規約公理中定義的安全需求。

3 安全模式及其代數歸約

通過代數規約對安全模式進行建模，有助于進一步分析模式中包含的數據、操作及安全需求，從而為模式驅動的系統安全性建模奠定基礎。分析現有的安全模式文檔[15]發現，安全模式主要包含模式中使用的數據結構和操作語義，同時包括模式的安全需求、類型和適用平臺等相關信息，因此可以使用四元組表示安全模式，其定義如下：

定義1(安全模式(Security Pattern)) 安全模式描述了特定應用場景下的安全需求以及相應的解決方案，使用四元組〈S,O,R,I〉表示，其中：

S表示安全模式中使用的數據類型，描述模式的靜態結構。

O表示安全模式中的操作及其語義，描述模式的動態行為。

R表示安全模式要實現的安全需求，通常使用一組操作序列構成的應用場景對其進行描述。

I表示安全模式的相關信息。I=〈C,P,D〉，其中C表示安全模式的類型，如身份認證、訪問控制等；P表示安全模式的適用平臺，大多數模式獨立于平臺，少部分模式依賴特定平臺；D表示該模式依賴的其他模式。

根據上述定義，使用SOFIA語言描述安全模式的主要結構，構建安全模式的代數規約。代數規約語言SOFIA將模式和S中的每個數據類型定義為一個類子(Sort)，類子包括基調(Signature)和公理(Axiom)2個部分，其中基調描述類型中的數據成員和O中的操作集合，包括各操作的操作名和輸入輸出參數。公理描述O中的操作行為和模式安全需求R。模式信息I用于輔助開發人員選擇合適的模式，與形式化驗證無關，使用自然語言描述。

安全模式的代數規約使用三元組〈S,Σ,Ax〉表示[16]，其中，S=〈S,?,>〉表示規約包含的類子集合及其上的擴展和依賴關系，Σ表示基調集合，Ax表示公理集。本節在文獻[16]定義的基礎上將規約中的公理集Ax細分為描述數據類型約束的公理集Axattr，描述單個操作語義的公理集Axop以及描述操作組合序列(即應用場景中的安全需求)的公理集Axseq，即Ax=Axattr∪Axop∪Axseq。

下面以基于會話的身份認證模式Session中的創建和驗證會話操作為例，說明如何使用代數規約描述安全模式。相關數據類型S包含會話數據和數據庫，安全需求R為“通過Session能夠獲取登錄用戶信息”，可使用“用戶創建Session后查詢該Session，結果中的用戶ID與創建時的用戶ID一致”的應用場景進行描述。

SpecSession;

usesInteger,String;

Attrid:String;uid:Integer;created:Integer;

End

SpecSessDB;

usesListOfSession;

Attrdatas:ListOfSession;

End

SpecSessReturn;

usesSession,SessDB;

Attrsess:Session;sdb:SessDB;

End

SpecSessM;

usesString,Integer,Bool,Expire,SessReturn,…;

Retr

verify_sess(SessDB,String,Integer):Bool;

get_sess(SessDB,String,Integer):Session;

Tran

create_sess(SessDB,Integer,Integer):SessReturn;

Axiom

Foralls:SessM,util:UtilOp,e:Expire,sid:String,

t:Integer,sdb:SessDBthat

letsess=util.getDataById(sid,sdb)in

s.verify_sess(sdb,sid,t) = true;

ifsess〈〉null,sess.last+e.expire>=t;//公理1

s.verify_sess(sdb,sid,t) = false;

ifs= null;//公理2

s.verify_sess(sdb,sid,t) = false;

ifsess.last+e.expire

End

End

Foralls:SessM,util:UtilOp,e:Expire,sid:String,

sdb:SessDB,u,t:Integerthat

letsr=s.create_sess(sdb,u,t)in

sr.sess.uid=u;//公理4

sr.sess.created=t;//公理5

sr.sdb=util.union(sdb,sr.sess);//公理6

End

End

Foralls:SessM,sid:String,sdb1,sdb2:SessDB,

u,t:Integerthat

s.create_sess(sdb1,u,t);get_sess(sdb2,sid,t).uid=u;

ifsdb2=s.create_sess(sdb1,u,t).sdb;

sid=s.create_sess(sdb1,u,t).sess.id;//公理7

End

End

上述規約中的類子集合S包括模式類子SessM，數據庫SessDB、會話Session和操作結果SessReturn，其中SessM類子的基調定義了驗證操作verify_sess、創建操作create_sess和查詢操作get_sess，公理集合中的公理1～公理3描述驗證操作，表示僅當Session不為空且未過期時才能通過驗證并返回true，否則返回false；公理4～公理6則描述創建操作，表示新創建的Session中保存當前用戶的ID和創建時間t；Axseq中的公理7則描述了上述應用場景，表示用戶依次調用創建和查詢操作，如果調用查詢操作時提供的Session ID等于創建Session時返回的Session ID，則返回Session中的用戶ID與當前用戶一致。

4 安全解決方案的設計和建模

4.1 安全解決方案的模塊化設計

設計安全解決方案的主要思路是根據系統安全需求確定方案應實現的功能，將其分解為一系列模塊，并確定模塊使用的安全模式，為形式化建模打下基礎。在模塊化設計的過程中，基本模塊粒度過大往往會導致模塊內部仍存在復雜的結構，從而加大建模的難度；而粒度過小則需要將模塊進行多次組合，使建模流程變得繁瑣。針對這一問題，本文根據現有軟件模塊化設計研究[17,18]給出的策略設計安全解決方案，并分析各個模塊對外提供的接口和需要調用的接口，確定模塊間的依賴關系，從而構造安全解決方案的設計結構圖，其定義如下：

定義2(安全解決方案的設計結構圖(Structure Diagram of Security Solution)) 一個安全解決方案的設計結構圖G=〈N,E,l〉使用L(L≥2)層有向無環圖表示，其中:

N表示節點集，N=Ns∪Nm，其中Ns表示基本模塊節點集合，Nm表示組合模塊節點集合。

E表示邊集，E=Ed∪Ec,Ed中的邊表示模塊間的依賴關系，使用帶箭頭的實線表示;Ec中的邊表示模塊間的組合關系，使用帶菱形的實線表示，Ec?(Ns×Nm)∪(Nm×Nm)。對于邊(n,n′)∈Ec，稱n是n′的一個子模塊。

l表示節點層次標識函數n→{i|0≤i≤L-1}，基本模塊節點ns的層數l(ns)=0;組合模塊節點nm的層數l(nm)=max(l(Nsub))+1，其中Nsub為nm的子模塊集合。

圖2以一個基于區塊鏈的醫療數據管理方案DataM為例，給出了該安全解決方案的設計結構。該方案的安全需求為僅允許用戶對其擁有的數據或具有訪問權限的數據進行操作，當數據所有者為多個用戶時，由這些用戶共同決定是否授予其他用戶訪問權限。因此安全解決方案需實現數據操作、訪問控制和共識機制等功能，劃分為DataOp、DataAC和Vote 3個子模塊，其中DataOp模塊無需使用安全模式，Vote模塊使用投票模式；然后進一步分析DataAC包含的2種訪問控制機制，將其劃分為基于數據所有者的Owner和基于策略的Policy 2個子模塊；最后根據模塊接口的相互調用確定依賴關系，完成設計結構圖的構造。

Figure 2 Structure diagram of security solution design圖2 安全解決方案的設計結構圖

設計結構圖同時反映出模塊的建模和驗證順序，由定義1可知，圖中節點的入度表示該模塊依賴和組合的其他模塊數量，因此采用拓撲排序思路優先遍歷層數較低的節點生成模塊序列，如DataOp→Owner→Policy→Vote→DataAC→DataM。

4.2 安全解決方案的建模

安全解決方案的建模流程包括2個主要步驟：首先根據設計結構圖給出的建模順序依次將各個基本模塊使用的安全模式實例化，然后使用抽象規約和實現規約分別描述組合模塊的對外功能和內部實現。

安全模式中往往使用抽象數據類型，與實際應用中的數據類型存在一定差異，其代數規約無法直接用于安全解決方案的建模。因此，需要對基本模塊使用的安全模式進行實例化，將模式規約中描述抽象數據的類子替換為描述應用場景中具體數據的類子，并更新使用這些類子的操作和公理。實例化操作得到的基本模塊代數規約與安全模式的代數規約相同，使用三元組〈S,Σ,x〉表示。

以基于數據所有者的訪問控制模式Owner為例，若使用該模式構建病歷管理模塊，其包含的抽象數據類型SOData需要實例化為病歷數據MedicalCase，將owner屬性更名為patient_id，同時新增了就診時間visit_time和就診醫院hospital等屬性，實例化前后的類子規約如下所示：

SpecSOData; //實例化前的類子SOData

usesInteger;

Attr

owner:Integer;

End

SpecMedicalCase;//實例化后的類子MedicalCase

usesInteger,Date,String;

Attr

patient_id:Integer;

visit_time:Date;

hospital:String;

End

實例化后的MedicalCase數據類型使用patient_id屬性存儲病歷所有者，因此驗證數據所有者操作中的公理也更新為使用patient_id屬性與當前用戶ID進行比較,相關公理如下所示：

//實例化前的公理

o.owner_verifier(db,uid,i) = true,ifd.owner=uid;

//實例化后的公理

o.owner_verifier(db,uid,i) = true,ifd.patient_id=ac.id,…;

以4.1節中的DataM模塊為例，該模塊為包含DataAC、DataOp和Vote 3個子模塊的組合模塊，其代數規約包括抽象規約DataM和實現規約DataMImp 2部分。模塊中的數據更新操作update的相關公理如下所示：

dac.update(ac,s,did,db,pdb).content=s,

ifdac.access_verifier(ac,did,2,pdb) = true;∥axA

dac.update(ac,s,did,db,pdb) =dac.dop.update(ac,s,did,db),

ifdac.access_verifier(ac,did,2,pdb) = true;∥axI

抽象規約中的公理axA表示若當前用戶通過權限驗證，則返回更新后的數據內容；實現規約中的公理axI則表示首先調用DataAC中的權限驗證操作，若驗證通過再調用DataOp中的數據更新操作實現更新功能。

5 代數規約的轉換和驗證

本節將SOFIA規約轉換為Alloy規約后，使用模型檢測工具[19]依次驗證方案中的基本模塊是否滿足安全需求，以及組合模塊是否正確組合了其子模塊且滿足安全需求。其中SOFIA規約中描述數據類型的類子對應為Alloy規約中的signature，類子的基調對應為Alloy規約中的enum或field。對于區塊鏈應用中的基本模塊，其SOFIA規約中描述單個操作的公理定義了各個操作的行為，對應為Alloy規約的謂詞；而描述操作序列的公理定義了模塊在具體應用場景中的安全需求，對應為Alloy規約的斷言。對于組合模塊，實現規約公理必須正確實現抽象規約公理中定義的模塊行為，因此對應為Alloy規約的謂詞；而抽象規約中的公理對應為斷言，用于驗證模塊使用的安全模式是否被正確組合和模塊是否滿足安全需求。接下來將在此基礎上分析2種規約間的映射關系并構造轉換規則，從而將區塊鏈應用的SOFIA規約轉換為Alloy規約。

5.1 基本模塊的規約轉換

基本模塊的Alloy規約使用七元組〈S,M,Enum,F,O,P,A〉表示，定義如下：

定義3(基本模塊的Alloy規約(Alloy Specification of Basic Module)) 使用Alloy語言對基本模塊進行形式化描述，所得規約是一個七元組〈S,M,Enum,F,O,P,A〉，其中：

S表示基本模塊中的類和類之間的繼承關系。S=〈S,?〉，其中S表示規約中signature的集合，?表示S上的擴展(繼承)關系。

M(Members)表示類中的數據成員，M={Ms|s∈S}，Ms表示s中的數據成員集合。

Enum(Enumeration)表示模式中的枚舉類型集合。

F(Fact)表示模塊中數據類型應滿足的約束，F={Fs|s∈S}，其中Fs表示對s中數據成員的約束。對于每個f∈F，f=〈fV,fp〉,其中fV為變量集合，fp為一個約束條件。

O(Operation)表示模塊中的操作集合。對于每個o∈O，o=〈φ,In,Out〉分別表示操作名和操作的輸入輸出參數集合。

P(Predicate)表示模塊中操作的行為。P={Po|o∈O}，其中Po表示對操作o的謂詞約束集合。

A(Assert)表示模塊的安全需求。對于每個a∈A,a=〈aV,ap〉，其中aV表示斷言中使用的變量集合，ap=〈seq,ae〉表示斷言中的謂詞約束，seq表示謂詞中包含的操作序列，ae表示執行操作序列后應成立的等式。

根據上述定義，分析2種規約之間的映射關系，進而給出以下的轉換規則：

規則1將SOFIA規約中的S轉換為Alloy規約中的S。其中，SOFIA規約的類子集合S和擴展關系?轉換為Alloy規約的signature集合S和擴展關系?，而使用關系在Alloy規約中沒有顯式定義，無需轉換。

規則2對于SOFIA規約中每個類子的基調單元Σs∈Σ，將其中的常操作子(Const)加入Alloy規約的枚舉類型集合Enum，屬性操作子(Attr)轉換為Alloy規約中對應signature的數據成員Ms∈M，其它操作子(Retr&Tran)則轉換為Alloy規約中的一個操作o∈O。

規則3對于SOFIA規約中每個描述數據類型約束的公理axattr=〈V,e〉，轉換為Alloy規約中的f∈F，其中變量集V轉換為fV，條件等式e轉換為fp。

規則4對于SOFIA規約中每個描述單個操作的公理axop=〈V,e〉，將公理中的條件等式e轉換為Alloy規約中對應操作o的一條謂詞約束po∈Po，其中變量為操作o的輸入輸出參數。

規則5對于SOFIA規約中每個描述操作序列的公理axseq=〈V,e〉，轉換為Alloy規約中的一個斷言a∈A，其中變量集V轉換為aV，條件等式e轉換為seq?ae。

根據上述規則構造基本模塊的規約轉換算法，表1給出了算法中使用的符號及描述。

Table 1 Symbols and descriptions in algorithm 1

算法1基本模塊的規約轉換算法

輸入:基本模塊SOFIA規約〈S,Σ,Ax〉。

輸出:基本模塊Alloy規約〈S,M,Enum,F,O,P,A〉。

1.foreachs∈Sdo/* 遍歷SOFIA規約的類子，根據規則1和2進行轉換 */

2.S←S+s;?←?+?S;/* 轉換類子s及其擴展關系 */

5.endfor

6.S=〈S,?〉;

7.foreachax∈Axdo//遍歷公理集合

8.ifax∈Axattrthen/*根據規則3將描述數據約束的公理轉換為fact*/

9.fV=ax.v;fp=ax.e;F←F+〈fV,fp〉;/*將轉換得到的fact加入集合F*/

10.endif

11.ifax∈Axopthen/* 根據規則4將描述單個操作的公理轉換為一條謂詞約束 */

12.o=∏op(ax);Po←Po+ax.e;/* 將公理等式加入對應操作o的謂詞集合 */

13.endif

14.ifax∈Axseqthen/* 根據規則5將描述操作序列的公理轉換為斷言 */

15.seq=∏oplist_seq(ax);aV=ax.v;ae=ax.e;/* 獲取公理的操作、變量和等式*/

16.foreacho∈seqdo/* 遍歷操作集合，將操作的輸出變量加入變量集 */

17.aV←aV+∏out(o);

18.endfor

19.A←A+〈aV,〈seq,ae〉〉;/*將轉換得到的斷言加入集合A*/

20.endif

21.endfor

22.foreacho∈Odo/* 公理處理完成后，遍歷操作集合 */

23.P←P+Po/* 將遍歷到的操作的謂詞加入集合P*/

24.endfor

25.return〈S,M,Enum,F,O,P,A〉

5.2 組合模塊的規約轉換

組合模塊使用其子模塊定義的數據類型，因此其Alloy規約不包含對數據類型的描述，使用三元組表示，定義如下：

定義4(組合模塊的Alloy規約(Alloy Specification of Composition Module)) 使用Alloy語言對組合模塊進行形式化描述，所得規約是一個三元組〈O,P,A〉，其中：

O(Operation)表示模塊中的操作集合。

P(Predicate)表示模塊中操作的內部實現。P={Po|o∈O}，其中Po表示描述操作o內部實現的謂詞集合。

以下規則從組合模塊的SOFIA規約中提取出定義操作的基調集合、描述操作內部實現和功能特性的公理集合，以及描述操作序列的公理集合，并將其轉換為Alloy規約：

規則6將抽象規約的基調集合ΣA加入Alloy規約的操作集合O。

規則9將實現規約的基調集合ΣI加入Alloy規約的操作集合O。

規則10對于實現規約的每條公理axI=〈V,e〉，將公理中的條件等式e轉換為Alloy規約中對應操作o的一條謂詞約束po∈Po，其中變量為操作o的輸入輸出參數。

根據上述規則給出組合模塊的規約轉換算法，算法的主要思路是依次處理抽象規約的基調和公理集，分別轉換為Alloy規約的操作集合和斷言集合，然后將實現規約的公理轉換為Alloy規約中對應操作的謂詞。除表1中定義的符號外，該算法還需要使用∏op_imp(axI)和∏oplist_abs(axA)2個符號，其中∏op_imp(axI)表示實現規約公理axI的對應操作，∏oplist_abs(axA)表示抽象規約公理axA包含的操作集合。

算法2組合模塊的規約轉換算法

輸入:組合模塊SOFIA規約，包括實現規約SI和抽象規約SA。

輸出:組合模塊Alloy規約〈O,P,A〉。

1.O←O+ΣA/* 將抽象規約的基調單元加入操作集合O*/

2.foreachax∈AxA do//遍歷抽象規約的公理集

3.seq=∏oplist_abs(ax);aV=ax.v;e=ax.e;/*獲取公理的操作集、變量集和等式*/

4.foreacho∈seqdo/* 遍歷操作集合，將操作的輸出變量加入變量集 */

5.aV←aV+∏out(o);

6.endfor

9.elseAseq←Aseq+〈aV,〈seq,e〉〉;/* 否則加入描述安全需求的集合Aseq*/

10.endif

11.endfor

12.foreachax∈AxIdo//遍歷實現規約的公理集

13.o=∏op_imp(ax);Po←Po+ax.e;/* 將公理等式加入對應操作o的謂詞集合*/

14.endfor

15.foreacho∈Odo/* 實現公理處理完成后，遍歷操作集合 */

17.endfor

18.A=Aop+Aseq;

19.return〈O,P,A〉

5.3 安全解決方案的驗證

安全解決方案的規約中往往存在操作的前后置條件定義錯誤、模塊間的操作調用錯誤等缺陷，導致方案無法滿足安全需求。本節使用模型檢測工具Alloy Analyzer分析規約中的謂詞和斷言，檢查規約中是否存在上述缺陷，從而對規約的正確性進行驗證。

規約的驗證過程包括2個階段，第1階段驗證基本模塊是否滿足安全需求，第2階段驗證組合模塊是否正確組合了其子模塊且滿足安全需求。下面分別介紹2個驗證階段的主要步驟。

在第1階段中，對于方案中的每個基本模塊，首先執行由謂詞定義的操作，以檢查該操作的前后置條件是否與模塊中的其他公理存在相互矛盾。然后將模塊中的斷言改寫為謂詞，其中斷言包含的全局變量被轉換為謂詞的變量，斷言等式被轉換為謂詞等式，改寫示例如下所示：

assertassertion{//改寫前的斷言

allv1:type1,v2:type2 |op[v1,v2] ?v1=v2

}

predpredicate[v1:type1,v2:type2] {/*改寫后的謂詞*/

op[v1,v2] =>v1=v2

}

改寫后的謂詞用于檢查斷言中定義的操作序列和需求是否存在矛盾，最后驗證各個斷言是否成立，以檢查模塊是否滿足斷言中定義的安全需求。

第2階段中對組合模塊的驗證包括以下3個步驟，其中步驟1和步驟2用于驗證模塊組合的正確性，步驟3用于驗證模塊是否滿足需求。

步驟1驗證模塊中各個謂詞的可滿足性。

組合模塊中的謂詞定義了模塊中的操作如何通過調用其子模塊中的的操作實現相應功能，如果謂詞中的操作調用是正確的，則謂詞應當是可滿足的，即能夠生成滿足謂詞的實例。因此，對于模塊中每個操作o對應的謂詞，使用模型檢測工具生成滿足謂詞的實例。如果無法生成實例，則表明操作調用存在錯誤。

步驟2驗證模塊中各個操作的功能特性。

步驟3驗證應用場景中的安全需求。

組合模塊中描述操作序列的斷言定義了模塊在應用場景中應滿足的安全需求。因此，對于模塊中每個描述操作序列的斷言，首先將斷言改寫為謂詞并生成實例，若能夠生成實例，則表明斷言中不存在相互矛盾。然后在給定范圍內生成違背斷言的反例，若無法生成反例，則表明斷言在給定范圍內成立，即模塊滿足該斷言中定義的安全需求。

根據文獻[20]中案例研究的結論，較小范圍的實例能夠檢測出絕大多數的缺陷，因此可以認為經過上述步驟驗證的斷言對所有實例都成立。

6 案例研究

6.1 案例描述

本文以4.1節的安全解決方案DataM為研究案例，該方案由基本模塊DataOp、Vote和組合模塊DataAC組成，因此其SOFIA規約包含Basic、UtilOp、DataOp、Owner、Policy、Vote、DataAC、DataACImp、DataM、DataMImp共10個規約包[14]，規約結構如圖3所示。

Figure 3 Specifications structure of security solution DataM圖3 安全解決方案DataM規約結構

規約中的Basic描述方案中使用的基本數據類型；UtilOp描述了一些公共操作，如集合操作、查詢操作等；Owner、Policy、Vote、DataOp分別是數據所有者驗證、訪問策略管理、投票管理以及數據操作規約包；DataAC和DataACImp分別是訪問權限驗證的抽象規約包和實現規約包；DataM和DataMImp分別是數據管理方案的抽象規約包和實現規約包。對應的Alloy規約將組合模塊的抽象規約和實現規約合并為一個模塊，其余部分的結構與SOFIA規約基本相同。

由于Basic、UtilOp、DataOp中不包含數據安全相關的操作，因此本案例主要分析Owner、Policy等7個規約包及其轉換后的Alloy規約模塊。SOFIA規約中的類子、操作和公理數量及對應Alloy規約中的signature(表中簡寫成sig)、fact、謂詞和斷言數量見表2。

Table 2 Statistics of specifications

6.2 實驗結果和分析

將Alloy規約中具有相同操作序列的斷言合并后，首先使用Alloy Analyzer分析Owner、Policy和Vote基本模塊中的謂詞和斷言，驗證基本模塊的正確性，然后執行DataAC和DataM規約中謂詞描述的操作并驗證描述單個操作和安全需求的斷言，從而驗證組合的正確性和模塊的安全性。以DataM規約為例，其合并斷言后的Alloy規約中包含4個謂詞集合、4個描述單個操作的斷言集合和10個描述安全需求的斷言集合，驗證結果顯示描述操作的謂詞及斷言改寫的謂詞均能生成實例，且斷言均無法生成反例，表明該方案能夠滿足定義的安全需求。

接下來向方案的SOFIA規約中注入單缺陷，再轉換為Alloy規約進行驗證。其中，注入缺陷的位置為基本模塊規約和組合模塊實現規約中描述單個操作的公理，此類公理被轉換為Alloy規約中描述操作的謂詞，因此能夠通過驗證模塊中的斷言檢測注入的缺陷。注入缺陷后的規約不能存在語法錯誤，否則將無法進行規約轉換和驗證。

注入缺陷的類型包括替換公理中的常量、變量和操作，添加或刪除公理，刪除公理中的if條件等文獻[21]給出的代數規約常見缺陷。這些缺陷往往改變了模式中部分操作的前后置條件，或改變了模式間的操作調用關系，導致模式無法實現預期的安全需求。以下面的公理為例：

pr.p.right=op;//公理1

pr.p.right=uid; //缺陷公理1(替換變量)

//公理2

dac.getdata(uid,did,db,pdb) =dac.dop.getdata(db,did);

//缺陷公理2(替換操作)

dac.getdata(uid,did,db,pdb) =dac.dop.deldata(did);

公理1為Policy規約中描述添加策略操作的公理，表示新策略的權限等級right等于輸入參數op。注入缺陷后變量op被替換為uid，即用戶id，導致添加策略操作出現錯誤。公理2為DataMImp規約中描述數據查詢操作的公理，表示調用DataOp模塊中的getdata操作查詢數據。注入缺陷后getdata操作被替換為刪除數據操作deldata，導致模式間的調用出錯。

根據注入缺陷位置的不同，驗證方法可分為2類。對于基本模塊缺陷，首先執行存在缺陷的操作謂詞，再驗證該模塊中的斷言；對于組合模塊缺陷，首先執行存在缺陷的操作謂詞，再依次驗證該模塊中描述單個操作的斷言和安全需求的斷言。若驗證過程中描述操作的謂詞或由斷言改寫的謂詞無法生成實例，以及斷言成功生成反例，則表明該方法能夠發現缺陷，否則無法發現缺陷。表3給出了注入150個單缺陷后的驗證結果，即發現的缺陷數量與注入缺陷總數之比。

Table 3 Verification results of defect injection

分析表3中給出的驗證結果，可得出以下結論：

(1)上述驗證方法能夠檢測出規約中的大部分缺陷。表3的驗證結果顯示，在注入的150個缺陷中有12個缺陷未被檢測出。進一步分析未被檢測出的缺陷發現，其中5個缺陷沒有改變操作的行為，如替換一個對操作結果沒有影響的常量，或添加一條if條件永不成立的公理。以Vote模塊中的部分公理為例，這些公理表示根據投票屬性policyOp執行權限授予、更新或解除3種操作。policyOp為枚舉類型，僅包含這3種操作，而缺陷公理的if條件表示policyOp不為這3種操作中的任何一種，因此這個條件不可能成立，缺陷公理對操作沒有影響。

auth_grant_sys(pdb,v.user,v.data,v.right),ifv.op=grant;

auth_update_sys(pdb,v.policy,v.right),ifv.op=update;

auth_revoke_sys(v.policy,pdb),ifv.op=revoke;

//缺陷公理

…,ifv.op〈〉grant,v.op〈〉update,v.op〈〉revoke;

(2)模塊中的公理必須正確、完整地描述安全需求。若公理缺少對部分應用場景的描述，則無法檢測出這些應用場景中的缺陷，未檢測出的7個缺陷屬于此類。如Policy模塊的授權操作中包含一個條件判斷，當用戶沒有權限或權限較低時才執行操作，以防止重復授權。注入的缺陷刪除了這一條件，但由于模塊中的公理沒有描述重復授權的場景，因此無法檢測出該缺陷。

實驗結果和上述分析表明，本文方法能夠有效地檢測出安全模式中的缺陷，但仍然存在一些問題。該方法只能驗證方案和定義的安全需求是否一致，而不能發現安全需求定義本身存在的漏洞。此外，組合模塊中描述安全需求的斷言往往包含3個以上的操作，導致驗證時生成的反例較為復雜，如DataM規約中的反例往往包含40個以上的變量，增加了在組合模塊中定位缺陷的難度。

7 結束語

本文提出了一個模式驅動的系統安全性設計與驗證方法，首先使用模塊化思想設計安全解決方案并確定方案中各個模塊使用的安全模式，然后使用SOFIA語言對模塊中包含的數據結構和操作語義進行建模，最后將SOFIA規約轉換為Alloy規約進行安全性驗證。案例研究表明，該方法能夠有效地驗證安全解決方案設計的正確性。下一步的工作將使用SOFIA語言對常用的安全模式進行建模，構建安全模式庫，并將該方法應用到一個完整的區塊鏈醫療系統的開發過程中，結合模型檢測和自動測試2種方式驗證該系統，以提高區塊鏈應用的安全性。