李 艷, 莊海燕,張哲寧

(1.山東理工大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，山東 淄博 255049； 2.鐵道警察學(xué)院 公安技術(shù)系，河南 鄭州 450053；3.連云港中復(fù)連眾復(fù)合材料集團(tuán)有限公司 信息技術(shù)部，江蘇 連云港 222000)

面向SOA架構(gòu)分布式系統(tǒng)的會(huì)話交互建模及其安全驗(yàn)證

李 艷1, 莊海燕2,張哲寧3

(1.山東理工大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，山東 淄博 255049； 2.鐵道警察學(xué)院 公安技術(shù)系，河南 鄭州 450053；3.連云港中復(fù)連眾復(fù)合材料集團(tuán)有限公司 信息技術(shù)部，江蘇 連云港 222000)

研究了SOA架構(gòu)分布式系統(tǒng)在基于社區(qū)的Web服務(wù)動(dòng)態(tài)會(huì)話交互的安全性，提出了一種基于形式化規(guī)格說明的Web服務(wù)組合行為建模和驗(yàn)證框架.基于OWL-S描述的若干個(gè)Web服務(wù)的組合和交互的安全性保障問題，構(gòu)建了一種基于WS-Trust和WS-SecureConversation規(guī)格的安全會(huì)話驗(yàn)證方法.該方法首先將Web服務(wù)組合行為建模為帶有標(biāo)簽的遷移系統(tǒng)AKTS來描述服務(wù)的觀察行為；進(jìn)而將安全會(huì)話約束翻譯為DPDL公式即將SOA系統(tǒng)的會(huì)話安全性驗(yàn)證問題規(guī)約為保障安全會(huì)話約束的前提下的Web服務(wù)組合行為的滿足性問題；最后通過經(jīng)典算法在有效時(shí)間內(nèi)得到該滿足性問題的驗(yàn)證.該框架為基于SOA架構(gòu)的分布式系統(tǒng)的交互安全提供了理論支持和保障，在安全關(guān)鍵的分布式系統(tǒng)設(shè)計(jì)階段及早發(fā)現(xiàn)安全隱患，節(jié)約了開發(fā)成本、提高了系統(tǒng)安全性.

語義Web服務(wù)；分布式系統(tǒng)；SOA架構(gòu)；Web服務(wù)組合；會(huì)話安全

面對(duì)復(fù)雜業(yè)務(wù)驅(qū)動(dòng)的行業(yè)需求[1-2]，目前產(chǎn)業(yè)界采用的技術(shù)架構(gòu)為SOA(ServiceOrientedArchitecture)即面向服務(wù)的體系結(jié)構(gòu)，是一種粗粒度、開放式、松耦合的服務(wù)結(jié)構(gòu)，使軟件產(chǎn)品更加彈性和靈活地與第三方軟件產(chǎn)品互補(bǔ)兼容，以達(dá)到功能或性能快速擴(kuò)展，滿足或響應(yīng)市場、行業(yè)客戶需求的多樣化和多變性.該架構(gòu)是實(shí)現(xiàn)分布式語義Web服務(wù)系統(tǒng)快速響應(yīng)業(yè)務(wù)單位的需求，構(gòu)建實(shí)時(shí)企業(yè)的最佳技術(shù)方案.

基于分布式的WebService的發(fā)布、發(fā)現(xiàn)和組合以及集成依賴于服務(wù)接口的標(biāo)準(zhǔn)化描述，通過SOAP協(xié)議實(shí)現(xiàn)其信息共享和互操作.為實(shí)現(xiàn)上述功能，Web服務(wù)所涉及的類、關(guān)系、規(guī)則、參數(shù)等必須描述為工業(yè)化的標(biāo)準(zhǔn)語言，比如Ontology本體語言、OWL-s語言等.SOA架構(gòu)環(huán)境下的服務(wù)交互安全機(jī)制已經(jīng)引起工業(yè)界和學(xué)術(shù)界的普遍關(guān)注，相關(guān)學(xué)者也提出了相應(yīng)安全框架如WS-Trust[3]和WS-SecureConversation[4]等.它們都是建立在安全協(xié)議分析和驗(yàn)證的一系列技術(shù)和方法上的，解決部分安全屬性，諸如服務(wù)內(nèi)安全、隱私、授權(quán)等相關(guān)經(jīng)典安全屬性.

