程序不变量检测技术研究进展

刘志明　时小芳　李萌　刘杰

摘要：伴随着经济的迅猛发展，软件更新速度日益加快，传统的软件测试方法已不能有效保障软件质量。对软件测试起到重要影响作用的不变量，受到了广泛的关注。经过近二十年的研究，程序不变量检测技术已经在软件开发、软件测试、逆向工程等领域得到了广泛应用。该文对程序不变量检测技术在国内外的研究现状进行了总结。主要论述了较成熟的程序不变量检测工具的工作原理、基于合约的程序不变量检测等各种方法的检测过程、不变量的应用范围，并分析了以上各种检测工具和方法的优缺点，最后，针对已有程序不变量检测技术及应用中待探究的问题进行了展望。

关键词：程序不变量；动态检测；Daikon

中图分类图：TP311 文献标志码：A 文章编号：1009-3044（2018）02-0216-03

Review of Program Invariant Detection Technology

LIU Zhi-ming， SHI Xiao-fang*， LI Meng， LIU Jie

（School of Computer， University of South China， Hengyang 421001， China）

Abstract： With the rapid development of economic， the update of software is increasingly accelerating， traditional methods of software test cant effectively guarantee the quality of software cant not be guaranteed effectively by traditional methods of software. Program invariant accords with people's expectation which is one of the most important indicators of health management in software runtime. After nearly two decades of research， Program invariant detection technology has been widely used in software development， software test， reverse engineering and other fields. In this paper， the research on invariant at home and abroad is described. Mainly discussed the working principle， the detection process and shortcomings of invariants Based on the Contract as well as the scope of invariants. Besides， it also analyzes merits and shortcomings of the above testing tools and methods. Finally， the possible research goal of the invariant is prospected in connection with the deficiency of existing detection.

Key words： Program Invariant； Dynamical Detection； Daikon

随着经济的发展，软件更新速度日益加快，软件出错率随之增大，如何有效保障和提高软件质量日益重要。在保障软件质量过程中，软件测试作为一种不可或缺的检测技术，对高效发现隐藏在软件中的漏洞起到十分重要的作用。程序不变量作为影响软件测试质量的重要因素之一，是在运行程序的整个过程中，能够反映程序代码中具有不变属性的逻辑语句，不但能够在执行程序时表现代码的各种属性特点，而且能够反映程序数据结构等各方面的信息，在程序的设计、编码、测试等各方面都发挥着不可代替的作用[1]，基于此，致力于研究不变量检测技术非常有必要。

通常，从是否运行被测程序的角度出发，可将不变量检测分为静态分析和动态检测两种方法。静态分析是指在不运行程序代码的情况下，通过检查程序记录文档和代码来发现潜伏在程序中一直不会改变的属性，一般只应用于中小型程序；动态不变量检测是一种可以应用于任意数据的机器学习技术，是指在测试环境中，根据所测代码设计适量的测试用例，然后再运行被测程序获取程序运行轨迹，之后再对获得的轨迹数据进行分析来发现程序中的抽象逻辑属性，弥补了静态分析的不足，适用于较大规模程序[2]。

本文主要介紹了程序不变量动态检测的各种工具、技术和应用背景并分析了其优缺点，最后针对程序不变量检测技术的研究及应用中待探究的问题进行了展望。

1 程序不变量检测工具

自从不变量的定义提出之后，为了能从程序中挖掘出大量精确的不变量，致力于相关工作的研究员已开发出很多不变量检测工具，在此，主要介绍Daikon、Diduce、TDDPA、DySy四种较成熟的不变量动态检测工具。

