基于模型驱动的Web服务符号执行与验证

王昌晶,陈 茜,丁希龙,罗海梅,左正康*

(1.江西师范大学计算机信息工程学院,江西 南昌 330022;2.江西师范大学管理科学与工程研究中心,江西 南昌 330022;3.江西师范大学物理与通信电子学院,江西 南昌 330022)

0 引言

随着云计算技术的高速发展,Web服务作为一种新兴的网络应用模式得到了迅速的发展.基于面向服务架构的(Service Oriented Architecture,SOA)Web服务是一个独立、自包含、低耦合、可编程的应用程序,在电子商务、资料查询、办公自动化等若干核心领域中有着广泛应用.

符号执行技术是目前研究领域广泛认可的形式化、自动化测试技术.近年来,符号执行技术不断地发展与优化以及与一些新技术(如SMT、Fuzzing等)结合,这极大地提高了符号执行的可用性与实用性.符号执行工具(如LLVM、KLEE、S2E、SED等)的出现与发展提高了自动化程度.因此,符号执行技术作为一种重要的形式化方法[1]和软件分析技术,引起了国际学术界的广泛研究.

如何保证Web服务可靠性与正确性并满足用户需求是目前Web服务研究领域的热点.Web服务的测试[2-3]与验证能提前发现Web服务存在的问题,这是发布高可靠Web服务的有效途径.但在实际测试中,由于资源有限所以使得测试不充分,而且Web服务测试复杂、费时费力.国内外对于Web服务验证的研究一般是基于某种形式化方法,大致可以分为3类:Petri网、自动机理论和进程代数.其中Petri网与自动机的方法对服务组合的验证[4]计算量大,其复杂度随着服务规模的增大而急剧增大;进程代数比较抽象,难以被广泛使用.

模型驱动架构的方法采用主流的商业过程建模[5-6],支持从系统高层模型逐步转换,但难以生成Web服务可执行代码.面向服务的建模分析方法(SOMA)缺乏形式化语义.针对该不足,本文前期工作使用自定义的建模语言Radl-WS对Web服务需求建模,使用模型驱动的方式对Web服务建模与转换,并对转换生成的Java代码进行符号执行与验证.

本文采用模型驱动的方法对Web服务进行符号执行与验证.在前期研究的基础上,对转换生成的Java代码符号执行,并将Radl-WS需求规约对应转换成JML(Java Modeling Language)方法契约加入Java代码进行验证.本文使用基于Eclipse平台扩展的符号执行工具SED(Symbolic Execution Debugger),对基于模型驱动的Web 3阶段生成的Java代码进行符号执行与验证.

1 3阶段Web服务模型转换生成方法

模型驱动架构MDA(Model Driven Architecture)是由OMG定义的一个软件开发框架[7],以模型为核心,将实际问题抽象化并建立相关模型,再对模型进行转换与精化.MDA开发过程是从3个不同的层次建立系统模型:第1层为计算无关模型(Computational Independent Model,CIM),第2层为平台无关模型(Platform Independent Model,PIM),第3层为平台相关模型(Platform Specific Model,PSM).

基于模型驱动的3阶段Web服务模型转换生成方法的过程如下:首先使用代数规范的Radl-WS对Web服务需求建模;然后将Radl-WS服务需求模型转换成Apla服务设计模型;再将Apla服务设计模型通过PAR方法及其支持平台程序转换器生成可执行代码[8-12];最后将可执行代码封装成服务.基于模型驱动的3阶段转换生成方法如图1所示.

图1 基于模型驱动的3阶段转换生成方法

其中Radl-WS服务需求模型对应CIM,Apla服务设计模型对应PIM,经过PAR方法及其支撑平台系列转换器(Apla→Java、Apla→C++等)生成的可执行代码对应PSM1,最后封装成的服务WSDL/RESTful API对应PSM2.

为了提高模型的可靠性与正确性,在前期模型驱动的3阶段转换生成方法的基础上,本文对Web服务进行符号执行与验证.

2 Java代码符号执行

2.1 符号执行

符号执行是一种程序分析技术,通过分析程序来得到让特定代码区域执行的输入[13-14].在使用符号执行分析一个程序时,用符号值代替具体值作为输入.通过追踪在程序中各个可能执行状态处的符号值及所需要满足的条件,计算可满足的具体值,将它作为输入代入程序中执行,从而验证在不同状态输入下程序的正确性.