伴隨著語義WebService在產(chǎn)業(yè)界的廣泛應(yīng)用，對(duì)于服務(wù)交互安全的需求不僅是身份驗(yàn)證、授權(quán)等靜態(tài)消息安全，而是整個(gè)服務(wù)交互會(huì)話的過程安全.然而，如上所述的傳統(tǒng)Web服務(wù)建模方法局限于描述部分安全屬性即表達(dá)力不足以表達(dá)會(huì)話交互過程，驗(yàn)證依賴于人工分析，不能滿足其交互安全屬性由計(jì)算機(jī)程序自動(dòng)化驗(yàn)證的需求.

因此，本文提出一種擴(kuò)展的服務(wù)會(huì)話交互建模與驗(yàn)證方法，將服務(wù)建模為AKTS結(jié)構(gòu)，刻畫服務(wù)的動(dòng)態(tài)會(huì)話交互行為，同時(shí)將經(jīng)典的PDL,OWL-S,AKTS整合翻譯為DPDL.該方法把服務(wù)會(huì)話安全問題轉(zhuǎn)化為一致性驗(yàn)證問題，而后者很容易實(shí)現(xiàn)自動(dòng)化驗(yàn)證，為SOA架構(gòu)下的分布式服務(wù)交互設(shè)計(jì)，尤其是安全關(guān)鍵的分布式系統(tǒng)設(shè)計(jì)中的動(dòng)態(tài)會(huì)話安全性提供了理論支撐和保障.

1 SOA架構(gòu)下基于語義的Web服務(wù)會(huì)話交互建模

1.1Web服務(wù)社區(qū)、組合及其一致性

在經(jīng)典的OWL-S語言描述中，每個(gè)服務(wù)被表示為OWL類的實(shí)例，包括處理模型、綁定、配置文件三個(gè)基本屬性. 處理模型描述了服務(wù)如何執(zhí)行及其執(zhí)行細(xì)節(jié)，服務(wù)綁定描述了如何訪問Web服務(wù)[5].由于OWL-s語言是基于本體直接繼承了OWL語義表達(dá)，對(duì)于確定性和復(fù)雜計(jì)算、動(dòng)態(tài)交互屬性表達(dá)力不足，甚至是缺失的.因而，對(duì)OWL-s的處理模型屬性進(jìn)行擴(kuò)展和重新定義如下：

定義 1 語義Web服務(wù)社區(qū), Community of Web Services簡稱為CS.服務(wù)社區(qū)標(biāo)記為CS(Φ,OΦ),其中Φ表示為若干個(gè)Web服務(wù)的集合； 服務(wù)集合Φ的本體映射為集合OΦ,其中：

-Φ={θi,i=1…n},θi表示集合Φ中的第i個(gè)服務(wù);

Oi:用OWL-s語言描述的服務(wù)θi的本體;

OBi:Web服務(wù)本體Oi的一個(gè)觀察.

狀態(tài)遷移系統(tǒng)是描述動(dòng)態(tài)行為的一種形式化方法，因而采用一個(gè)帶動(dòng)作標(biāo)簽的Kripke結(jié)構(gòu)來建模服務(wù)社區(qū)中每個(gè)服務(wù)的觀察OBi.

定義 2 帶動(dòng)作標(biāo)簽的狀態(tài)遷移系統(tǒng)，ActionsKripkeTransitionSystem,簡稱為AKTS.

AKTS是一種擴(kuò)展的Kripke結(jié)構(gòu)定義為AKTS(Σ,s0,A,R,AP,L), 其中:

Σ 是狀態(tài)集;

s0是初始狀態(tài);

A是一個(gè)有限動(dòng)作集，每一個(gè)ei是一個(gè)元素,i∈1…n;

L: Σ→2AP, 是從狀態(tài)映射為原子命題集AP的標(biāo)簽函數(shù);

AP:是有限的原子命題集.

根據(jù)業(yè)務(wù)需求的復(fù)雜度不同，復(fù)雜目標(biāo)服務(wù)可以由服務(wù)社區(qū)中的多個(gè)服務(wù)組合構(gòu)成, 可以定義為在AKTS增加一個(gè)調(diào)度函數(shù)(DispatchFunction).

Σc是一個(gè)關(guān)于Oc狀態(tài)的有限集;

sc0是初始狀態(tài);

Rc:Σc×Ac→Σc; 是狀態(tài)遷移關(guān)系.

APc: 是從Oc翻譯出的原子命題集;

Lc:Σc→2APc, 是一個(gè)二元關(guān)系;

