一种可动态部署规则的Java程序运行时验证系统

摘要

本发明一种可动态部署规则的Java程序运行时验证系统，该系统运行于DiSL字节码注入框架之上，包括验证规则翻译器、部署管理器以及运行时引擎三个模块，所述验证规则翻译器用于将验证规则定义文件翻译成由事件注入代码和规则验证代码组合成验证代码，所述部署管理器用于提供部署验证代码的相关用户接口；所述运行时引擎用于根据接收的验证代码中事件注入代码产生的事件序列，为每个监控对象维护一个事件序列，验证事件注入代码产生的事件序列是否与规则验证代码的事件序列相同，并根据验证情况通过部署管理器对事件注入代码进行实时部署优化。本发明根据运行时验证结果对代码注入进行动态优化，有效降低了验证系统的性能开销。

说明书

技术领域

本发明涉及运行时程序验证领域，具体是一种可以将规则动态部署的针对 Java程序的运行时验证系统。

背景技术

程序验证技术对于保证程序的正确性起着关键性作用。程序验证技术主要 包括传统的静态程序验证技术和运行时程序验证技术，两者的不同在于开展验 证过程的时机。传统的静态程序验证技术包括模型检测和定理证明，旨在对于 整个系统进行形式化建模验证，其主要缺点在于静态方法导致的状态空间爆炸， 使得其不具备可扩展性，无法对大型系统进行验证。运行时程序验证技术则只 关注程序的具体执行路径是否满足具体的特性，大大减少了验证空间，使得程 序验证变得真正可行。

运行时程序验证分为三步，首先通过用户定义或者程序挖掘得到规则描述， 然后验证系统根据规则通过自动或手动注入代码获取到相关事件，最后验证系 统根据规则对产生的事件系列进行验证，以检测目标系统是否违背规则。

近年来运行时程序验证受到了越来越多的关注，有大量技术被开发出来， 主要集中在解决第一步规则描述和第三步验证过程中的问题。

对于第一步，现有技术解决的问题主要是如何增强规则描述语法的表达能 力，从而使得规则描述更加简单。现有的描述语法包括：有限状态机模型(FSM)、 上下文无关文法(CFG)、扩展正则表达式(ERE)和线性时序逻辑(LTL)等等， 已经能够很好地表达各种基本事件序列规则和含参事件序列规则。

对于第三步，现有技术解决的问题主要是如何在产生较小性能开销的前提 下完成验证工作。具体的技术有结合静态分析优化注入代码、对监控对象进行 采用更好的垃圾回收机制等等，现有的技术已经能够做到在较低的资源耗费下 对单个规则进行验证，但多个规则同时验证仍需耗费大量资源。

然而，现有技术对如第二步的探索很少，大部分技术依赖于传统的注入工 具，例如AspectJ来注入代码，使得现有验证系统有如下缺点：(1)无法在运 行时动态部署验证规则(2)无法针对验证结果进行动态注入优化。

通过检索发现，瑞士卢加诺大学开发的Java字节码注入工具DiSL，能够动 态部署和反部署注入代码，具有很高的灵活性，同时提供自定义代码编织接口， 使得编织时数据能够被收集到，从而用于运行时优化。在本发明的系统中，DiSL 被选为Java程序运行时验证的字节码注入框架。

发明内容

针对现有动态程序验证技术的不足，本发明提出了可动态部署规则的Java 程序运行时验证系统，能够在不影响目标程序运行的前提下动态部署、反部署 和重部署用户定义规则，具有很高的灵活性，同时能够根据运行时验证结果对 代码注入进行动态优化，有效降低了验证系统的性能开销。

本发明的技术解决方案如下：

一种可动态部署规则的Java程序运行时验证系统，该系统运行于DiSL字 节码注入框架之上，包括验证规则翻译器、部署管理器以及运行时引擎三个模 块。

所述验证规则翻译器用于将验证规则定义文件翻译成由事件注入代码和规 则验证代码组合成验证代码；

所述部署管理器用于提供部署验证代码的相关用户接口；

所述运行时引擎用于根据接收的验证代码中事件注入代码产生的事件序列， 为每个监控对象维护一个事件序列，验证事件注入代码产生的事件序列是否与 规则验证代码的事件序列相同，并根据验证情况通过部署管理器对事件注入代 码进行实时部署优化。

优选地，所述验证规则定义文件为AspectJ语言切片语法描述的事件定义 和状态机语言定义的事件序列规则。

优选地，所述部署管理器提供的相关用户接口包括：将验证代码注入到目 标Java程序的动态部署接口、根据运行时引擎的验证从目标Java程序中移除 违反了验证规则和已通过验证的验证代码的动态反部署接口、动态更新目标 Java程序中已部署规则的动态重部署接口

优选地，所述运行时引擎包括规则监控器模块和部署优化器模块：

所述规则监控器模块根据接收的验证代码中事件注入代码产生的事件序列， 为每个监控对象维护一个事件序列，验证产生的事件序列是否与规则验证代码 定义的事件序列相同；

