面向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