面向SOA架構分布式系統的會話交互建模及其安全驗證

李 艷, 莊海燕,張哲寧

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

面向SOA架構分布式系統的會話交互建模及其安全驗證

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

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

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

語義Web服務；分布式系統；SOA架構；Web服務組合；會話安全

面對復雜業務驅動的行業需求[1-2]，目前產業界采用的技術架構為SOA(ServiceOrientedArchitecture)即面向服務的體系結構，是一種粗粒度、開放式、松耦合的服務結構，使軟件產品更加彈性和靈活地與第三方軟件產品互補兼容，以達到功能或性能快速擴展，滿足或響應市場、行業客戶需求的多樣化和多變性.該架構是實現分布式語義Web服務系統快速響應業務單位的需求，構建實時企業的最佳技術方案.

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

伴隨著語義WebService在產業界的廣泛應用，對于服務交互安全的需求不僅是身份驗證、授權等靜態消息安全，而是整個服務交互會話的過程安全.然而，如上所述的傳統Web服務建模方法局限于描述部分安全屬性即表達力不足以表達會話交互過程，驗證依賴于人工分析，不能滿足其交互安全屬性由計算機程序自動化驗證的需求.

因此，本文提出一種擴展的服務會話交互建模與驗證方法，將服務建模為AKTS結構，刻畫服務的動態會話交互行為，同時將經典的PDL,OWL-S,AKTS整合翻譯為DPDL.該方法把服務會話安全問題轉化為一致性驗證問題，而后者很容易實現自動化驗證，為SOA架構下的分布式服務交互設計，尤其是安全關鍵的分布式系統設計中的動態會話安全性提供了理論支撐和保障.

1 SOA架構下基于語義的Web服務會話交互建模

1.1Web服務社區、組合及其一致性

在經典的OWL-S語言描述中，每個服務被表示為OWL類的實例，包括處理模型、綁定、配置文件三個基本屬性. 處理模型描述了服務如何執行及其執行細節，服務綁定描述了如何訪問Web服務[5].由于OWL-s語言是基于本體直接繼承了OWL語義表達，對于確定性和復雜計算、動態交互屬性表達力不足，甚至是缺失的.因而，對OWL-s的處理模型屬性進行擴展和重新定義如下：

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

-Φ={θi,i=1…n},θi表示集合Φ中的第i個服務;

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

OBi:Web服務本體Oi的一個觀察.

狀態遷移系統是描述動態行為的一種形式化方法，因而采用一個帶動作標簽的Kripke結構來建模服務社區中每個服務的觀察OBi.

定義 2 帶動作標簽的狀態遷移系統，ActionsKripkeTransitionSystem,簡稱為AKTS.

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

Σ 是狀態集;

s0是初始狀態;

A是一個有限動作集，每一個ei是一個元素,i∈1…n;

L: Σ→2AP, 是從狀態映射為原子命題集AP的標簽函數;

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

根據業務需求的復雜度不同，復雜目標服務可以由服務社區中的多個服務組合構成, 可以定義為在AKTS增加一個調度函數(DispatchFunction).

Σc是一個關于Oc狀態的有限集;

sc0是初始狀態;

Rc:Σc×Ac→Σc; 是狀態遷移關系.

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

Lc:Σc→2APc, 是一個二元關系;

{|si=|OP};P是APc的一個子集;

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

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

定義6 組合動作一致性. 社區內服務的組合動作一致性定義如下：

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

,ri∈Rc,i=1…n;

在服務社區中最后2個變遷分別為

且滿足前提條件θ, 則γ是可運行的；

組合動作一致性,滿足當且僅當任意一個γ是可運行的.

1.2 服務組合動作編碼為DPDL

社區內服務組合問題可以約簡為組合動作模型公式的可滿足性問題.作為一種經典的模態邏輯,確定性命題動態邏輯(theDeterministicPropositionalDynamicLogic，DPDL) 有很強的表達力適合用來建模服務組合問題.命題動態邏輯DPDL的語法規則如下:

其中,

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

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

φis 是由P基于 ┓, ∧, ∨構建的命題;

DPDL是PDL的一個變種版本, 用來建模一個確定的結構.按照某種規則，一個遷移系統可以翻譯為DPDL，而一個語義服務的觀察模型AKTS,可以按照如下規則編碼為DPDL公式:

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

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

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

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

2)編碼社區中其它服務的觀察OB規則如下:

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

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

表1DPDL翻譯規則映射表

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

如果組合行為CB是服務社區 CS的一個服務組合問題，則可以根據上述規則翻譯為DPDL公式并檢查其滿足性來判定該組合行為是否可執行. 對于社區CS，其命題集和動作集分別定義如定義8-9.

定義8 命題集(PropositionsSetonCommunity).命題集用符號PDPDL標識，是建立在社區所有服務的相關狀態基礎上的.

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

Σi: 描述服務的狀態集;

定義 9 動作集(ActionsSetonCommunity). 動作集用符號ADPDL來標識，其定義為

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

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

定理1 根據定義10所創建的DPDL公式ΦDPDL是可滿足的，當且僅當組合行為CB是存在且在服務社區是可執行的[6].

2 Web服務安全會話模式

2.1 基于WS-Trust的安全會話

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

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

圖1 Web服務交互場景

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

2.2 將安全會話規約為DPDL驗證

在上述場景中, 三個參與方可以看作是三個相互動態交互的獨立Web服務模型.因此檢查其安全會話問題可以規約為根據定義11描述的DPDL定義的Web服務的組合行為問題.

定義 11 安全會話模式.安全會話模式是個Web服務訪問行為的序列，遵守WS-Trust規則. 根據本文服務社區的相關定義, 可以定義帶有2個服務的服務社區, 即STS和Web服務A. 從客戶的角度看, 其安全訪問過程就是STS和Web服務A的組合行為.因此, 服務社區的構建問題約簡為驗證組合行為可執行性問題，規則如下：

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

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

根據定理1所述，可以將服務社區上的組合行為執行問題轉化為DPDL公式的可滿足性問題來驗證，上述PDDL的可滿足性問題M可采用經典的Lookahead算法求解[7].

3 結束語

本文以SOA架構分布式系統的Web服務交互安全問題為研究切入點，深入研究了Web服務的動態交互組合的形式化規約，同時借鑒并擴展了經典的WS-Trust安全框架的表達能力，將分布式系統的Web服務安全交互建模為改進的Kripke結構即AKTS，能夠有效描述服務會話交互過程以及其相關約束. 進而，將服務交互的安全約束規約為DPDL公式的可滿足性問題，可采用經典算法在有效時間內得到驗證.

該建模和驗證方法為面向SOA架構的分布式系統等安全關鍵性系統，在設計的前期階段實現了分析和驗證基礎，為系統的安全性設計提供了可靠保障，有效避免了系統后期的安全風險.目前的主要建模和驗正工作依賴于手工，下一步的主要工作是實現一個自動化建模與驗證的軟件平臺.

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

[2]茅維華,唐守國,高淑娟,等. 基于SOA架構的業務協同關鍵技術平臺監控系統[J].計算機工程,2009,35(19):280- 283.

[3]楊楊,賈君君,李晨. 面向服務架構的云計算平臺[J].計算機應用,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

河南省科技廳科技攻關項目(2014GGJS-073);鐵道警察學院基金項目(JY2014Z05)

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

1672-6197(2017)03-0020-05

TP

A