基于两区间抽象域的抽象解释方法研究与实现

摘要

随着信息技术的飞速发展，软件已经成为决定系统安全性的重要因素。数值计算是大部分安全关键软件必不可少的部分，因而程序变量的数值分析对于软件安全性的保证至关重要。
　　抽象解释提供了一种对程序语义进行上近似的通用静态分析框架，是最适合进行程序变量数值分析的方法之一。抽象域作为抽象解释框架下的核心要素，通过特定的语义表示和域操作来发现所关注的性质。数值抽象域是用来发现程序变量数值性质的抽象域。经过几十年的发展，在基于抽象解释的程序变量数值分析领域，已经出现了许多各具特色的抽象域。然而，大部分已有抽象域无法表达程序的非凸语义，从而可能会导致分析的误报率增加。
　　本文首先给出面向程序变量数值性质的抽象解释分析框架。然后，在此分析框架下，引入“两区间”的概念对经典的非关系型抽象域和弱关系型抽象域进行非凸性扩展，形成了两个新的可以表达程序某类非凸语义的扩展抽象域，统称为两区间抽象域。最后，通过两区间抽象域对程序变量数值性质进行了分析。论文的具体内容包括：
　　(1)设计并实现了两区间非关系型抽象域。该抽象域在区间抽象域的基础上进行了两区间扩展，从而使其表达能力强于经典的区间抽象域。
　　(2)设计并实现了两区间弱关系型抽象域。在两区间非关系型抽象域的基础上，进一步对弱关系型抽象域进行了两区间扩展，从而形成了可以表达某类程序非凸语义的两区间弱关系型抽象域。
　　(3)基于抽象解释分析框架，实现了支持两区间抽象域的程序变量数值分析原型工具。
　　最后，利用原型分析工具，本文分别基于文中提出的两区间抽象域和已有经典抽象域进行了对比分析实验。实验结果表明，两区间的扩展可以有效地提高程序变量数值分析的精度。

目录

声明

缩略词

第一章 绪论

1.1课题研究背景

1.2选题依据及研究内容

1.3论文组织结构

第二章 面向程序变量数值性质的抽象解释

2.1抽象解释理论

2.2程序变量数值性质分析

2.3面向程序变量数值性质的抽象解释分析框架

2.4本章小结

第三章 两区间非关系型抽象域

3.1两区间非关系型抽象域的域表示

3.2两区间抽象域的域操作

3.3实例分析

3.4本章小结

第四章 两区间弱关系型抽象域

4.1两区间弱关系型抽象域的域表示

4.2两区间八边形约束的空性测试与标准化

4.3两区间弱关系型抽象域的域操作以及迁移函数

4.4本章小结

第五章 原型工具的实现及实验分析

5.1支持两区间抽象域的原型分析工具实现

5.2实验结果与分析

5.3本章小结

第六章 总结与展望

6.1工作总结

6.2研究展望

参考文献

致谢

在学期间的研究成果及发表的学术论文