字节net虚拟主机

ISSN1000-9825,CODENRUXUEWE-mail:jos@iscas.
ac.
cnJournalofSoftware,Vol.
21,No.
2,February2010,pp.
305317http://www.
jos.
org.
cndoi:10.
3724/SP.
J.
1001.
2010.
03794Tel/Fax:+86-10-62562563byInstituteofSoftware,theChineseAcademyofSciences.
Allrightsreserved.
字节码虚拟机的构造和验证董渊+,任恺,王生原,张素琴(清华大学计算机科学与技术系,北京100084)ConstructionandCertificationofaBytecodeVirtualMachineDONGYuan+,RENKai,WANGSheng-Yuan,ZHANGSu-Qin(DepartmentofComputerScienceandTechnology,TsinghuaUniversity,Beijing100084,China)+Correspondingauthor:E-mail:dongyuan@tsinghua.
edu.
cnDongY,RenK,WangSY,ZhangSQ.
Constructionandcertificationofabytecodevirtualmachine.
JournalofSoftware,2010,21(2):305317.
http://www.
jos.
org.
cn/1000-9825/3794.
htmAbstract:Thispaperpresentsamethodtobuildandverifybytecodevirtualmachine.
Theformaldefinitionandtheoperationalsemanticsofabytecodevirtualmachine(BVM)aregiven.
CertVM(certifiedvirtualmachine)isimplementedwithX86assemblycode.
ItisprovedinthispaperthattheCertVMissatisfiedwiththeformaldefinitionofthebytecodemachinewithsimulationrelation.
ThevirtualmachineimplementationprogramiscertifiedintheCoqproofassistant.
Theproofismachinecheckable.
Thismethodguaranteesthatacertifiedbytecodeprogramwillrunonthecertifiedvirtualmachinewithoutstuckunlesshardwarefaults.
Thisworkdoesnotonlyprovideasolidtheoreticalfoundationforreasoningaboutvirtualmachine,butalsomakesanimportantadvancetowardbuildingthetrustworthysoftware.
Keywords:certifiedVM;modularcertification;bytecode;Hoare-stylelogic摘要:提出一种虚拟机构造和验证方案.
给出字节码程序运行环境BVM(bytecodevirtualmachine)的形式化定义;采用X86机器语言构造虚拟机CertVM(certifiedvirtualmachine);并证明该虚拟机实现符合相应程序规范并和BVM之间具有模拟关系.
利用辅助工具Coq给出证明,所有证明均可机器自动检查.
CertVM确保在硬件环境满足其语义规范的情况下,已验证的字节码程序能够在给定虚拟机环境中正常运行.
给出的方案不仅为虚拟机验证提供理论基础,而且为可信软件构造提供了一种有益的尝试.
关键词:已验证虚拟机;模块化验证;字节码;类Hoare逻辑中图法分类号:TP316文献标识码:A互联网和智能终端设备日益深入地渗透到日常生产和生活中的各个环节,如何验证这样的软件,确保程序正确、顺利地执行,成为大家普遍关注和深入研究的一个热点问题[1].
字节码(bytecode)及其虚拟机(virtualmachine)运行环境是其中最为重要的技术,很多现有研究工作集中在字节码程序验证上.
但是,虚拟机实现的可SupportedbytheNationalNaturalScienceFoundationofChinaunderGrantNos.
90818019,90816006(国家自然科学基金);theNationalHigh-TechResearchandDevelopmentPlanofChinaunderGrantNos.
2008AA01Z102,2009AA011902(国家高技术研究发展计划(863))Received2009-06-15;Revised2009-09-11;Accepted2009-12-07306JournalofSoftware软件学报Vol.
21,No.
2,February2010信问题也同样重要,因为即便是已验证字节码程序,一旦虚拟机出错依然无法正确运行.
而现实中虚拟机通常采用C/C++等语言实现,其中的缺陷屡见不鲜[2].
本文深入探讨字节码虚拟机的可信问题,给出一种可信虚拟机构造和验证方案,为可信软件运行环境的构造提供理论和技术支持.
1虚拟机验证的价值本文研究字节码程序运行环境——语言级虚拟机的验证问题.
这类虚拟机通常解释执行以JAVA字节码(Javabytecode)[3]和微软.
NETCIL[4]为代表的字节码程序,是目前大多数网络应用程序的运行环境.
随着程序形式化验证研究的深入开展,字节码程序验证成为一个得到广泛关注的话题.
从高级语言[5]和汇编语言[69,10]两个方面的验证研究发展趋势来看,都需要在中间表示层面进行深入、细致的研究工作,而字节码是最佳选择之一.
字节码验证可以大大提高相关软件的可信程度,具有相当大的实用价值.
将验证语言提高到字节码将带来验证效率方面的显著提升,同时可以为未来从高级语言到汇编语言的证明保持编译器构造提供中间语言的支持,为可信软件构造提供有力的理论和工具支持.
最初,针对JAVA字节码验证的主要研究工作集中于JVM内部检查器,目标是类型正确性,从而保证存储安全性(verifier)[11].
随着研究工作的深入,人们逐步认识到仅有类型安全检查远远不够,还需要进一步研究其他更多程序的性质.
近年来,人们提出大量用于字节码程序验证的逻辑系统,代表性研究工作包括:Quigley设计了一个用于字节码程序的类Hoare逻辑系统,证明了含有循环的程序片段[12];MRG项目主要着眼于程序资源,提出一种针对字节码的具有资源感知特征的操作语义,以及相应的逻辑系统[13];Bannwart和Muller提出一种支持对象、引用、方法和继承等面向对象特征的逻辑系统,用来证明类JAVA字节码[14];Benton提出一种组合逻辑系统,用于一种.
NETCIL的命令式语言子集,并给出纯手工证明[15].
特别值得一提的是字节码建模语言BML(bytecodemodelinglanguage)的研究工作[16].
该语言作为一种可理解的字节码程序规范,应用开发人员可用它在字节码层面书写程序标注,以规范字节码程序的行为功能;与之对应,JML语言提供JAVA源语言层面的规范描述.
该研究同时包含一个并不完整的JML到BML编译器,其局限性在于,证明检查仍然需要借助一个复杂的验证器.
此前我们提出一系列针对字节码程序的验证方法,实现了程序的模块化验证、对嵌套程序的支持[17]等.
虽然上述工作取得了大量成果,但是这些研究工作通常都没有考虑虚拟机运行环境实现本身的可信问题,所以即便是验证过的字节码程序,一旦虚拟机出错都将不能正确运行.
而现实中虚拟机实现中的错误屡见不鲜,因此,开展可信虚拟机构造研究是一个非常迫切的需求.
本文深入探讨虚拟机本身的验证问题,基于FPCC方法[18],采用汇编代码构造出一个可真实运行于Bochs模拟器[19]的虚拟机系统原型,使用证明辅助工具Coq[20]给出该虚拟机符合规范的证明.
所有证明均可以自动检查[21],为可信虚拟机的构造问题提供了一种良好的解决思路.
2字节码虚拟机BVM(bytecodevirturalmachine)本节定义字节码虚拟机BVM,支持类似于JAVA字节码和.
NETCIL的字节码子集BC/0(bytecodezero).
图1给出该机器可运行的程序实例.
本节给出虚拟机定义、BC/0指令操作语义.
董渊等:字节码虚拟机的构造和验证307;intfactor(){r=1;while(n!
=0){r=r*n;n=n1;}};methodfactor:Factorial,whileloopwithspecification{(p0,g0)};I1(instructionsequence1),entrypoint0pushc1;pushimmediatedata1|8pushc1;pushimmediatedata11popr;r=1|9binop;n12goto11;jumptotheendofwhileloop|10popn;savevariablen{(p3,g3)};I2,loopstarthere|{(p11,g11)};I33pushvr;pushvariabler|11pushvn;pushvarn4pushvn;pushvariablen|12pushc0;pushimm05binop*;r*n|13binop#;n#06popr;savevariabler|14brture3;conditionalgoto7pushvn;pushvariablen|15ret;functionretFig.
1Stack-Basedbytecodeprogramwithsourcecode(functionfactor)图1基于栈的字节码程序及其源代码(函数factor)2.
1虚拟机BVM的定义图2给出了虚拟机的定义.
BVM采用类似于JAVA虚拟机的双栈结构.
整个机器配置(machineconfiguration)称为"世界"W(world),包含只读的代码堆C(codeheap)、可修改的状态S(state)、函数调用栈Kc(callstack)和程序计数器pc(programcounter).
代码堆是代码标号f(labels)到指令序列I(instructionsequences)的部分映射,状态S包含内存堆H(memoryheap)和计算栈K(evaluationstack),函数调用栈Kc(callstack)存放函数调用的返回地址,程序计数器pc指向代码堆中的当前指令.
(World)W::=(C,S,Kc,pc)(State)S::=(H,K)(CodeHeap)C::={f→I}*(ProgCounter)pc::=n(CStack)Kc::=nil|f::Kc(EStack)K::=nil|w::K(Memory)H::={k→w}*(Word)w::=i(integers)(Labels)f,k::=n(natnums)(OprNum)m:(Command)c::=ι|ret|gotof(InstrSeq)I::=ι;I|ret|gotof(Instr)ι::=pushcw|pushvk|popk|binopm|unopm|btruef|callfFig.
2DefinitionofBVM图2BVM定义指令序列I定义为由跳转和返回指令结尾的一系列指令组成的片段,C[f]表示C中由f开始的一个指令序列.
用"点"来表示多元组中的组成部分,如S.
K表示状态S中的栈K.
(F{a→b})(x)表示对映射F赋值,使得F(a)=b,所有其余映射关系保持不变.
函数length()和max()用来获取栈K,Kc的有效长度和最大长度,valid表示有足够计算栈和函数调用栈空间,validRa表示函数调用栈中保存了合法的返回地址.
C[f],[]andgotoor;,[]and[1]ccfcfretffιι′====+CICIC(F{a→b})(x),if(),otherwisebxaFx=validKnKlength(K)+n≤max(K)validKnKclength(Kc)+n≤max(Kc)validRaKcf,Kc′,Kc=f::Kc′Fig.
3Definitionofrepresentation图3表示符号定义2.
2指令操作语义图4定义指令的操作语义,这里,Enable(c,Kc,S)是每一条指令c可以执行的最弱前条件,NextKc(c,pc,S)关系308JournalofSoftware软件学报Vol.
21,No.
2,February2010定义pc所指指令执行后的函数调用栈Kc的变化,NextS(c,pc,Kc)关系定义pc所指指令执行后的状态S的变化,NextPC(c,S,Kc)表示状态S、调用栈Kc时c指令执行导致的pc变化.
程序执行通过机器配置W的逐步转化来刻画,即W→W′是通过pc所指指令的执行而实现.
NextS(c,pc,Kc)S′S′′whereS′=(H,K)ifc=ifEnable(c,Kc,S)=thenS′=pushcwvalidK0K(H,w::K)pushvkvalidK0KandH(k)=w(H,w::K)popkK=w::K′(H{k→w},K′)binopbopK=w1::w2::K′,w=bop(w1,w2)(H,w::K′)unopuopK=w1::K′,w=uop(w1)(H,w::K′)brtruefK=w::K′,w=TrueorFalse(H,K′)callfvalidKc1Kc(H,K)retvalidRaKc(H,K)……(H,K)NextKc(c,pc,S′)KcKc′whereS=(H,K)ifc=ifEnable(c,Kc,S)=thenKc′=callfvalidKc1Kc(pc+1)::KcretvalidRaKcKc′……KcNextPC(c,S,Kc)pcpc′whereS=(H,K)ifc=ifEnable(c,Kc,S)=thenpc′=brtruefK=w::K′w=TruefK=w::K′w=Falsepc+1callfvalidKc1KcfretvalidRaKc∧Kc=f::Kc′fgotoff……pc+1()cpcEnableccNextScpccNextKccpcccNextPCccpcpcpccpccpc′′′=′′′→CKSKSSSKKSKCSKCSKFig.
4OperationalsemanticsofBVM图4BVM机器操作语义3虚拟机构造和验证本文主要工作是采用形式化验证的软件构造方案,给出一种CertVM虚拟机的实现和证明.
CertVM采用X86汇编代码实现,可运行于Bochs模拟器,采用SCAP逻辑系统[6]证明该虚拟机符合上一节所给出的语义,证明实现代码则使用Coq完成.
本节首先给出CertVM虚拟机的实现,接着讨论运行环境——X86实模式的形式化定义,然后简单介绍证明CertVM所采用的逻辑系统,最后着重讨论如何证明模拟关系.

