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

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

1 引言

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

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

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

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

2 系統(tǒng)安全性設(shè)計(jì)與驗(yàn)證流程

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)定義了驗(yàn)證操作verify_sess、創(chuàng)建操作create_sess和查詢操作get_sess，公理集合中的公理1～公理3描述驗(yàn)證操作，表示僅當(dāng)Session不為空且未過期時(shí)才能通過驗(yàn)證并返回true，否則返回false；公理4～公理6則描述創(chuàng)建操作，表示新創(chuàng)建的Session中保存當(dāng)前用戶的ID和創(chuàng)建時(shí)間t；Axseq中的公理7則描述了上述應(yīng)用場景，表示用戶依次調(diào)用創(chuàng)建和查詢操作，如果調(diào)用查詢操作時(shí)提供的Session ID等于創(chuàng)建Session時(shí)返回的Session ID，則返回Session中的用戶ID與當(dāng)前用戶一致。

4 安全解決方案的設(shè)計(jì)和建模

4.1 安全解決方案的模塊化設(shè)計(jì)

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

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

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

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

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

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

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

設(shè)計(jì)結(jié)構(gòu)圖同時(shí)反映出模塊的建模和驗(yàn)證順序，由定義1可知，圖中節(jié)點(diǎn)的入度表示該模塊依賴和組合的其他模塊數(shù)量，因此采用拓?fù)渑判蛩悸穬?yōu)先遍歷層數(shù)較低的節(jié)點(diǎn)生成模塊序列，如DataOp→Owner→Policy→Vote→DataAC→DataM。

4.2 安全解決方案的建模

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

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

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

SpecSOData; //實(shí)例化前的類子SOData

usesInteger;

Attr

owner:Integer;

End

SpecMedicalCase;//實(shí)例化后的類子MedicalCase

usesInteger,Date,String;

Attr

patient_id:Integer;

visit_time:Date;

hospital:String;

End

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

//實(shí)例化前的公理

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

//實(shí)例化后的公理

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

以4.1節(jié)中的DataM模塊為例，該模塊為包含DataAC、DataOp和Vote 3個(gè)子模塊的組合模塊，其代數(shù)規(guī)約包括抽象規(guī)約DataM和實(shí)現(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表示若當(dāng)前用戶通過權(quán)限驗(yàn)證，則返回更新后的數(shù)據(jù)內(nèi)容；實(shí)現(xiàn)規(guī)約中的公理axI則表示首先調(diào)用DataAC中的權(quán)限驗(yàn)證操作，若驗(yàn)證通過再調(diào)用DataOp中的數(shù)據(jù)更新操作實(shí)現(xiàn)更新功能。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

規(guī)則5對于SOFIA規(guī)約中每個(gè)描述操作序列的公理axseq=〈V,e〉，轉(zhuǎn)換為Alloy規(guī)約中的一個(gè)斷言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進(jìn)行轉(zhuǎn)換 */

2.S←S+s;?←?+?S;/* 轉(zhuǎn)換類子s及其擴(kuò)展關(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將描述單個(gè)操作的公理轉(zhuǎn)換為一條謂詞約束 */

12.o=∏op(ax);Po←Po+ax.e;/* 將公理等式加入對應(yīng)操作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語言對組合模塊進(jìn)行形式化描述，所得規(guī)約是一個(gè)三元組〈O,P,A〉，其中：

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

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

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

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

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

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

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

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

輸入:組合模塊SOFIA規(guī)約，包括實(shí)現(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//遍歷實(shí)現(xiàn)規(guī)約的公理集

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

14.endfor

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

17.endfor

18.A=Aop+Aseq;

19.return〈O,P,A〉

5.3 安全解決方案的驗(yàn)證

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

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

在第1階段中，對于方案中的每個(gè)基本模塊，首先執(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

}

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

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

步驟1驗(yàn)證模塊中各個(gè)謂詞的可滿足性。

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

步驟2驗(yàn)證模塊中各個(gè)操作的功能特性。

步驟3驗(yàn)證應(yīng)用場景中的安全需求。

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

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

6 案例研究

6.1 案例描述

本文以4.1節(jié)的安全解決方案DataM為研究案例，該方案由基本模塊DataOp、Vote和組合模塊DataAC組成，因此其SOFIA規(guī)約包含Basic、UtilOp、DataOp、Owner、Policy、Vote、DataAC、DataACImp、DataM、DataMImp共10個(gè)規(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ù)所有者驗(yàn)證、訪問策略管理、投票管理以及數(shù)據(jù)操作規(guī)約包；DataAC和DataACImp分別是訪問權(quán)限驗(yàn)證的抽象規(guī)約包和實(shí)現(xiàn)規(guī)約包；DataM和DataMImp分別是數(shù)據(jù)管理方案的抽象規(guī)約包和實(shí)現(xiàn)規(guī)約包。對應(yīng)的Alloy規(guī)約將組合模塊的抽象規(guī)約和實(shí)現(xiàn)規(guī)約合并為一個(gè)模塊，其余部分的結(jié)構(gòu)與SOFIA規(guī)約基本相同。

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

Table 2 Statistics of specifications

6.2 實(shí)驗(yàn)結(jié)果和分析

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

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

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

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，導(dǎo)致添加策略操作出現(xiàn)錯(cuò)誤。公理2為DataMImp規(guī)約中描述數(shù)據(jù)查詢操作的公理，表示調(diào)用DataOp模塊中的getdata操作查詢數(shù)據(jù)。注入缺陷后getdata操作被替換為刪除數(shù)據(jù)操作deldata，導(dǎo)致模式間的調(diào)用出錯(cuò)。

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

Table 3 Verification results of defect injection

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

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

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)模塊中的公理必須正確、完整地描述安全需求。若公理缺少對部分應(yīng)用場景的描述，則無法檢測出這些應(yīng)用場景中的缺陷，未檢測出的7個(gè)缺陷屬于此類。如Policy模塊的授權(quán)操作中包含一個(gè)條件判斷，當(dāng)用戶沒有權(quán)限或權(quán)限較低時(shí)才執(zhí)行操作，以防止重復(fù)授權(quán)。注入的缺陷刪除了這一條件，但由于模塊中的公理沒有描述重復(fù)授權(quán)的場景，因此無法檢測出該缺陷。

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

7 結(jié)束語

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