Typestate性质运行时验证的关键技术研究

发布时间：2019-09-02 08:09

【摘要】：现代大规模的软件系统一般都是建立在第三方程序库之上的,比如大家所熟知的Java类库。但是,第三方程序库往往对其提供的接口规定了一些调用规约,软件开发人员必须遵循这些调用规约,否则将会导致软件系统在运行时出现不可预知的异常或失效。这些规约被称作typestate性质,通常可以使用带自由变量的时序逻辑表示。据统计,许多大规模软件系统的错误都是由于违反第三方程序库的接口调用规约而引起的,并且此类错误不易被软件开发和维护人员发现和修复,极大地增加了软件开发和维护成本。静态分析程序是否满足给定的typestate性质是一个不可判断的问题。通常,大家使用运行时验证这种动态方式测试程序是否违反typestate性质。运行时验证技术能够将typestate性质自动转换为运行时监控器,并对原程序进行插装处理。但是,插装过后的程序一般包含了大量的冗余插装,这会严重影响程序运行时性能。近年来,大家使用静态分析技术在编译阶段删除一些不必要的监控插装代码,以此来降低动态监控给程序运行时性能所带来的不利影响,这就是所谓的混成typestate性质分析技术。Eric Bodden提出的Nop-shadows Analysis(NSA)就是一种典型的混成Typestate性质分析技术。NSA使用部分上下文敏感、过程内流敏感的数据流分析方法在编译阶段识别和删除一些不必要的监控插装代码。尽管NSA静态分析的精度比较高,但是仍然存在一些案例,NSA不能完全删除其中的监控插装。甚至,对于某些案例,NSA基本上没有效果。本课题认真地研究分析了失效案例,详细地剖析了NSA静态分析过程。在此基础之上,我们提出了三种分别适用于不同情形的优化技术,它们都能针对某些案例提高NSA静态分析精度,在编译阶段识别和删除更多的监控插装代码。具体来说,本文取得了如下贡献和创新:1.定义了稳定configuration的概念,详细地分析了它的特性,并提出了基于稳定configuration的NSA静态分析优化技术。为了识别后向数据流分析结果中产生的稳定configuration,我们通过增加一个布尔变量将原来configuration二元组扩展为三元组,使configuration能够记录状态转换信息,并修改了后向数据流分析过程中的configuration转换算法。本文提出了消除稳定configuration对识别冗余监控插装代码时的不利影响的规则,并对该规则的正确性进行了证明。在程序中存在多个相同类型的对象的操作相互交叉的情况下,我们的优化技术能进一步提高NSA静态分析的精度,识别和删除更多的冗余监控插装代码。2.定义了本地对象和过程间configuraiton的概念,提出了基于本地对象的优化技术,它可以进一步提高NSA静态分析技术识别冗余监控插装代码的能力。本文基于过程内流敏感的指针别名信息,设计了一个识别本地对象的高效算法。我们通过增加一个布尔变量将configuration扩展为三元组结构,使其能够记录数据流分析过程中的过程间控制流传播信息,便于从数据流分析结果中识别过程间configuration。另外,根据configuration在控制流图中的传播机理,本文修改了configuration在过程间的传播转换函数。基于本地对象和过程间configuration,本文提出了消除过程间configuration对识别冗余监控插装代码时的不利影响的规则,并证明了该规则的正确性。3.提出了基于部分过程间流敏感信息的NSA分析优化技术,其核心思想是利用被调用方法中所包含的部分流敏感信息,精化过程间方法调用的数据流分析结果。这样我们可以不用对整个程序的控制流图进行流敏感的数据流分析,有效地避免了完全过程间流敏感分析的代价,还能进一步提高NSA静态分析的精度。本文定义了两个变量绑定和configuration的二元运算符,计算过程间数据流分析的结果。基于过程内流敏感的肯定别名分析算法,本文定制了一个简单高效的过程间肯定别名分析算法。在此基础之上,本文介绍了基于部分过程间流敏感信息的NSA静态分析优化技术的工作流程。4.本课题实现了以上三种优化技术,并将它们集成到Clara框架中,将Clara的静态分析阶段由3个扩展到6个。采用学术界公认的Da Capo基准程序测试集,对比分析和评估我们所提出的优化方法的效果。实验表明,我们所提出的优化方法能够在超过一半的案例中有明显的效果,平均每个案例在原来NSA静态分析之后还能进一步删除11个监控插装代码。特别是在两个案例中,我们得到了非常好的实验结果,完全删除了由原来NSA技术不能识别的冗余监控插装代码,避免了运行时动态监控。此外,三种优化方法并不会额外地引入大量的分析时间。事实上,与程序在编译阶段的总时间相比,优化技术引入的额外开销几乎可以忽略不计。
【学位授予单位】：国防科学技术大学
【学位级别】：博士
【学位授予年份】：2016
【分类号】：TP311.5

【相似文献】