3.
1虚拟机的构造我们采用X86实模式汇编实现了虚拟机CertVM字节码解释执行和加载等通常语言级虚拟机最为核心的功能部件,暂未考虑垃圾回收、即时编译等运行时优化功能,也不考虑检查器.

董渊等:字节码虚拟机的构造和验证309内存分配:字节码虚拟机CertVM的只读代码堆(C)、内存堆(H)、计算栈(K)和函数调用栈(Kc)在X86汇编实现中均采用数组表示,即内存中一段连续的空间.
我们分别用符号,,MMMCHK和来表示这些数组.
我们定义函数base()和max()来描述这些数组基地址和数组上界.
定义top()函数来获取K和Kc的栈顶指针(sp,csp)cMK的位置.
栈顶指针(sp,csp)和程序计数器(pc)等在X86汇编中实现为变量.
字节码加载:字节码加载器(loader)是用来加载一段字节码程序的.
它进行如下一系列的操作:把字节码程序加载到只读代码堆MC;初始化内存堆MH(即清零),将计算栈MK清空(栈指针置底);将当前程序作为顶层函数,其返回值的地址设为1(0xFF),因此函数调用栈被清空,压入1到栈底;最后将pc指向字节码程序的cMK入口处,程序转入取值执行阶段.
执行机制:字节码程序的每条指令都是通过一系列的X86汇编代码模拟执行.
每条指令的模拟执行都需要经过4个阶段:取指、译码、分配和解释运行.
虚拟机在取指阶段主要利用pc值在得到当前待模拟的字节CM码指令.
在译码阶段,虚拟机分析并判断待模拟指令的类型.
然后在分配阶段,通过查询分配表跳转到该指令类型对应的解释代码.
最后在解释运行阶段,完成这条指令的解释运行.
需要注意的是,对于不同的字节码指令,其取值、译码和分配阶段相应的X86代码完全相同,只有在解释运行阶段的X86代码才有区别.
图5给出goto指令相应的X86解释代码.
其中,标号fetch,decode,dispatch和goto分别对应了字节码goto指令的取指、译码、分配和解释运行4阶段的X86实现.
;PartoftheimplementationofBVM{(pfetch,gfetch)};bytecodefetch11addw%ax,%bx;offsetforcurrentbytecode1fetch:12addw%ax,%bx;entrypointis2wordlong2movw(pc),%ax;bytecodeprogramcounter13movw(%bx),%ax;getentrypoint3cmpw$0xFF,%ax;raoftoplevelfunction14jmpw*%ax;jumptoentrypoint4jefetch;loopaftertopfunction{(pgoto,ggoto)}5decode:;bytecodedecode15goto:;bytecodeexecution6movw$code,%bx;bytecodebaseaddress16movw(pc),%ax;codepoint7addw%ax,%bx;currentbytecodeaddress17movw$code,%bx;bytecodebaseaddress8movw(%bx),%ax;bytecodefetchi.
f18movw2(%bx),%cx;operandfetchi.
a{(pdispatch,gdispatch)}19addw%cx,%cx;eachinstructionis4bytes9dispatch:;pushvariablen20addw%cx,%cx10movw$table,%bx;baseofdispatchtable21jmpfetchFig.
5FragmentofCertVMimplementation,instructiongoto图5CertVM实现代码片段,goto指令3.
2X86机器定义和SCAP逻辑系统本文采用SCAP逻辑系统来证明字节码虚拟机CertVM的汇编代码实现,本节给出SCAP系统的简单介绍.
该系统采用(p,g)规范描述函数功能,支持X86汇编代码的模块化验证,具有很强的表达能力.
这里简单给出SCAP系统相关的X86机器定义、指令操作语义、推理规则和合理性证明.
SCAP系统给出一种形式化的保证,硬件满足其语义规范的情况下,通过证明的程序将不会进入滞留状态,而且符合其相应的程序规范.