Daikon先后用Python、java语言开发过，可以动态检测C、C ++、Java等多种程序的属性，且支持记录结构化数据源[3]；Diduce是受Daikon启发开发得来的，侧重于辅助程序员查看程序中存在的漏洞，并定位错误的具体位置，已经被成功应用在JSSE等较大规模的程序排错[2]；TDDPA针对面向对象程序不变量设计并实现的一种交互式的动态检测工具，是基于关系数据库理论提出的；DySy使用了强大的符号执行和简化引擎实现了动态符号执行技术，大幅度地提高了推断不变量的质量。它们的检测过程和特点如表1所示：endprint

表1主要描述了Daikon、Diduce、TDDPA、DySy四种检测工具的检测过程和特点，为以后不变量检测技术的研究提供了依据。

2 程序不变量检测技术

程序不变量检测技术是为了扩充Daikon的预置库形式而提出的。基于合约的程序不变量检测等多种检测技术都遵循图1理论模型。

图1主要描述了动态不变量检测技术的流程，其流程主要是将待检测程序预编译后设置观测点进行编配，然后设计与程序相符的测试用例，在测试用例上运行编配后的程序，运行后会得到观测点对应的输出数据，这些输出数据会以文件的形式保存到数据库中，最后再对文件数据进行分析，得到最终不变量。以下各种检测方法都遵循以上检测流程，但都有各自的创新之处，下面逐一对之说明。

（1） 基于合约的不变量动态检测：存储时将待测数据分成了类层次关系、方法依赖关系和变量内在隐含关系3个层次关系，然后运用数据挖掘算法对其进行分析并根据层次关系将它们进行聚类[5]。巧妙得结合了数据库理论知识和适当的数据挖掘算法有效地解决了轨迹数据如何存储、以及如何推导变量之间的隐含关系的问题。

（2） 基于契约的程序不变量检测：提出了一种新的思想来分析不变量：通过给定待测函数的前置条件与后置条件来保障程序代码质量，简单来说，就是，对任意一个待测函数，提供满足条件的输入，应该得到明确的输出，不管是输入还是输出有错误，能够精确定位出错位置（参数or程序本身）。此方法从一种新的视角维度来保障软件质量，对未来不变量的检测技术研究有很强的借鉴意义。

（3） 非函数依赖程序不变量检测：首先指定要选取的变量类型，然后，选取或构造与之对应的检测条件，然后通过与之对应的语句模板产生精确的查询语句，运行之后便能够查询出符合需要的不变量，最后，将这些目标不变量全部放入不变量集合中[5]。此方法可以按照实际情况灵活地定义新的检测条件并生成与之对应的查询语句，在一定程度上增加了检测不变量的精确性。

（4） 函数依赖程序不变量检测：对轨迹数据进行分析时运用了数据挖掘中的FP-growth关联规则来分析变量之间的关联性， 而且，在确定函数依赖关系阶段利用了回归分析方法对理想化的一元以及多元变量关系进行检测，有效地证实了函数依赖不变量检测的可行性。但是它只分析了简单的几种线性不变量，对复杂的线性不变量还未深入研究。

（5） 接口重载不变量检测：把前置条件和后置条件分成两个单独的阶段来处理，先提取所有可执行方法的前置条件，然后再针对每个接口重载函数，查找与之相符的前置条件，若找到，则提取出与之对应的后置条件，以完成重载方法不变量的提取[6]。有效地解決了面向对象中方法调用时调用者和被调用者产生的不变量不一致的问题。但因为针对同一个测试用例运行了两次程序，效率不高。

2.1 其他方法

近年来，很多工作者致力于不变量检测的相关研究中。相继有相关研究人员运用数学理论与图形化结合的方法有效发现了区间型程序不变量，运用启发式发现规则和检测算法进行一元多项式不等式动态检测、多元多项式不等式动态检测，运用基因表达式编程算法对线性指数型函数进行动态检测，运用GEP-RNC算法对指数与对数型程序不变量进行检测等[7]，克服了原有技术的计算盲目性，进一步扩充了Daikon的预置库形式，使不变量形式更加多样化，增大了挖掘出更多不变量的概率，对不变量检测技术进行了补充。