符号执行路径是一个true和false序列seq=(P0,P1,…,Pn),若一个条件语句为Pi=true则这表示条件语句为true,否则为false.对如图2所示的代码进行符号执行,分析程序testme(),符号执行有3条路径,形成如图3所示的符号执行树.

图2 符号执行示例代码

图3 示例程序代码执行树

以图2的代码为例,符号执行会在全局中维护2个变量(σ,PC).符号状态σ记录在程序中每个变量到符号表达式的映射.符号化路径约束PC表示路径条件,初始值为true.σ和PC在符号执行过程中不断更新,当符号执行结束时,求解PC就可得覆盖所有路径的输入.将输入x、y定义为符号变量a、b的过程如下:

(i)σ:x→a,y→b,PC1:true;

(ii)σ:x→a,y→b;z→2b,PC2:true;

(iii)σ:x→a,y→b;z→2b,PC3:true∧2*b≤a;

(iv)σ:x→a,y→b;z→2b,PC4:true∧2*b>a;

(v)σ:x→a,y→b;z→2b,PC5:true∧(2*b>a)∧(a≤b+10);

(vi)σ:x→a,y→b;z→2b,PC6:true∧(2*b>a)∧(a>b+10).

在符号代码执行过程中,若遇到赋值操作,则也将新产生的变量当成符号变量进行处理.如代码第5行变量赋值,符号变量在处理后为z→2b.在分析处理完毕后,可以使用SMT约束求解器求解满足路径约束PC的解,即为沿着该路径执行的某一具体测试案例.如在该示例中的路径约束PC6:true∧(2*b>a)∧(a>b+10),当a=30、b=16时满足此路径约束(即当以x=30、y=16作为其中一个测试案例输入)时,可以触发程序错误.

2.2 对Java代码符号执行

SED(Symbolic Execution Debugger)是Eclipse平台扩展的交互式符号执行调试器[15],可以安装到Java编译环境中,方便使用.交互式符号执行调试器SED与传统调试器一样能定位在源码中的缺陷,SED还提供了一个Java程序符号执行引擎KeY[16],支持用JML规范注释的Java代码.SED不仅可以提高对Java代码的审查与错误定位,还可验证任务的有效性与正确性.本文使用交互式调试器SED作为自动化验证工具来验证实验的有效性与正确性.

将在图2中的伪代码转换成Java可以执行代码,使用SED交互式符号执行调试器执行.如图4所示,可以看出自动化工具生成的符号执行树与图3对示例程序分析生成的执行树分支路径一致,达到了预期效果,这说明符号执行的正确性.SED视图结构形象直观、操作界面友好、交互方便且易使用易上手.SED不仅支持严格的验证,还提高了代码审查与证明的效率.

图4 Java代码符号执行

3 Java代码形式化验证

3.1 Radl-WS建模语言转换为JML方法契约

Radl-WS是在Radl语言的基础上扩展而来的,是一种新型的基于代数规范的Web服务建模语言.Radl-WS代数规范由若干规格单元组成,代表在软件系统中的一个实体类型[17-20].每个规格说明单元包括一个〈sort name〉,其中又包括2个更小的单元:(i)签名单元(signature unit),其语法由签名来定义;(ii)公理单元(axiom unit),其语法由若干必须满足的公理来定义.使用BNF描述Radl-WS代码规范如下:

〈spec unit〉::=spec〈sort name〉

[extends〈extend sort list〉]

[imports〈import sort list〉]

〈signature unit〉;

[〈axioms unit〉]

end-spec.

其中签名单元(〈signature unit〉)BNF描述如下:

〈signature unit〉::[sorts〈sort list〉];

ops 〈operation list〉.

在Radl-WS的签名单元(〈signature unit〉)中,前置断言用Q开头的谓词表达式来表示,后置断言用R开头的谓词表达式来表示,规格说明如下:

|[标志符声明]|

Q:谓词表达式;

R:谓词表达式.

JML是一种形式化的行为接口规范语言,是为Java量身定制的.JML引入模型域、量词、前后置断言、预处理、条件继承及异常行为处理规范等描述行为到结构中.通过使用标识符来说明一个方法的预期功能,而不关心具体的实现.

如求一个整型数组的平均值,该方法命名为sum_average,该方法的Java代码很简单,具体代码如图5所示.

图5 求数组平均值的Java代码

本文采用Radl-WS对该方法进行建模,由对该方法需求分析可知,该方法成立的前提是数组不为空,即作为在Radl-WS规范中前置断言Q:a!=null.该方法在执行结束后,需满足i大于等于0且小于数组长度,用Radl-WS后置断言R描述为R:i≥0&&i<#(a);a[i].根据Radl-WS语法规则,关键词spec规格说明是一个方法,规格说明单元sort为数组类型,op表示具体操作为检查观察子(observer),in表示输入,out表示输出.该方法的Radl-WS规约如图6所示.