3.
2.
1X86机器定义图6给出了对X86机器状态的形式化定义.
类似于BVM,整个机器配置(machineconfiguration)也称为"世界"W(world).
不同的是,世界中主要包含只读的代码堆C(codeheap)、可修改的状态S(state)和程序计数器pc(programcounter).
其中,可修改的状态S由内存堆H(memoryheap)、通用寄存器R(generalregister)和标志寄存器zf(flagregister)组成.
此定义对X86进行了简化,只包含虚拟机代码中使用的4个通用寄存器.
类似于BVM,图7定义了X86指令的操作语义.
NextS(c,pc)关系定义pc所指指令执行后的状态变化,NextPC(c,S)表示c指令执行导致的pc变化.
其中,eval(o)表示对操作数o求值.
程序执行通过机器配置W的逐步转化来刻画,即W→W′是通过pc所指指令的执行而实现.
310JournalofSoftware软件学报Vol.
21,No.
2,February2010fpcn(World)Flag)::false|true(CodeHeap)Label)natnums)(State)Word)::(integers)(Heap)Register)(RegFile)::{pczfflzfwilwraxbxcxdx===→====→==WCSCISHRHR}*(Address)(Command)::|jmp|jmpw(Operator)::|(InstrSeq)jmp|jmpw(Instr)::mov,|ld,|st,|cmp,|add,|sub,|jerwallrcfrowrfroraroaorororfιιι→=====IIFig.
6DefinitionofX86machine图6X86机器的定义NextS(c,pc)SS″whereS=(H,R,zf)ifc=ifEnable(c,S,pc)=thenS″=movo,rw=eval(o)(H,R{r→w},zf)lda,rl=eval(a)∧l∈dom(H)∧H[l]=w(H,R{r→w},zf)sto,al=eval(a)∧l∈dom(H)∧w=eval(o)(H{l→w},R,zf)cmpo,rw=eval(o)(H,R,true)ifw=R(r);(H,R,false)othersaddo,rw=R(r)+eval(o)(H,R{r→w},zf)subo,rw=R(r)eval(o)(H,R{r→w},zf)…(H,R,zf)NextPC(c,S)pcpc′whereS=(H,R,zf)ifc=thenpc′=jeff,ifzf=true;pc+1,othersjmpffjmpwrR(r)…pc+1()cpcEnablecpcNextScpcNextPCcpcpcpcpcpc′′=′′→CSSSSCSCSFig.
7OperationalsemanticsofX86machine图7X86机器操作语义定义3.
2.
2SCAP规范介绍SCAP直接使用Coq证明辅助工具的内嵌逻辑作为程序规范书写语言.
该逻辑是一种使用归纳定义的高阶谓词逻辑.
SCAP系统是基于程序规范(programspecification,又称断言)进行推理的.
程序员在每个指令序列开始处插入断言(程序规范)s来规定程序执行需要满足的条件.
SCAP程序规范是谓词二元组(p,g),插入断言之后的代码如图5所示,图中的大括号即给出程序规范.
谓词p描述程序入口状态S的性质,谓词g描述两个程序状态之间的关系,Coq中的p,g均定义为返回值为命题的函数,分别以S和两个S为参数.
我们使用p来描述当前状态的前条件,使用g来描述程序当前点与函数返回点(出口)之间的状态变化(即程序行为).
图8给出SCAP规范的形式定义.
图7中Enable(c,S,pc)就是一个谓词p,而NextS(c,pc)就是一个谓词g.
11(Pred)(Guarantee)(Spec)MPred)(CdHpSpec)nnpStatePropgStateStatePropspgmMemoryPropfsfsΨ→∈∈=→∈=→→Fig.
8SpecificationconstructorsforSCAP图8SCAP的规范构造符董渊等:字节码虚拟机的构造和验证311同时,我们定义基于SCAP规范的一系列运算,如图9所示.
这些运算能够从简单的程序规范出发,构造更复杂、语义更丰富的程序规范.
000,,,ppgpgpggpppppgpgggggggggλλλ′′′′′′→∧′DDSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS′Fig.
9Constructorsforpandg图9p,g构造符3.
2.
3SCAP系统介绍SCAP系统类似于Hoare逻辑[22],通过一系列的推理规则来证明每个程序点满足相应的程序规范.
能够满足所有的规范的程序被称作良型程序或良型世界,表述如下:Ψ6{s}W(WLD,良型世界)Ψ6C:Ψ′(CDHP,良型代码堆)Ψ6{s}I(良型代码序列)证明程序良型性的推理规则如图10所示.
1212(WLD)(CDHP)::#(LINK){jmp,jmpw,je}1:()((spcpcsspcfssffspcspcpgpcpgpgppggιιιΨΨΨΨΨΨΨΨΨΨΨΨΨΨΨιΨ′′′′∈′′′′+′′666666666DDCCSCSCCSCCCCCSIjejejeje))(SEQ)1:(JE)je;TTFFgpgpcfpgpgpcpgppgggpgppgggpgpcffpgppΨιΨΨΨΨ∈+′′′′′′′′′∈66DDDD6IIIje(je,_)je(j()(JMP)jmp(JMPW)jmpw,.
(where.
true),.
TFpggpgpcfrffpgpppggpgpcrgNextSzfgNextSΨΨΨλλ′′′′′=∈′′′=′D6D6RSSSSSSSe,_)(,_)(where.
false),.
(forallother)cczfgNextScλ′′=′′SSSSSSSFig.
10SCAPinferencerules图10SCAP的推理规则程序不变量:WLD规则中描述一个程序满足良型性(well-formedness)的所有前提:根据CDHP规则,代码堆C是良型的(well-formed).
当前模块对内规范Ψ是对外规范Ψ′的子集,Ψ中包含C所使用到的位于其他代码块的被调用接口规范,Ψ′还包含本模块定义以及将被其他模块调用的接口说明.
当前pc所对应的规范s在Ψ中,因此当前指令序列C[pc]关于规范s是良型的.
给定外部规范集Ψ′,当前状态S应满足断言s.
312JournalofSoftware软件学报Vol.
21,No.
2,February2010推理规则所用符号定义如图9.
谓词pgι描述p满足初始状态并经过状态转移gι后的结果,它是状态转移gι的最强后条件.
两个连续状态转移g和g′的组合用g°g′来表示,p°g表示在g的基础上已知p得到满足.

