模式驅(qū)動的系統(tǒng)安全性設計的驗證*

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

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

1 引言

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

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

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

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

2 系統(tǒng)安全性設計與驗證流程

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

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

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

形式化建模流程根據(jù)設計方案中使用的安全模式構(gòu)造各個基本模塊的代數(shù)規(guī)約，然后使用抽象規(guī)約和實現(xiàn)規(guī)約組成的雙元結(jié)構(gòu)描述組合模塊。

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

3 安全模式及其代數(shù)歸約

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

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

S表示安全模式中使用的數(shù)據(jù)類型，描述模式的靜態(tài)結(jié)構(gòu)。

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

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

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

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

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

下面以基于會話的身份認證模式Session中的創(chuàng)建和驗證會話操作為例，說明如何使用代數(shù)規(guī)約描述安全模式。相關(guān)數(shù)據(jù)類型S包含會話數(shù)據(jù)和數(shù)據(jù)庫，安全需求R為“通過Session能夠獲取登錄用戶信息”，可使用“用戶創(chuàng)建Session后查詢該Session，結(jié)果中的用戶ID與創(chuàng)建時的用戶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

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

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

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

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

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

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

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

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

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

Figure 2 Structure diagram of security solution design圖2 安全解決方案的設計結(jié)構(gòu)圖

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

4.2 安全解決方案的建模

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

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

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

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

usesInteger;

Attr

owner:Integer;

End

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

usesInteger,Date,String;

Attr

patient_id:Integer;

visit_time:Date;

hospital:String;

End

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

//實例化前的公理

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

//實例化后的公理

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

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

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

抽象規(guī)約中的公理axA表示若當前用戶通過權(quán)限驗證，則返回更新后的數(shù)據(jù)內(nèi)容；實現(xiàn)規(guī)約中的公理axI則表示首先調(diào)用DataAC中的權(quán)限驗證操作，若驗證通過再調(diào)用DataOp中的數(shù)據(jù)更新操作實現(xiàn)更新功能。

5 代數(shù)規(guī)約的轉(zhuǎn)換和驗證

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

5.1 基本模塊的規(guī)約轉(zhuǎn)換

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

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

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

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

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

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

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

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

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

根據(jù)上述定義，分析2種規(guī)約之間的映射關(guān)系，進而給出以下的轉(zhuǎn)換規(guī)則：

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

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

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

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

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

根據(jù)上述規(guī)則構(gòu)造基本模塊的規(guī)約轉(zhuǎn)換算法，表1給出了算法中使用的符號及描述。

Table 1 Symbols and descriptions in algorithm 1

算法1基本模塊的規(guī)約轉(zhuǎn)換算法

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

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

1.foreachs∈Sdo/* 遍歷SOFIA規(guī)約的類子，根據(jù)規(guī)則1和2進行轉(zhuǎn)換 */

2.S←S+s;?←?+?S;/* 轉(zhuǎn)換類子s及其擴展關(guān)系 */

5.endfor

6.S=〈S,?〉;

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

8.ifax∈Axattrthen/*根據(jù)規(guī)則3將描述數(shù)據(jù)約束的公理轉(zhuǎn)換為fact*/

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

10.endif

11.ifax∈Axopthen/* 根據(jù)規(guī)則4將描述單個操作的公理轉(zhuǎn)換為一條謂詞約束 */

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

13.endif

14.ifax∈Axseqthen/* 根據(jù)規(guī)則5將描述操作序列的公理轉(zhuǎn)換為斷言 */

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〉〉;/*將轉(zhuǎn)換得到的斷言加入集合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 組合模塊的規(guī)約轉(zhuǎn)換

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

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

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

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

以下規(guī)則從組合模塊的SOFIA規(guī)約中提取出定義操作的基調(diào)集合、描述操作內(nèi)部實現(xiàn)和功能特性的公理集合，以及描述操作序列的公理集合，并將其轉(zhuǎn)換為Alloy規(guī)約：

規(guī)則6將抽象規(guī)約的基調(diào)集合ΣA加入Alloy規(guī)約的操作集合O。

規(guī)則9將實現(xiàn)規(guī)約的基調(diào)集合ΣI加入Alloy規(guī)約的操作集合O。

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

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

算法2組合模塊的規(guī)約轉(zhuǎn)換算法

輸入:組合模塊SOFIA規(guī)約，包括實現(xiàn)規(guī)約SI和抽象規(guī)約SA。

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

1.O←O+ΣA/* 將抽象規(guī)約的基調(diào)單元加入操作集合O*/

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

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//遍歷實現(xiàn)規(guī)約的公理集

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

14.endfor

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

17.endfor

18.A=Aop+Aseq;

19.return〈O,P,A〉

5.3 安全解決方案的驗證

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

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

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

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驗證模塊中各個謂詞的可滿足性。

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

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

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

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

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

6 案例研究

6.1 案例描述

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

Figure 3 Specifications structure of security solution DataM圖3 安全解決方案DataM規(guī)約結(jié)構(gòu)

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

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

Table 2 Statistics of specifications

6.2 實驗結(jié)果和分析

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

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

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

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規(guī)約中描述添加策略操作的公理，表示新策略的權(quán)限等級right等于輸入?yún)?shù)op。注入缺陷后變量op被替換為uid，即用戶id，導致添加策略操作出現(xiàn)錯誤。公理2為DataMImp規(guī)約中描述數(shù)據(jù)查詢操作的公理，表示調(diào)用DataOp模塊中的getdata操作查詢數(shù)據(jù)。注入缺陷后getdata操作被替換為刪除數(shù)據(jù)操作deldata，導致模式間的調(diào)用出錯。

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

Table 3 Verification results of defect injection

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

(1)上述驗證方法能夠檢測出規(guī)約中的大部分缺陷。表3的驗證結(jié)果顯示，在注入的150個缺陷中有12個缺陷未被檢測出。進一步分析未被檢測出的缺陷發(fā)現(xiàn)，其中5個缺陷沒有改變操作的行為，如替換一個對操作結(jié)果沒有影響的常量，或添加一條if條件永不成立的公理。以Vote模塊中的部分公理為例，這些公理表示根據(jù)投票屬性policyOp執(zhí)行權(quán)限授予、更新或解除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模塊的授權(quán)操作中包含一個條件判斷，當用戶沒有權(quán)限或權(quán)限較低時才執(zhí)行操作，以防止重復授權(quán)。注入的缺陷刪除了這一條件，但由于模塊中的公理沒有描述重復授權(quán)的場景，因此無法檢測出該缺陷。

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

7 結(jié)束語

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