图6 sum_average Radl-WS需求规约

以图6为例,将Radl-WS规约转换成JML方法契约,具体转换步骤如下:

(i)名称和标识符声明转换.将观察子中对应的操作的名称sum_average转换成Java代码的方法名sum_average(方法名称不变),Radl-WS中输入in操作(a:array)转换成Java方法中的参数输入(a[]),其中array→int表示数组的类型为整型,对应Java中的整型数组定义.

(ii)前后置断言转换.关键词对应转换,Radl-WS代数规范中前置断言Q与后置断言R分别对应JML关键词requires及ensures.将Radl-WS 描述的规约转换成符合JML语法规范的描述.在此例中,前置断言转换不变.对于后置断言部分在执行结束后的返回值JML中使用关键词 esult,其中Radl-WS规范中#(a)表示求数组长度,对应地在JML中调用length.其他部分对应转换,主要是把在Radl-WS中前后置断言的谓词表达式转换成符合JML语言规范的描述.

(iii)异常处理.在头部中添加关键词normal_behavior 表示正常执行部分.异常处理关键词exceptional_behavior,从aslo开始到最后是异常处理部分.

(iv)其他部分的关键词为变量约束,根据具体情况来添加符合JML规范的描述即可.

将图6的Radl-WS需求规约按照上述转换步骤进行转换,转换后的JML代码如图7所示.

JML语言能较好地与Radl-WS语言的关键部分(前后置断言)对应起来,其他部分按照语义使用JML规范书写即可.

3.2 对Java代码进行验证

本文采用符号执行的自动化验证工具SED对JML方法契约验证.如图8所示,使用方法契约及循环不变量来代替内联和展开,从而保证有限深度的符号执行,方法indexOf返回过滤器接受的在给定数组中第1个索引.接口Filter不用具体实现,但它的方法accept可用JML指定.如图8所示,在对该方法进行验证时,在符号执行树左侧任意循环迭代中,循环结束节点出现交叉线,这表明该方法验证有误.

由图8可知:在if分支最左边的分支结束节点上出现了交叉线条,这说明程序存在问题.分析if条件是否满足,并找到原因是i没有增加,这里不满足循环不变量的递减子句decreasing array.length-i的递减要求,所以在if子句中最后加上i++即可满足,若抛出异常或跳出循环(break、continue或return),则循环不变量不必保持,并且在循环外继续执行.修改后再验证,结果如图9所示.

图7 sum_average JML方法契约

图8 过滤器查找数组元素验证失败

图8的程序代码如下:

public class ArrayUtil {

/*@ normal_behavior

@ requires invariant_for(filter);

@*/

public static int /*@ strictly_pure @*/ indexOf(Object[] array,

Filter filter) {

int index=-1;

inti=0;

/*@ loop_invarianti≥ 0 &&i≤array.length;

@ decreasing array.length-i;

@ assignable strictly_nothing;

@*/

while (index<0 &&i

if (filter.accept(array[i])) {

index=i;

}

else {

i++;

}

}

returni;

}

public static interface Filter {

/*@ normal_behavior

@ requires true;

@ ensures true;

@*/

public boolean /*@ strictly_pure @*/ accept(/*@ nullable @*/ Object object);

}

}.

图9 修改后验证成功

图9的程序代码如下:

public class ArrayUtil {

/*@ normal_behavior

@ requires invariant_for(filter);

@*/

public static int /*@ strictly_pure @*/ indexOf(Object[] array,

Filter filter) {

int index=-1;

inti=0;

/*@ loop_invarianti≥0 &&i≤ array.length;

@ decreasing array.length-i;

@ assignable strictly_nothing;

@*/

while (index<0 &&i

if (filter.accept(array[i])) {

index=i;

break;

}

else {

i++;

}

}

returni;

}

public static interface Filter {

/*@ normal_behavior

@ requires true;

@ ensures true;

@*/

public boolean /*@ strictly_pure @*/ accept(/*@ nullable @*/ Object object);

}

}

使用该方法可对上述求数组平均值sum_average方法的验证,根据Radl-WS转换生成的JML方法契约,使用test函数来调用该方法,进而验证sum_average方法是否正确.其中,在使用符号执行工具对该方法进行验证时,需要在符号执行选项设置中选择需使用方法.在具体执行时应根据自己的验证条件及需求设置合适的符号执行选项.sum_average方法验证结果如图10所示.