程序模块:在CDHP规则中,每个模块是由至少1个指令序列组成的小代码堆,每个模块的规范不仅包含当前模块内部代码块的规范,还包含了所有可能被该模块调用的其他代码块的规范,因此,SCAP逻辑支持各个程序模块的独立验证.
每个独立模块的良型性通过CDHP规则定义,多个互不重叠的良型模块通过LINK规则链接起来.
WLD规则保证所有良型模块能够链接成为一个全局良型代码堆.
指令序列:类似于传统Hoare逻辑,SCAP采用前、后条件作为程序规范.
SEQ规则是对每个以顺序指令ι(不含条件跳转和函数调用指令)开始序列的判定形式.
它描述在给定内部规范Ψ和满足前条件(p,g)的情况下执行以当前pc开始的指令序列是安全的.
程序员需要找到一个中间规范(p″,g″),使剩余指令序列得到满足,该规范同时也作为当前指令的后条件.
gι用来描述执行指令ι所引起的状态转移,具体定义如图7所示.
对于顺序指令而言,NextS不依赖于当前pc值,因此用"_"表示任意pc.
找到合适的中间规范(p″,g″)后,检查SEQ规则中的4个条件以确定该指令序列的良型性.
第1个前提表明剩余指令序列在该中间规范下是良型的;第2个前提表明,pgι检查只要初始状态满足p,状态转移gι就可以完成;第3个前提表示,如果当前状态满足p,那么在状态转移gι后,新状态满足p″.
最后一个前提描述在当前状态满足p的情况下,gι和g″的组合能够满足g.
其他指令:条件跳转指令跳转成功与否依赖于其判定条件是否得到满足,因此,JE规则中使用gjeT和gjeF来表示不同的执行情况.
无条件跳转指令可以安全执行的充分必要条件是当前断言能够蕴含目标代码处的断言,它可以看作是条件跳转je的特例.
SCAP的完备性:基于前进性和保持性引理,SCAP的完备性保证只要初始状态满足WLD规则中定义的程序不变量,整个程序就永远不会陷入滞留状态.
程序运行过程中永远满足该不变量.
该不变量还可以蕴含部分正确性等更多程序性质.
SCAP推理规则同时保证程序满足jmp或jmpw指令跳转目标地址处的规范,也满足程序模块边界处的规范.
关于SCAP更进一步的信息参见文献[6].
引理2.
1(CBPprogress).
如果Ψ6{s}W,则存在世界W′,使得W→W′.
引理2.
2(CBPpreservation).
如果Ψ6{s}W,并且W→W′,则存在s′,使得Ψ6{s′}W′.
3.
3虚拟机验证3.
3.
1模拟关系定义对于任意字节码虚拟机BVM的世界W=(C,(H,K),Kc,pc),模拟运行W的X86机器需要将W保存在其内存堆中.
保存在内存堆的信息维护了两个层次之间的模拟关系.
为了能够正确模拟运行W,X86模拟程序必须保证在解释运行每一条字节码指令时,内存堆中的模拟关系信息能够完整保持,同时正确执行前文所述的4个阶段.
令X86机器在SCAP框架中表示为世界Wx=(Cx,(Hx,Rx,zf),pcx),则在每解释一条字节码指令之前,W和Wx之间存在着如下的模拟关系~:fetch(,)(SIM).
xVMxxxpcsim==CCWHWW代码堆Cx中的代码必须是CertVM的代码;程序计数器pc必须指向CertVM取指阶段程序的入口;字节码虚拟机世界W的信息必须被保存到Hx中,维持相应的内存模拟关系(详细内容见下文);对于通用寄存器Rx和标志寄存器zfx没有限制.
3.
3.
2内存模拟关系如前文所述,在X86机器的内存堆Hx中,数组,,MMMCHK和分别保存了BVM的C,H,K和Kc.
除此之cMK董渊等:字节码虚拟机的构造和验证313外,我们还用数组Mp保存指针pc,cps和sp.
因此,内存模拟关系sim(W,Hx)形式的定义为(,)xxcsimMpMMMMM=KKCHWHHO,其中,表示内存之间非重叠的合并关系,即当且仅当domH1∩domH2=,才有H1H2=H1∪H2.
而MO表示M中其他剩余内存空间.
字节码指令保存在MC中,每条指令长度为4字节,MC定义为Hx中一段连续内存.
对于C的任意合法标号f(f∈dom(C)),指令C[f]保存在MC[f*4]=Hx[base(MC)+f*4]的内存块.
类似地,计算栈K、内存堆H和函数调用栈Kc的每一项在Hx中保存时,每项占2字节.
其中,Mp中保存pc,cps和sp,每个占2字节,分别保存在Mp[0],Mp[2]以及Mp[4]起始的内存中.
下面给出这些数组的具体定义:max()4],2],2]max()2],6].
xxcxccxpxpMbaseMbaseMMbaseMbaseMlengthMbaseMbaseMlengthcMbaseMbaseMMbaseMpbaseM+*+*+*+*+CCCKKKKKKHHHHCHKHKHHH,3.
3.
3虚拟机良型性定义通过模拟关系给出良型虚拟机(well-formedvirtualmachine)的定义:一个良型的虚拟机WFVM(W,Wx),对于任意字节码世界W,存在对应的X86世界Wx满足W~Wx;并且若有字节码世界W′且W→W′,那么存在x′W满足W′~x′W且n,Wx→nx′W.
图11表述了这一定义.
Fig.
11Illustrationofwell-formedvirtualmachine图11良型虚拟机的表示从良型虚拟机的定义可知,任意一条字节码指令的执行必须严格对应一段X86程序,并且在这段X86程序的入口和出口都必须严格满足模拟关系.
为了利用SCAP框架证明虚拟机的良型性,我们需要利用SCAP的程序规范来描述良型虚拟机需要满足的性质.
从前文的虚拟机执行机制可知,这段X86程序恰好就是虚拟执行的4个阶段.
因此,每一条字节码指令对应的X86程序片段的入口一定是fetch(如图5所示的实例).
定义fetch处程序规范(pfetch,gfetch)为fetchfetchwherexxxxxxxxxpsimEnablecccpccpcgsimsimλλ→∧∧SWWSHSKWCSKCSSWWWWWSHWSH其中,pfetch描述在进入fetch之前,X86世界的内存堆中必须维持某个字节码世界的模拟关系,并且要求这个字节码世界是可以运行的(也就是存在下一个状态).
第1次进入fetch时,X86内存堆中必定保存着字节码程序的最初始状态;gfetch保证执行完解释程序后,其出口状态x′S能由入口状态Sx严格推出,即x′S保存了S所模拟字节码世界后续状态的模拟关系.
一旦解释执行完一条字节码指令时,程序就返回到fetch入口,此时的状态Sx必又能满足pfetch.
因此,要完成整个虚拟程序的验证工作,我们只需要利用SCAP框架对每一条字节码指令分别证明其对应的CertVM实现代码满足如下性质:WpopfWxloadr5spstorefr5sp1W′x′W314JournalofSoftware软件学报Vol.
21,No.
2,February2010),=Ψcvm6{(pfetch,gfetch)}fetch:CVM[fetch].
4程序实例和实现本文第3节图5介绍的X86程序实例是对字节码指令goto进行解释执行.
本节将以这段程序为例,展示CertVM的证明过程.
4.
1验证步骤介绍划分指令序列:划分指令序列是验证工作的第1步,正确的划分才能够确保证明过程.
根据图6中对指令序列I的定义,整个代码片段能够自然地化成两个部分:fetch和goto标号所指向的程序块(fetch段从第1行开始到第14行结束,而goto段为第15行~第21行).
其中,fetch段代码是不同字节码指令解释程序所共用的,所以一旦证明,就可以被复用.
程序规范建立:程序员需要给出代码堆规范Ψ,即从指令标号f到代码断言s(即(p,g)二元组)的映射,我们将SCAP规范内嵌在X86汇编代码中,即见图5中花括号部分.
根据推理规则,需要给出以下位置的代码断言:每一个指令序列的开头、跳转指令(包括jmp和je)的目标位置.
在此段程序中,我们只需要在fetch和goto标号处加入程序规范.
由前文分析可知,fetch处的程序规范主要保证模拟关系,这里不再赘述.
goto入口处需要满足当前字节码世界pc所指的指令为goto类型即可.
程序规范的形式定义见图12.
定义中,默认W=(C,(H,K),Kc,pc)且Sx=(Hx,Rx,zf).
其中,pdispatch为中间断言,后文将解释.
type函数是一个把字节码指令类型映射到自然数的函数.
而Tgoto则为字节码goto所映射的自然数.