{|si=|OP};P是APc的一個(gè)子集;

K:Rc→Ri,函數(shù)K的變遷滿足rc∈Rc且rj∈Ri.

定義5 面向服務(wù)社區(qū)的服務(wù)組合. 一個(gè)面向服務(wù)社區(qū)CS的語義Web服務(wù)組合定義為給定一個(gè)組合行為CB來描述服務(wù)操作或動(dòng)作的序列及其分支， 并檢查社區(qū)CS內(nèi)服務(wù)的組合動(dòng)作一致性(如定義6所示).

定義6 組合動(dòng)作一致性. 社區(qū)內(nèi)服務(wù)的組合動(dòng)作一致性定義如下：

γ是一個(gè)從s0∈Σ開始的變遷序列,

,ri∈Rc,i=1…n;

在服務(wù)社區(qū)中最后2個(gè)變遷分別為

且滿足前提條件θ, 則γ是可運(yùn)行的；

組合動(dòng)作一致性,滿足當(dāng)且僅當(dāng)任意一個(gè)γ是可運(yùn)行的.

1.2 服務(wù)組合動(dòng)作編碼為DPDL

社區(qū)內(nèi)服務(wù)組合問題可以約簡為組合動(dòng)作模型公式的可滿足性問題.作為一種經(jīng)典的模態(tài)邏輯,確定性命題動(dòng)態(tài)邏輯(theDeterministicPropositionalDynamicLogic，DPDL) 有很強(qiáng)的表達(dá)力適合用來建模服務(wù)組合問題.命題動(dòng)態(tài)邏輯DPDL的語法規(guī)則如下:

其中,

p∈P，P是原子命題集;

α∈A,A是原子程序集;

φis 是由P基于 ┓, ∧, ∨構(gòu)建的命題;

DPDL是PDL的一個(gè)變種版本, 用來建模一個(gè)確定的結(jié)構(gòu).按照某種規(guī)則，一個(gè)遷移系統(tǒng)可以翻譯為DPDL，而一個(gè)語義服務(wù)的觀察模型AKTS,可以按照如下規(guī)則編碼為DPDL公式:

定義7 組合行為CB及其觀察OBs的編碼規(guī)則.

1) 給定a的前提條件φ，編碼組合行為CB和其最終狀態(tài)FCB的步驟如下所述:

[u](s→┓snext)是不同狀態(tài)的不相交集;

[u](FCB→∨s∈FCBs)CB遷移到最終狀態(tài).

2)編碼社區(qū)中其它服務(wù)的觀察OB規(guī)則如下:

[u](s→┓snext)是不同狀態(tài)的不相交集;

3) 所有社區(qū)內(nèi)的語義WebService是基于OWL-DL語言的，即一種變種的描述邏輯SHOIQ, 也可以根據(jù)規(guī)則翻譯為DPDL[6-7].部分主要關(guān)系映射見表1.

表1DPDL翻譯規(guī)則映射表

ConstructorsDPDLformulas⊥FALSETTRUE？C？CC∩DC∧DC∪DC∨D?R．CC?R．C[R]C

如果組合行為CB是服務(wù)社區(qū) CS的一個(gè)服務(wù)組合問題，則可以根據(jù)上述規(guī)則翻譯為DPDL公式并檢查其滿足性來判定該組合行為是否可執(zhí)行. 對(duì)于社區(qū)CS，其命題集和動(dòng)作集分別定義如定義8-9.

定義8 命題集(PropositionsSetonCommunity).命題集用符號(hào)PDPDL標(biāo)識(shí)，是建立在社區(qū)所有服務(wù)的相關(guān)狀態(tài)基礎(chǔ)上的.

Oi: 服務(wù)翻譯為命題的本體(Ontology);

Σi: 描述服務(wù)的狀態(tài)集;

定義 9 動(dòng)作集(ActionsSetonCommunity). 動(dòng)作集用符號(hào)ADPDL來標(biāo)識(shí)，其定義為

ADPDL=AΦ,AΦbelongstoCS(OΦ,Φ).

定義10 公式ΦDPDL編碼為DPDL公式. 公式ΦDPDL定義為

定理1 根據(jù)定義10所創(chuàng)建的DPDL公式ΦDPDL是可滿足的，當(dāng)且僅當(dāng)組合行為CB是存在且在服務(wù)社區(qū)是可執(zhí)行的[6].

2 Web服務(wù)安全會(huì)話模式