3 程序不变量的应用

不变量被广泛应用于程序开发中，可以作为断言插入到程序中以确保在进一步测试时随着代码的演变不被窜改；可以过滤无效测试用例、验证和改进测试套件、检测软件缺陷并准确定位软件错误位置；可以检测程序重构对象以保证程序的性能；可以静态分析操作系统内核的属性是否完整；可以检测程序是否发生并发错误；除此之外，不变量还可以形成光谱以指示程序和输入属性的改变[8，9]。应用不变量比较成功的一个实例是美国布朗大学研究人员开发出了一个利用不变量自动查找程序错误的工具Carrot，它的工作原理是先确定不变量库，通过多次运行程序，不断扩展其运行轨迹，最后再对比正确运行轨迹和错误运行轨迹的差异。另外一个不变量应用较为成功的实例是使用Gibraltar工具进行内核数据结构不变量的自动推理和执行[10]，它主要是先通过外部PCI卡周期性地捕获内核内存的快照，然后由Gibraltar进行处理，自动检测内核数据结构，进而查找到修改了关键内核数据结构的rootkit，使系统质量得到保证。不变量不仅仅在以上各方面得到了应用，在谐波雷达等领域也得到了成功的运用，是一个很大的突破。

4 总结与展望

本文系统地讨论了不变量检测技术及其在各个领域的应用，并取得了阶段性成果。在回顾了不变量基本概念基础上，详细分析和总结了不变量检测技术在国内外的研究现状以及不变量的适用背景。从以上分析中可看出：虽然现有的不变量检测技术对不变量的检测有一定的成效，但在检测性能和效率方面仍有进一步提升的空间，而测试用例集的完备性、编配时观测点的选取、轨迹数据的记录格式是影响程序不变量检测性能和效率的重要因素，基于此，如何降低以上因素的影响是研究者需要进一步研究的问题；虽然已有不变量检测方法对Daikon预置库形式进行了大量的扩充，但是，对矩形函数、积分函数等较为复杂的函数并未涉及，未来程序不变量检测方法的研究应该着眼于这些问题的研究和解决上；除此之外，程序不变量在新型软件中的应用亦有待更进一步的研究。

参考文献：

[1] Ernst M D，Notkin D.Dynamically discovering likely program invariants[J].Software Engineering IEEE Transactions on，2001，27（2）：99-123.endprint

[2] University N H，Hengyang H，Liu C，et al.Dynamically Discovering Likely Program Invariants Based on the Contract[J].2006.

[3] http：//plse.cs.washington.edu/daikon/

[4] Csallner C，Tillmann N，Smaragdakis Y.DySy：dynamic symbolic execution for invariant inference[C] //ACM/IEEE International Conference on Software Engineering.2015：281-290.

[5] Bocchi L，Honda K，Tuosto E，et al.A theory of design-by-contract for distributed multiparty interactions[C] //International Conference on Concurrency Theory.Springer-Verlag，2010：162-176.

[6] Baliga A，Ganapathy V，Iftode L.Automatic Inference and Enforcement of Kernel Data Structure Invariants[C] //Computer Security Applications Conference. IEEE Computer Society，2008：77-86.

[7] 李玉燕，陽小华，吴取劲.基于GEP-RNC的指数对数型程序不变量发现方法[J].南华大学学报，2017，31（1）：72-76.

[8] Wei J，Zhu F，Shinjo Y.Static analysis based invariant detection for commodity operating systems[J]. Computers & Security，2014，43（6）：49-63.

[9] Roest D，Deursen A V，Mesbah A.Invariant-Based Automatic Testing of Modern Web Applications[J].IEEE Transactions on Software Engineering，2012，38（1）：35-53.

[10] 单锦辉，姜瑛，刘江红，等.基于合约的构件易测试性设计支撑工具的设计与实现[J] .北京大学学报：自然科学版，2005，（5）：815-819.endprint