gotogotodispatchgotoftechdispatchftechwhere(),where(,.
xxxxxxxpsimEnablecctypecTcpcpsimEnableccaxtypeccpcggggλλ∧∧===SWWSHSKCSWWSHSKRCFig.
12SpecificationfortheX86implementationofbytecodeinstructiongoto图12字节码goto指令X86解释执行代码的示例规范验证并连接:为了检查一个以指令ι开始序列的良型性,程序员需要寻找恰当的中间断言(即是当前指令ι的后条件,又是后续指令序列的前条件),并选用相应推理规则完成指令ι的证明.
一个简单的例子是,在dispatch标号处可以加入图12中所定义的断言(pdispatch,gdispatch).
这个断言表示在取指译码完成之后,X86程序正确地获得字节码世界W中pc所指向指令的类型,并将类型信息保存在寄存器ax中.
完成指令证明之后,程序员使用CDHP规则建立各个独立指令序列的良型性证明,多个互不重叠的良型代码片段可以用LINK规则连接在一起,最后,应用WLD规则把所有代码片段连接并构成全局良型代码堆.
4.
2验证实现本文采用Coq证明辅助工具来实现逻辑系统和上述实例程序的证明,所有的定义和证明都可以机器自动检查.
给出了BVM及其操作语义、X86机器及其操作语义、SCAP逻辑系统和CertVM实现及其证明的形式化表示.
字节码和X86语法采用Coq的归纳定义给出,相应的操作语义和所有的SCAP推理规则都定义为归纳关系,逻辑系统的合理性证明则根据语法方式进行形式化和证明,同时还给出CertVM实现程序实例的形式化描述和证明.
所有证明实现约14000行的Coq代码,花费数个人月.
其中,接近1/6分的工作在于一些基本工具的实现,包括关于映射与分离逻辑的引理和策略.
这些通用工具独立于本逻辑系统以及验证实例,部分内容重用自以往相关项目中并加以适当修改.
其中,3200多行定义字节码机器及其操作语义,2700多行定义X86机器及其操作语义、SCAP推理规则定义及其完备性证明,另外约1800行是CertVM实现的内存映射和机器状态模拟关系董渊等:字节码虚拟机的构造和验证315定义.
本文中图5对应实例的证明超过3200行,且CertVM实例直接由X86汇编代码开发.
事实上,SCAP系统同样可用于人工优化过的程序以及优化编译工具自动生成代码的证明.
程序验证实践表明,编写程序规范依赖于程序员,其难度取决于所感兴趣的程序性质以及算法本身的复杂性.
只要给出程序规范,程序证明书写就相对比较简单.
对于本文虚拟机CertVM的证明,其程序规范由字节码操作语义和状态之间的模拟关系共同确定,而字节码的操作语义比较容易给出.
因此,只要确定字节码状态和相应X86机器状态之间的模拟关系,就可以很方便地给出程序规范,进而完成证明实现.
Table1Coqproofcodestatistic表1Coq证明代码统计LinesofproofcodeNumberTypeValuePercent1Basiccoqlacticlibrary235417.
52Bytecodevirtualmachinedefinition328524.
43X86machinedefinitionandSCAPlogic270620.
14CertVMmemorylayoutandSPECrelations186413.
85ProofcodeofCertVMexample325824.
2Total134671004.
3未来扩展研究初步完成虚拟机的构造和验证之后,还将进一步结合以往字节码程序验证的工作基础,建立一套完整的逻辑系统,将已验证的字节码程序和已验证虚拟机有机地结合起来,确保硬件环境满足其语义规范的情况下,已验证的字节码程序能够在已验证虚拟机环境中正常运行,建立完整的已验证计算环境.

目前,本文的字节码子集只针对最关键的控制栈和非结构化控制流,因此只包含其中的关键指令,后续将扩展支持更多的语言特征.
系统首先要扩展的是对象、引用、方法和继承等面向对象特征,以便更好地体现当今字节码程序的发展趋势和使用情况.
另外,提供例外处理支持是一个直接的扩展工作,采用类似于函数调用/返回的思路,加入例外支持应该比较容易.
并发程序验证支持是又一个值得深入探讨的热点问题,随着多核处理器的发展而更加突出,即便是广泛使用的并发程序库,比如JDK同步类等,也存在一系列缺陷[23].
引入上述特征之后,将进一步完成对应特征的X86汇编实现和对应的证明实现.
这些扩展工作的主要难度将在于相应的操作语义定义以及X86实现的模拟关系建立.
此外,证明过程中引入更多的自动技术以提高验证效率,也是一个需要深入研究的方向.
5结束语与本文CertVM验证工作相关的研究包括一系列针对字节码、虚拟机的形式化描述和检查方面的工作.
近年来提出的大量用于字节码程序验证的逻辑系统[12,1416]以及我们提出的字节码程序模块化验证和嵌套字节码程序的验证[17]等工作,都没有考虑虚拟机运行环境实现本身的可信问题.
本文则深入探讨虚拟机本身的可信问题,采用汇编代码构造出一个可真实运行的虚拟机系统原型,并利用FPCC方法证明该实现符合字节码操作语义.
Fong等人的可运行FJVM系统模型[24]等工作提供了一系列可用于新语言特性研究的VM模型,我们则不仅形式化地给出一个虚拟机模型,而且构造相应的可执行代码实现并给出完整证明.
Klein和Nipkow深入研究了一种类JAVA语言及相应虚拟机、编译器的模型[25],给出了类JAVA语言和相应JinjaVM执行之间的模拟关系证明,但是没有回答如何确保JinjaVM实现符合其规范这一重要问题,本文的CertVM则通过形式化证明的方案给出了"VM实现是否符合规范"这一问题的确切回答.
本文基于FPCC方法构造出一个符合字节码语义规范的虚拟机原型系统.
给出字节码操作语义和运行环境X86机器的形式化定义,利用SCAP逻辑系统证明虚拟机实现和字节码程序之间模拟关系证明,并利用辅助工具Coq给出证明,所有证明均可机器自动检查.
本系统能够确保只要字节码程序能够在给虚拟机CertVM中正常运行,其执行结果就符合字节码操作语义定义.
本文的工作采用程序验证手段构造字节码程序的可信运行环境,为广泛使用的一类复杂网络应用程序的316JournalofSoftware软件学报Vol.
21,No.
2,February2010深刻理解、深入分析和准确验证提供理论帮助,同时为可信软件构造问题的解决提供了一种良好的思路.

致谢在此,我们向对本文工作给予建议的同行,特别是Yale大学的ZhongShao教授、TTI-Chicago的XinyuFeng博士和Lehigh大学的GangTan博士等人表示感谢.
感谢论文评审专家的宝贵意见,感谢北京大学梅宏教授和国防科学技术大学王戟教授在NASAC2009会议上关于可信的讨论和建议.
References:[1]HoareT.
Theverifyingcompiler:Agrandchallengeforcomputingresearch.
In:Proc.
ofthe2003Int'lConf.
onCompilerConstruction(CC2003).
LNCS2622,Heidelberg:Springer-Verlag,2003.
262272.
[2]http://bugs.
sun.
com/bugdatabase/top25_bugs.
do[3]LindholmT,YellinF.
TheJavaVirtualMachineSpecification.
2nded.
,Boston:Addison-WesleyPublishingCompany,1999.
[4]InformationTechnologyCommonLanguageInfrastructure(CLI).
ISO/IEC23271:2006,2006.
http://standards.
iso.
org/ittf/PubliclyAvailableStandards/index.
html[5]vonOheimbD.
HoarelogicforJavainIsabelle/HOL.
ConcurrencyandComputation:PracticeandExperience,2001,13(13):11731214.
[6]FengXY,ShaoZ,VaynbergA,XiangS,NiZZ.
Modularverificationofassemblycodewithstack-basedcontrolabstractions.
In:Proc.
oftheProgrammingLanguagesDesignandImplementation(PLDI2006).
NewYork:ACMPress,2006.
401414.
[7]FengXY,ShaoZ,DongY,GuoY.
Certifyinglow-levelprogramswithhardwareinterruptsandpreemptivethreads.
In:Proc.
oftheProgrammingLanguagesDesignandImpl.
(PLDI2008).
NewYork:ACMPress,2008.
170182.
[8]WangSY,LiangYY,DongY.
VerificationofconcurrentassemblyprogramswithaPetrinetbasedsafetypolicy.
TsinghuaScienceandTechnology,2007,12(6):684690.
[9]ZhuYM,ZhangLW,WangSY,DongY,ZhangSQ.
Verifyingparallellow-levelprogramsformulti-coreprocessor.
ActaElectronicaSinica,2009,37(z1):1–6(inChinesewithEnglishabstract).
[10]GuoY,ChenYY,LinCX.
Amethodforcodesafetyproofconstruction.
JournalofSoftware,2008,19(10):27202727(inChinesewithEnglishabstract).
http://www.
jos.
org.
cn/1000-9825/19/2720.
htm[11]LeroyX.
BytecodeverificationforJavasmartcard.
SoftwarePractice&Experience,2002,32(4):319340.
[12]QuigleyCL.
AprogramminglogicforJavabytecodeprograms.
In:Proc.
ofthe16thInt'lConf.
onTheoremProvinginHigher-OrderLogics(TPHOLs2003).
Berlin:Springer-Verlag,2003.
4154.
[13]AspinallD,BeringerL,HofmannM,LoidlHW,MomiglianoA.
Aprogramlogicforresourceverification.
In:Proc.
oftheTPHOLs2004.
Berlin:Springer-Verlag,2004.
411445.
http://portal.
acm.
org/citation.
cfmid=1321978[14]BannwartF,MullerP.
Aprogramlogicforbytecode.
ElectronicNotesinTheoreticalComputerScience,2005,141(1):255273.
[15]BentonN.
Atyped,compositionallogicforastack-basedabstractmachine.
In:Proc.
ofthe3rdAsianSymp.
onProgrammingLanguagesandSystems(APLAS).
LNCS3780,Berlin:Springer-Verlag,2005.
364380.
[16]BurdyL,PavlovaM.
Javabytecodespecificationandverification.
In:Proc.
oftheSAC2006.
NewYork:ACMPress,2006.
1835–1839.
http://portal.
acm.
org/citation.
cfmid=1141277.
1141708[17]DongY,WangSY,ZhangLW,YangP.
Modularcertificationoflow-levelintermediaterepresentationprograms.
In:Proc.
ofthe33rdAnnualIEEEInt'lComputerSoftwareandApplicationsConf.
(COMPSAC2009).
Washington:IEEEComputerSocietyPress,2009.
563570.
http://dblp.
uni-trier.
de/rec/bibtex/conf/compsac/DongWZY09[18]AppelAW.
Foundationalproof-carryingcode.
In:Proc.
ofthe16thIEEESymp.
onLogicinComputerScience.
Washington:IEEEComputerSocietyPress,2001.
247258.
http://portal.
acm.
org/citation.
cfmid=871860[19]LawtonK,DenneyB,GuarneriND,RuppertV,BothamyC.
Bochsusermanual.
2009.
http://bochs.
sourceforge.
net/[20]CoqDevelopmentTeam.
TheCoqproofassistantreferencemanual.
TheCoqreleasev8.
1,2006.
[21]http://soft.
cs.
tsinghua.
edu.
cn/dongyuan/~dongyuan/verify/certvm.
html[22]HoareCAR.
Anaxiomaticbasisforcomputerprogramming.
CommunicationsoftheACM,1969,26(1):5356.
[23]SenK.
Racedirectedrandomizeddynamicanalysisofconcurrentprograms.
In:Proc.
oftheProgrammingLanguagesDesignandImplementation(PLDI2008).
NewYork:ACMPress,2008.
1121.
董渊等:字节码虚拟机的构造和验证317[24]FongPWL.
ReasoningaboutsafetypropertiesinaJVM-likeenvironment.
ScienceofComputerProgramming,2007,67(2-3):278300.
[25]KleinG,NipkowT.
Amachine-checkedmodelforaJava-likelanguage,virtualmachine,andcompiler.
ACMTrans.
onProgrammingLanguagesandSystems,2006,28(4):619695.
附中文参考文献:[9]朱允敏,张丽伟,王生原,董渊,张素琴.
面向多核处理器的低级并行程序验证.
电子学报,2009,37(z1):1–6[10]郭宇,陈意云,林春晓.
一种构造代码安全性证明的方法.
软件学报,2008,19(10):27202727.