在符号执行或者验证中,若在某个节点上出现了交叉线条,则该程序或者方法契约不正确.具体操作步骤及图标含义参见文献[15].在图10的整个执行树中每一个节点都没有交叉线条,这说明此方法契约正确,验证成功.

图10 sum_average方法契约验证执行树

4 案例:PayPal Web服务

4.1 服务业务流程

以PayPal Web服务为例分别对数据建模与服务建模,其中服务模型会调用数据模型.本文采用基于模型驱动的3阶段方法对Java代码符号执行与验证,分别对PayPal数据模型与服务模型进行符号执行与验证[21].

首先对Web服务进行需求分析,并使用Radl-WS语言进行需求建模.在案例研究分析后,创建数据模型,根据CRUD原则,新增createRecord、查询findRecordBykey及更新updateRecord和操作删除deletRecord.定义了交易记录类TransRecord和用户个人信息记录类型PayerInfoType.

创建服务模型包括setExpressCheckout启动付款交易服务、getExpressCheckoutDetail获取买方信息、doExpresssCheckout更新余额完成交易.PayPal Web服务业务具体调用如图11所示.

图11 PayPal服务调用流程

当买方在商品加入购车后将点击支付,这时会启动setExpressCheckout服务,并返回时间令牌值.然后登录网站,确认用户信息.若用户批准付款,则调用getExpressCheckoutDetail服务,返回买方用户信息;若用户不同意付款,则结束服务.用户同意,确认订单,完成支付,调用doExpresssCheckout服务,更新余额,完成订单.

4.2 符号执行

4.2.1 数据模型符号执行 在模型驱动的Web服务建模与3阶段模型转换方法的工作基础上,本文对3阶段转换生成的Java可执行代码进行测试与验证.分别从数据模型与服务模型2个方面进行符号执行与验证来检验转换结果的正确性.由于篇幅原因,所以本文仅从数据模型中选择其中的一个方法(查询findRecordBykey)进行符号执行.findRecordBykey方法的Java代码如下:

publicstatic/*@ pure @*/TransRecord /*@ pure @*/findRecordByKey(/*@ nullable @*/String token){

TransRecord rec=newTransRecord();

/*@ loop_invarianti≥0&&i≤transEntity.length;

@ decreases (transEntity.length-i);

@ assignablei;

@*/

for (inti=0;i

if(token==transEntity.[i].getToken())

{

rec.setToken(transEntity.[i].getToken());

rec.setTransAmount(transEntity.[i].getTrans-Amount());

rec.setPaymentStatus(transEntity.[i].getPaymentStatus());

rec.setPayerInfo(transEntity.[i].getPayerInfo());

returnrec;

}

}

returnnull;

}.

符号执行涉及循环,本文使用循环规范处理,如上代码中的第2～4行.在符号执行选项设置中选择使用循环不变式.对findRecordBykey方法符号执行,结果如图12所示.

图12 findRecordBykey符号执行

案例程序较复杂,符号执行树较大,本文截取关键部分展示.符号执行树与预期结果走向相同,且分支与预先分析设计相同.结果表明findRecordBykey执行结果正确.数据模型的其他方法同理执行,符号执行均成功,这表明本文案例数据模型符号执行测试成功.

4.2.2 服务模型符号执行 在数据模型成功后,同理可使用符号执行对服务模型测试.本文选取在服务模型中的setExpressCheckout服务符号执行测试.该方法的Java代码如下:

public static/*@ pure @*/ String setExpressCheckout(/*@ nullable @*/intpaymentAmount){

ppdm.createRecord(rec);

return rec.getToken();

}.

即对该方法Java代码进行符号执行(见图13).

图13 setExpressCheckout符号执行

通过符号执行树及节点可以看出该方法执行成功.

数据模型与服务模型符号执行均正确执行,这表明案例符号执行测试成功.

4.3 形式化验证

4.3.1 数据模型验证 根据Radl-WS规则,对该案例中的新增、查询、更新及删除操作进行数据建模.为了验证转换后的Java代码的正确性,本文将Radl-WS需求模型转换成JML方法契约,将JML方法契约加入Java代码中并验证.以查询操作为例,Radl-WS代码如下:

其中type是类型定义,定义了2个记录及变量,该规约规格名为PayPalDM):

type TransRecord=record

token:string;

transAmount:real;

payerInfo:PayerInfoType;

paymentStatus:{Processed,Inprogress,Denied};

end

type PayerInfoType=record