2.1 基于WS-Trust的安全會(huì)話

采用WS-Trust和WS-SecureConversation形式化定義的基礎(chǔ)架構(gòu)和安全交互模式維持一個(gè)安全會(huì)話，來保障服務(wù)不受外部的攻擊，這種安全模式可以抽象為服務(wù)的約束.

一個(gè)基于Web服務(wù)交互的信任代理模型如圖1所示，包括三個(gè)參與方： 客戶、Web服務(wù)和 安全令牌服務(wù)(SecurityTokenSystem，STS). 為了便于討論起見，假定所有Web服務(wù)通過STS一個(gè)內(nèi)部機(jī)制共享認(rèn)證信息、安全令牌信息，且客戶、Web服務(wù)和STS分別持有證書授權(quán).作為一個(gè)安全代理服務(wù)STS為客戶和服務(wù)間的通信提供了安全上下文令牌(securitycontexttokens,SCTs). 為了訪問和使用Web服務(wù), 用戶首先向STS請求一個(gè)安全上下文令牌SCT，通過會(huì)話秘鑰序列來保護(hù)一系列的消息安全. 限于論文篇幅, 安全上下文的修正、取消和更新在這里不展開討論. 整個(gè)交互過程包括兩個(gè)階段如圖1所示： 第一個(gè)階段是用戶向安全令牌服務(wù)STS申請一個(gè)上下文安全令牌SCT包括步驟1請求和步驟2響應(yīng)； 第二個(gè)階段是 客戶和相關(guān)Web服務(wù)在安全上下文SCT的安全保護(hù)下的會(huì)話交互，該交互過程包括步驟3i客戶請求和步驟4i服務(wù)響應(yīng).

圖1 Web服務(wù)交互場景

如圖1所示, 基于上述安全框架可以構(gòu)建一個(gè)安全會(huì)話來保障一個(gè)客戶和服務(wù)間的交互安全.但是我們需要形式化驗(yàn)證Web服務(wù)尤其是多個(gè)Web服務(wù)的組合行為交互過程是否滿足可執(zhí)行性.

2.2 將安全會(huì)話規(guī)約為DPDL驗(yàn)證

在上述場景中, 三個(gè)參與方可以看作是三個(gè)相互動(dòng)態(tài)交互的獨(dú)立Web服務(wù)模型.因此檢查其安全會(huì)話問題可以規(guī)約為根據(jù)定義11描述的DPDL定義的Web服務(wù)的組合行為問題.

定義 11 安全會(huì)話模式.安全會(huì)話模式是個(gè)Web服務(wù)訪問行為的序列，遵守WS-Trust規(guī)則. 根據(jù)本文服務(wù)社區(qū)的相關(guān)定義, 可以定義帶有2個(gè)服務(wù)的服務(wù)社區(qū), 即STS和Web服務(wù)A. 從客戶的角度看, 其安全訪問過程就是STS和Web服務(wù)A的組合行為.因此, 服務(wù)社區(qū)的構(gòu)建問題約簡為驗(yàn)證組合行為可執(zhí)行性問題，規(guī)則如下：

1)定義服務(wù)社區(qū)并將組合行為翻譯為DPDL公式：

2)規(guī)約安全會(huì)話約束CSSP(ConstraintofSecureSessionPattern)為DPDL公式的可滿足性問題M：

根據(jù)定理1所述，可以將服務(wù)社區(qū)上的組合行為執(zhí)行問題轉(zhuǎn)化為DPDL公式的可滿足性問題來驗(yàn)證，上述PDDL的可滿足性問題M可采用經(jīng)典的Lookahead算法求解[7].

3 結(jié)束語

本文以SOA架構(gòu)分布式系統(tǒng)的Web服務(wù)交互安全問題為研究切入點(diǎn)，深入研究了Web服務(wù)的動(dòng)態(tài)交互組合的形式化規(guī)約，同時(shí)借鑒并擴(kuò)展了經(jīng)典的WS-Trust安全框架的表達(dá)能力，將分布式系統(tǒng)的Web服務(wù)安全交互建模為改進(jìn)的Kripke結(jié)構(gòu)即AKTS，能夠有效描述服務(wù)會(huì)話交互過程以及其相關(guān)約束. 進(jìn)而，將服務(wù)交互的安全約束規(guī)約為DPDL公式的可滿足性問題，可采用經(jīng)典算法在有效時(shí)間內(nèi)得到驗(yàn)證.

