CAJ | 학술논문

字节码既是运行于虚拟机的解释指令,也是定义良好的中间表示,是当今网络软件和计算设备中广泛使用的重要技术.字节码验证可以提高相关软件的可信程度,同时为构造证明保持编译器提供中间表示支持,具有重要的实用价值和理论价值.虽然近年提出了一些用于字节码程序的逻辑系统,但由于字节码本身的特点,造成了抽象控制栈复杂、控制流结构信息不足,因而字节码程序的"模块化验证"依然是一个巨大的挑战,并没有得到有效解决.将FPCC(foundational proof-carrying code)方法引入中间表示字节码,借鉴汇编程序的验证方法,设计出一种逻辑系统,给出字节码程序运行环境BCM(ByteCode machine)的逻辑系统CBP (certifying bytecode program)定义,完成系统的合理性证明和一组代表性实例程序的模块化证明,并实现机器自动检查.该工作为字节码验证提供一种良好的解决方案,同时也向着构造证明保持编译器环境迈出了坚实的一步,还可以为广泛使用的基于虚拟机复杂网络应用程序的深刻理解和深入分析提供理论帮助.
자절마기시운행우허의궤적해석지령,야시정의량호적중간표시,시당금망락연건화계산설비중엄범사용적중요기술.자절마험증가이제고상관연건적가신정도,동시위구조증명보지편역기제공중간표시지지,구유중요적실용개치화이론개치.수연근년제출료일사용우자절마정서적라집계통,단유우자절마본신적특점,조성료추상공제잔복잡、공제류결구신식불족,인이자절마정서적"모괴화험증"의연시일개거대적도전,병몰유득도유효해결.장FPCC(foundational proof-carrying code)방법인입중간표시자절마,차감회편정서적험증방법,설계출일충라집계통,급출자절마정서운행배경BCM(ByteCode machine)적라집계통CBP (certifying bytecode program)정의,완성계통적합이성증명화일조대표성실례정서적모괴화증명,병실현궤기자동검사.해공작위자절마험증제공일충량호적해결방안,동시야향착구조증명보지편역기배경매출료견실적일보,환가이위엄범사용적기우허의궤복잡망락응용정서적심각리해화심입분석제공이론방조.