age:integer;

name:string;

sex:string;

shipping address:string;

email:string;

end

spec PayPalDM

Imports:TransRecord,PayerInfoType

sorts:

transEntity:set(TransRecord);

ops:

observer:

findRecordBykey:string→table(TransRecord)

|[in key:string;out result.transEntity:table (TransRecord)]|

{Q:true}

{R:result.transEntity=

Π{token,transAmount,payerInfo,paymentStatus}σ{this.token=key}(this.transEntity)}

axioms:

end-spec.

Radl-WS建模语言转换成的JML方法契约代码如下:

/*@ normal_behavior

@ requirestransEntity !=null;

@ ensures (exists inti;0≤i&&i

@ also

@ exceptional_behavior

@ requires transEntity==null;

@ signals_only NullPointerException;

@ signals (NullPointerException) true;

@*/

}

public static TransRecord /*@ pure @*/findRecordByKey(/*@ nullable @*/ String token){}.

本文以查询操作为例,对数据模型中的findRecordBykey查询操作进行验证,验证结果的执行树如图14所示.

图14 findRecordBykey方法契约验证执行树

从图14可以看出:该方法的每一个节点图标均未出现交叉线.这表明执行成功,即该方法契约正确.同理,表明对数据模型中每一个方法契约进行验证,均成功执行,PayPal数据模型验证成功.

4.3.2 服务模型验证 基于模型驱动的Web服务不仅能对数据模型验证,而且也可对服务模型进行验证.同理,使用Radl-WS服务建模语言,关键代码如下:

setExpressCheckout:real→string

|[in sPaymentAmount:real;out result:string;]|

{Q:true}

{R:rec.token≠null∧ppdm.findRecordByKey(rec.token)=null}

{R:rec.payerInfo≠null∧rec.transAmount=sPaymentAmount∧result=rec.token }

{R:rec.paymentStatus=InProgress}

{R:ppdm′=ppdm.createRecord(rec)}.

由于篇幅原因,所以本文仅以setExpressCheckout服务为例来说明对服务模型的验证.首先将Radl-WS需要模型转换成的JML方法契约代码如下:

/*@ modifiesrec,URL,ppdm;

@ requiresURL!=null && URL==Checkout_URL;

@ ensures(rec.getToken() !=null) &&@(old(ppdm).findRecordByKey(rec.getToken())==null);

@ ensuresrec.getPayerInfo() !=null && rec.getTransAmount()==old(paymentAmount);

@ ensures (URL==success_URL &&rec.getPaymentStatus()=="InProgress")||

@ (URL==cancel_URL && rec.getPaymentStatus()=="Denied");

@ ensuresold(ppdm).createRecord(rec);

@ ensures esult==rec.getToken();

@ also

@ exceptional_behavior

@ requires URL==null;

@ signals_only NullPointerException;

@ signals (NullPointerException) true;

@*/

public String setExpressCheckout(int sPaymentAmount){}.

然后使用自动化工具对服务模型的方法契约进行验证,服务模型验证结果的执行树如图15所示.

图15 setExpressCheckout方法契约验证执行树

该工具图形界面显示方法在契约验证时会把细节显示在方框中.图15的契约节点处方框较大,可以从左侧节点层级目录中看出:该方法每个节点图标均未出现交叉线.这表明执行成功,即该方法契约正确.使用同样的方法对剩下的服务模型进行验证,执行结果均成功,这表明PayPal服务模型验证成功.

5 总结与展望

基于前期工作的研究,本文提出一种基于模型驱动的Web服务符号执行与验证方法,该方法是对基于模型驱动的3阶段转换生成Java代码进行符号执行测试与验证.本文提出了运用符号执行的方式对Web服务功能正确性进行验证,并采用基于Eclipse平台扩展的交互式符号执行调试器SED,使用自动化工具对结果检验,提高了Web服务开发的可靠性.

通过PayPal实例来展示本方法的实际效果.首先对3阶段转换生成的数据模型与服务模型的Java代码进行符号执行;在成功执行后,在Radl-WS服务建模语言的基础上,将Radl-WS语言描述的需求模型转换成JML方法契约,并将此加入Java代码中分别对数据模型及服务模型进行验证;在自动化工具的支持下,数据模型与服务模型的符号执行与验证均成功,这说明该方法有效、可靠.

基于本文工作与3阶段转换生成方法,计划将此方法扩展到对Web服务组合的测试与验证,以及在Web服务组合的基础上加上可交易服务,验证可交易的Web服务组合可靠性与正确性.