該建模和驗(yàn)證方法為面向SOA架構(gòu)的分布式系統(tǒng)等安全關(guān)鍵性系統(tǒng)，在設(shè)計(jì)的前期階段實(shí)現(xiàn)了分析和驗(yàn)證基礎(chǔ)，為系統(tǒng)的安全性設(shè)計(jì)提供了可靠保障，有效避免了系統(tǒng)后期的安全風(fēng)險(xiǎn).目前的主要建模和驗(yàn)正工作依賴于手工，下一步的主要工作是實(shí)現(xiàn)一個(gè)自動(dòng)化建模與驗(yàn)證的軟件平臺(tái).

[1]謝春麗,俞析蒙,王書芹. 基于SOA的web服務(wù)可靠性預(yù)測[J].計(jì)算科學(xué),2014,41(7):222 -226.

[2]茅維華,唐守國,高淑娟,等. 基于SOA架構(gòu)的業(yè)務(wù)協(xié)同關(guān)鍵技術(shù)平臺(tái)監(jiān)控系統(tǒng)[J].計(jì)算機(jī)工程,2009,35(19):280- 283.

[3]楊楊,賈君君,李晨. 面向服務(wù)架構(gòu)的云計(jì)算平臺(tái)[J].計(jì)算機(jī)應(yīng)用,2015,35(11):35-38

[4]KALERC,NADALINA,MONZILLR.WebServicesTrustLanguage(WS-Trust)Version1.1,May2014. [EB/OL]. [2014-05-10].https://msdn.microsoft.com/zh-cn/library/aa480726.aspx

[5]CARMINATICB,FERRARIE,HUNGPCK.SecurityconsciousWebServiceComposition[C]//ProceedingsofIEEEInternationalConferenceonWebServices.USA:IEEEComputerSociety, 2015: 489-496.

[6]KAGALL,FININT,JOSHIA.APolicybasedApproachtoSecurityfortheSemanticWeb[J].LectureNotesinComputerScience, 2013,28(70): 402-418.

[7]BERARDID,CALVANESED,GIACOMOGD,etal.Automaticservicecompositionbasedonbehaviouraldescriptions[J].InternationalJournalofCooperativeInformationSystem, 2015, 14(4):333-376.

(編輯：劉寶江)

ModelingandverificationofsecurityofinteractivesessionforSOAbaseddistributedsystems

LIYan1,ZHUANGHai-yan2,ZHANGZhe-ning3

(1.SchoolofComputerScienceandTechnology,ShandongUniversityofTechnology,Zibo255049,China;2.DepartmentofPublicSecurityTechnology,RailwayPoliceCollege,Zhengzhou450053,China;3.InformationDepartment,ZhongfuLianzhongCompositesGroupCompanyLimited,Lianyungang222000,China)

ThepaperresearchtheissueofsessionsecurityforSOA(ServiceOrientedArchitecture)baseddistributedinformationsystemsandputforwardaformalmodelingandverificationframeworkinordertocheckandmaintainthesecurityoftheinteractivebetweenthesemanticwebservices.HierarchyandcomposedinteractionsamongseveralWebservicesdepictedbyOWL-S(OntologyWebLanguageforServices)needtobeconsideredwhethersatisfyingsecuritywhencomposition.Therefore,asecuresessionpatternbasedapproachispresentedtoverifytheconsistencywiththoseinspecifications,whichbasedonWS-TrustandWS-SecureConversation.Firstofall,processesincompositionrequirementsandwebservicesaremodeledbyAKTS(ActionsKripkeTransitionSystems)todescribeobservablebehaviors.Then,withtheconstraintsofsecuresessionpatterns,thesatisfactionofthecompositionisverifiedbyDPDL(DeterministicPropositionalDynamicLogic).Finally,theformulaofdeterministicpropositionallogiccanbesolvedbythetypicalmethodologyeffectively,whichwillbringusmoreconvenienceforthedesignoftheSOAbaseddistributedsystemsespeciallyforsecuritycriticalsystems.

semanticwebservice;distributedsystems;serviceorientedarchitecture;webservicecomposition;sessionsecurity

2016-04-26

河南省科技廳科技攻關(guān)項(xiàng)目(2014GGJS-073);鐵道警察學(xué)院基金項(xiàng)目(JY2014Z05)

李 艷，女，lly_xiao@sohu.com； 通信作者：莊海燕，女,zhuanghy76@163.com

1672-6197(2017)03-0020-05

TP

A