所述部署优化器模块根据规则监控器的验证结果，将已违背规则验证代码 的事件注入代码和路径已完全覆盖的事件注入代码动态移除。

优选地，所述验证规则翻译器将将验证规则定义文件翻译成由事件注入代 码和规则验证代码组合成验证代码的过程为：

a)验证规则翻译器对验证规则进行词法分析，生成token流；

b)验证规则翻译器对token流进行语法分析，生成事件对象集合和规则对 象集合；

c)验证规则翻译器分别将事件对象集合和规则对象集合生成为事件注入代 码和规则验证代码。

附图说明

图1为本发明的系统结构示意图；

图2为本发明中验证规则定义样本；

图3为本发明中验证规则翻译器架构；

图4为本发明中部署管理器的接口类型示意图。

具体实施方式

本实施例在以本发明技术方案为前提的情况下进行实施，下面对具体的实 施方式和操作过程作详细说明。本发明的验证范围包括但不限于这些实施例。

图1所示为可动态部署规则的Java程序运行时验证系统架构。结合图1， 本实施例的具体流程为：

步骤1)用户提供图2所示验证规则定义文件。

其中：a)验证规则名称为HasNext,验证对象类型为Iterator；

b)事件callHasNext和callNext，由AspectJ语言切片定义；

c)状态机状态集合safe，unsafe

d)事件发生时状态转移规则

e)状态机到达unsafe状态时的动作，包括调用验证失败函数和输出错误 信息。

步骤2)验证规则翻译器将验证规则定义文件翻译成验证代码，验证代码包 括事件注入代码和规则验证代码。

图3给出了验证规则翻译器的架构和翻译流程，具体为：

a)验证规则翻译器对验证规则进行词法分析，生成token流；

b)验证规则翻译器对token流进行语法分析，生成事件对象集合和规则对 象集合；

c)验证规则翻译器分别将事件对象集合和规则对象集合生成为事件注入代 码和规则验证代码，其中事件注入代码会被注入到目标Java程序以产生相关事 件，规则验证代码则被规则监控器调用以验证事件序列是否满足规则。

步骤3)用户调用部署管理器，将验证代码部署到目标Java程序。

图4给出了部署管理器提供的相关用户接口，包括动态部署接口：将验证 代码注入到目标Java程序；动态反部署接口：根据运行时引擎的验证从目标Java 程序中移除违反了验证规则和已通过验证的验证代码；动态重部署接口：动态 更新目标Java程序中已部署规则目标Java程序的范围可以为包、类、方法以 及基本块，

具体实现方式为：

a)部署管理器将验证规则名称映射到具体的验证代码的类名称；

b)部署管理器调用DiSL接口将规则类代码注入到指定代码块范围，并维 护注入记录列表；

c)部署管理器在注入记录列表里查询指定范围内的注入记录，调用DiSL接 口移除。

步骤4)部署管理器通过DiSL注入框架注入验证代码到运行时引擎。

运行时引擎包括规则监控器模块和部署优化器模块，规则监控器模块接收 验证代码产生的事件序列，为每个监控对象维护一个事件序列，验证产生的事 件序列是否与规则定义的事件序列相同，部署优化器模块根据规则监控器验证 结果，将已违背规则的验证代码和路径已完全覆盖的验证代码动态移除。

其中，规则监控器具体验证流程为：

1)记录部署优化器提供的事件与规则代码列表；

2)接收事件注入代码产生的相关事件；

3)查询事件相关对象的事件序列，如果序列不存在，为该对象创建新的事 件序列，将新的事件添加到事件序列中；

4)查询事件与规则代码列表，调用规则验证代码验证事件序列是否满足规 则；

5)将验证结果反馈给用户以及部署优化器。

部署优化器具体验证流程为：

1)在注入代码编织过程中被DiSL注入框架调用，从而在此过程中构建用 户程序的控制流图；

2)根据规则监控器的验证结果进行优化：如果验证结果为违反了定义规则， 则将对应基本块的对应事件产生代码移除，避免多次验证；如果验证结果为未 违反，则检查对应基本块所在的所有路径是否都已被验证，如果都已被验证， 则将对应基本块的对应事件产生代码移除。

步骤5)DiSL注入框架在编织验证代码过程中回调部署优化器，部署优化 器在此过程中构建目标程序控制流图；

步骤6)验证代码开始运行，将产生的相关事件传递给规则监控器；

步骤7)规则监控器为每个验证对象保存一个事件序列，同时验证事件序列 是否满足规则，并将验证结果反馈给用户和部署优化器；

步骤8)部署优化器根据实时验证结果决定是否反部署相关注入验证代码， 从而提高验证性能；

步骤9)用户也可以根据验证结果调用部署管理器反部署验证代码；

步骤10)部署管理器通过DiSL注入框架移除验证代码，目标代码继续运 行。

经过对比实验，本发明系统的运行时间开销要比基于AspectJ语言的验证系 统少21％，堆内存消耗要比基于AspectJ语言的验证系统少16％，因此本发明能 够有效降低Java程序运行时验证开销。