安全C语言验证器的形状系统的扩展设计与实现

发布时间：2020-06-30 01:45

【摘要】：随着计算机技术的不断发展,软件已经融入到人们的日常生活和工作生产中,而随着软件规模和复杂度的不断攀升,软件的质量依旧不尽如人意,由此造成的问题对于安全攸关的领域威胁极大。提高软件的可信度是大势所趋,其中基于演绎推理的形式化验证方法就是主要研究方向之一。本课题组设计并开发了安全C语言验证器,它是一款基于演绎推理的C语言程序验证工具,采用了霍尔逻辑和形状图逻辑。形状系统是安全C语言验证器对于形状图逻辑的实现,用于完成堆指针相关程序语句的演算,并限制程序能够使用的易变数据结构及其相关操作。本工作针对形状系统中存在的不足,实施了一系列改进和扩展。第一,扩展了形状系统的演算操作。通过为节点定位演算扩展角标表达式相关的操作规则,把该演算扩展到适用于带角标的指针访问路径的场合,解决原本指针访问路径抽象表述能力不足的问题。此外,本工作还通过函数调用窗口的概念,细化和实现了形状图逻辑中最复杂的函数调用规则,使得形状系统能支持带函数调用语句的验证。第二,改进了形状图的构造方法。形状图构造方法用于从描述堆指针性质的符号断言构造等价的形状图,以便形状系统能够根据构造得到的形状图对堆指针操作语句进行演算。本工作为该方法引入了内置形状谓词,用以简化和复用部分断言描述,并对不同类型的断言施加明确的操作语义,使得形状系统可以正确还原断言描述的形状图,并发现断言中的错误。此外,本工作还引入了自定义谓词到内置形状谓词的推断方法,以尽可能规避内置形状谓词引入后造成的冗余表述的问题。第三,引入了形状检查方法。形状检查方法用以检查程序使用的易变数据结构是否符合安全C语言的相关限定。为表示检查操作的不同严格程度,本工作为形状检查方法引入不同的形状级别,并通过形状分割、形状分析和形状推断这三个阶段分解由易变数据结构中不同指针域带来的复杂性。另外,本工作还通过实现显式形状检查和隐式形状检查,简化形状检查方法的使用。通过本文工作,扩展后的形状系统可以处理表述能力更强、更为复杂的描述形状图的断言,能够支持含有函数调用的程序的演算,并且能够灵活便捷地完成对于易变数据结构是否符合形状定义的检查,最终使得形状系统的功能和性能得到改善。
【学位授予单位】：中国科学技术大学
【学位级别】：硕士
【学位授予年份】：2018
【分类号】：TP311.52
【图文】：

形状,节点,指代

形状图是对于程序执行过程中易变数据结构状态的图形化描述，它通过有逡逑向图的形式描述程序中声明的堆指针变量和堆内存中数据结构节点指针域的指逡逑向情况，但并不关心节点的数据域。如图２．３所示，在形状图的表述中，存在６种逡逑不同类型的形状图节点［３７］：声明节点用于指代程序中声明的堆指针变量，显示逡逑为圆形节点；ＮＵＬＬ节点用于描述Ｃ语言中的ＮＵＬＬ字面量，显示为含Ｎ的虚逡逑线矩形，若存在指针指向ＮＵＬＬ节点，即该指针的值为ＮＵＬＬ；悬空节点用于描逡逑述悬空的内存块，显示为含Ｄ的虚线矩形，若存在指针指向悬空节点，即该指逡逑针悬空；结构节点用于指代动态分配的结构体内存块，显示为实线矩形；浓缩节逡逑点用于描述指定数量的结构节点的折叠，显示为灰底实线矩形，其中ｅ为描述数逡逑量的表达式，ａ为关于ｅ的约束断言，引入浓缩节点主要用以简化形状图的表述逡逑（如减少节点的数量）并提升其抽象表述能力；谓词节点用于指代具备特定谓词逡逑性质的内存块

类继承,形状,体系

限制程序能够使用的易变数据结构种类及相关操作的目的，当前的形状系统能逡逑够支持５种形状类别：单向链表、循环单向链表、双向链表、循环双向链表和二逡逑叉树。形状系统演算操作的主要对象即形状图，实现中通过如图２．５所示的类继逡逑承体系完成对于不同节点的表述，其中ＢａｓｅＮｏｄｅ是所有节点的抽象基类，包含逡逑适用于所有节点类型的操作接口，ＣｏｎｄｅｎｓｅＮｏｄｅ则是继承自ＳｔｒｕｃｔＮｏｄｅ，其在后逡逑者的基础上，还包含与长度信息相关的成员变量。逡逑ＢａｓｅＮｏｄｅ逡逑逦逦逦邋ｉ逦１逡逑Ｔ逦丨ＤｅｃＫＮｏｄｅ：声明节点逡逑逦Ｉ逦１逦１逦｜邋ＳｔｍｃｔＮｏｄｅ：结构节点邋；逡逑ＤｅｃｉＮｏｄｅ逦ＳｔｍｃｔＮｏｄｅ逦ＤａｎｇｌｉｕｇＮｏｄｅ邋｜邋Ｃ°ｎｄｅｉｉｓｅＮｏｄｅ：浓缩＂ｐ邋点邋｜逡逑逦邋逦邋逦！邋ＰｒｅｄｉｃａｔｅＮｏｄｅ：谓词节点逦｜逡逑Ｓ逦＊ＮｕｌｌＮｏｄｅ：邋ＮＵＬＬ节点逡逑逦Ｊ逦逦逦１逦．Ｉ逦逦邋；ＤａｉｉｇｌｉｎｇＮｏｄｅ：悬空节点邋｜逡逑ＰｒｅｄｉｃａｔｅＮｏｄｅ邋ＣｏｎｄｅｎｓｅＮｏｄｅ邋ＮｕｌｌＮｏｄｅ逦！逡逑图２．５形状图节点的类继承体系逡逑原型形状系统初步实现了形状图逻辑中所述的除函数调用之外的演算规则，逡逑但在实现层面上对于系统的子模块并未作出明确的划分。本研宄在实现过程中逡逑对形状系统的实现做了重构

【参考文献】