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

来源 :国防科学技术大学 | 被引量 : 0次 | 上传用户:XUE19880204
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
现代大规模的软件系统一般都是建立在第三方程序库之上的,比如大家所熟知的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技术不能识别的冗余监控插装代码,避免了运行时动态监控。此外,三种优化方法并不会额外地引入大量的分析时间。事实上,与程序在编译阶段的总时间相比,优化技术引入的额外开销几乎可以忽略不计。
其他文献
印刷业历史悠久,是中国的四大发明之一。在今天这样一个瞬息万变的世界,印刷业也发生了重大的变化,紧跟当今时代步伐,由原来的传统印刷向数字印刷转变,适应了当今社会的发展
随着三维游戏、影视娱乐和虚拟现实等技术的发展和普及,人们对三维模型形状的多样性以及逼真程度的要求与日俱增。树木是自然场景不可或缺的景物对象,逼真的树木模型能极大提
以革兰氏阴性菌大肠杆菌((Escherichia coli)作为试验菌,通过测定艾草(Artemisia argyi Lévl.et Van.)水提物与大肠杆菌作用前后细菌培养液的电导率、总糖和总蛋白的变
社区自发性群众体育组织是我国群众体育健身活动的主要载体。运用协同学理论从自组织的形成条件、系统内部要素和序参量等方面阐述了社区自发性群众体育组织的形成、发展和动
俗话说:火车跑得快,全靠车头带。作为带动农村经济发展的火车头,村党组织书记队伍建设发展至关重要。一个守信念、讲奉献、有本领、重品行的村党组织书记直接关系着党的政策
中学数学教师专业化发展已是世界数学教师教育的发展趋势,师德是中学数学教师专业素养的核心,是中学数学教师专业化的重要标志。师德建设贯穿于中学数学教师专业化发展的全过