(12)发明专利申请
(10)申请公布号 CN 109426614 A(43)申请公布日 2019.03.05
(21)申请号 201811013103.6(22)申请日 2018.08.31
(66)本国优先权数据
201710781158.0 2017.09.01 CN
(71)申请人 深圳市源伞新科技有限公司
地址 518055 广东省深圳市南山区西丽街
道西丽中山园路1001号TCL国际E城C7-C栋201(72)发明人 肖枭 时清凯 周金果 范刚
张川 (74)专利代理机构 北京律智知识产权代理有限
公司 11438
代理人 袁礼君 阚梓瑄(51)Int.Cl.
G06F 11/36(2006.01)
(54)发明名称
缺陷检测方法、设备、系统和计算机可读存储介质(57)摘要
本发明公开了一种缺陷检测方法、装置、设备和计算机可读存储介质,该方法包括:输入待检测的程序,并对待检测的程序进行预处理;生成待检测的程序的符号表示图,其中,符号表示图中的节点表示程序中的变量,符号表示图中的边表示数据依赖性和控制依赖性,符号表示图中还包括运算符;沿着数据依赖性边,向后遍历该符号表示图,以检测缺陷。本发明的方法、装置、设备通过遍历本发明提出的符号表示图,能够高效地检测空指针解引用或缓冲区溢出缺陷。
G06F 8/41(2018.01)
权利要求书2页 说明书14页 附图10页
CN 109426614 ACN 109426614 A
权 利 要 求 书
1/2页
1.一种缺陷检测方法,包括:对待检测的程序进行预处理;
生成待检测程序的符号表达式图,所述符号表达式图包括值节点、运算符节点,以及连接节点的数据依赖性边和控制依赖性边,其中,所述值节点包括终端值节点和非终端值节点,所述终端值节点表示当前函数外生成的未知的值或常量,所述非终端值节点表示所述当前函数内生成的非终端值,并且每个所述非终端值与一个唯一的内存地址相关联,所述数据依赖性边是将所述节点连接到与其有直接数据依赖关系的值节点的有方向性的边,所述控制依赖性边是当存在限定变量的条件时将变量连接到条件的有方向性的边;以及
对所述符号表达式图向后进行深度优先遍历,在发现缺陷时生成错误报告。2.如权利要求1所述的方法,其中所述缺陷是空指针解引用,从空指针结点开始对所述符号表达式图向后进行深度优先遍历,在发现缺陷时生成错误报告。
3.如权利要求2所述的方法,其中当检测到空指针时,为所述空指针对应的空指针结点生成约束;到达空指针解引用地址,添加约束,并检查是否满足约束,如果是,则生成错误报告。4.如权利要求3所述的方法,还包括从空指针解引用地址返回到追溯点,并弹出解引用地址的约束,继续搜索空指针解引用地址,直到所述符号表达式图遍历完成。
5.如权利要求1所述的方法,其中所述缺陷是缓冲区溢出。6.如权利要求5所述的方法,其中
对缓冲区使用回溯算法计算偏移量,所述偏移量为先序指针偏移量之和;检查缓冲区分配大小和所述偏移量是否满足约束,如果是,则生成错误报告。7.如权利要求6所述的方法,其中对每个缓冲区计算偏移量,并检查每个缓冲区的大小和对应的偏移量的布尔可满足性,如果相应的真值成立,则生成错误报告。
8.如权利要求7所述的方法,其中深度优先搜索每个缓冲区,并缓存相应约束。9.如权利要求1所述的方法,其中所述控制依赖性边指向的一侧为逻辑运算的运算符或布尔值节点。
10.如权利要求1所述的方法,其中用真和假来标记所述控制依赖性边,以表明逻辑运算的所需的结果。
11.如权利要求1所述的方法,其中所述待检测程序是程序片段,并且所述符号表达式图是从底层向上构建的。
12.如权利要求1所述的方法,其中所述预处理包括展开程序中的循环。13.一种缺陷检测设备,包括存储器和处理器,其中所述处理器配置成执行如权利要求1-12所述的方法。
14.一种计算机可读存储介质,所述介质存储有计算机程序,所述计算机程序被执行时,执行如权利要求1-12所述的方法。
15.一种缺陷检测系统,包括:预处理模块,对待检测的程序进行预处理;符号表达式图生成模块,生成待检测程序的符号表达式图,所述符号表达式图包括值节点、运算符节点,以及连接节点的数据依赖性边和控制依赖性边,其中,所述值节点包括
2
CN 109426614 A
权 利 要 求 书
2/2页
终端值节点和非终端值节点,所述终端值节点表示当前函数外生成的未知的值或常量,所述非终端值节点表示当前函数内生成的非终端值,并且每个非终端值与一个唯一的内存地址相关联,所述数据依赖性边是将节点连接到与其有直接数据依赖关系的值节点的有方向性的边,所述控制依赖性边是当存在限定变量的条件时将变量连接到条件的有方向性的边;以及
检测模块,对所述符号表达式图向后进行深度优先遍历,在发现缺陷时生成错误报告。16.如权利要求15所述的系统,其中所述缺陷是空指针解引用,从空指针结点开始对所述符号表达式图向后进行深度优先遍历,在发现缺陷时生成错误报告。
17.如权利要求16所述的系统,其中所述检测模块还配置成:在检测到空指针时,为所述空指针对应的空指针节点生成约束;到达空指针解引用地址,添加约束,并检查是否满足约束,如果是,则生成错误报告。18.如权利要求17所述的系统,其中所述检测模块还配置成:从空指针解引用地址返回到追溯点,并弹出解引用地址的约束,继续搜索空指针解引用地址,直到所述符号表达式图遍历完成。
19.如权利要求15所述的系统,其中所述缺陷是缓冲区溢出。20.如权利要求19所述的系统,其中所述检测模块还配置成:对缓冲区使用回溯算法计算偏移量,其中所述偏移量为先序指针偏移量之和;检查缓冲区分配大小和所述偏移量是否满足约束,如果是,则生成错误报告。21.如权利要求20所述的系统,其中所述检测模块还配置成:对每个缓冲区计算偏移量,并检查每个缓冲区的大小和对应的偏移量的布尔可满足性,如果相应的真值成立,则生成错误报告。
22.如权利要求21所述的系统,其中所述检测模块还配置成:深度优先搜索每个缓冲区,并缓存相应约束。23.如权利要求15所述的系统,其中所述控制依赖性边指向的一侧为逻辑运算的运算符。
24.如权利要求23所述的系统,其中用真和假来标记所述控制依赖性边,以表明逻辑运算的所需的结果。
25.如权利要求15所述的系统,其中所述待检测程序是程序片段,并且所述符号表达式图是从底层向上构建的。
26.如权利要求15所述的系统,其中所述预处理模块还配置成展开程序中的循环。
3
CN 109426614 A
说 明 书
缺陷检测方法、设备、系统和计算机可读存储介质
1/14页
技术领域
[0001]本发明涉及计算机应用技术领域,具体而言,涉及一种缺陷检测方法、设备、系统和计算机可读存储介质。
背景技术
[0002]空指针解引用(NPD)是导致软件故障的常见问题,而且空指针解引用并不容易检测。静态检测NPD错误需要非常准确的数据流分析以跟踪信息流,特别是流入堆(heap)和从堆流出的那些信息流。另一方面,缓冲区溢出(Buffer Overflow)也是一种常见的软件安全缺陷,通常指的是程序向缓冲区中写入超过允许的数据量,即导致了溢出。该行为不仅有可能导致软件运行异常,甚至有可能造成隐私泄露、被获取程序乃至系统控制权之风险。[0003]程序分析是编译器执行程序转换的先决条件。简单来讲,编译器就是将一种语言(通常为高级语言)翻译为另一种语言(通常为低级语言) 的程序,高级计算机语言便于人编写,阅读交流,维护,机器语言是计算机能直接解读、运行的。经典的用于程序编译的程序表示叫做控制流图(CFG),基于CFG的分析和转换有两方面的缺陷:首先,它们必须保持CFG不变,以在每个代码动作或其他转换之后产生语义上相当的 CFG;其次它们对赋予值的名称非常敏感。
[0004]为了解决以上问题,值依赖图(VDG)被用于空指针解引用检测和缓冲区溢出检测。VDG是一种稀疏的数据流式表示,它是一种功能性的表示,将控制流表示为数据流,并明确表达所有机器数量,如,存储和 I/O通道的数量。Weise,Daniel等人于1994年提出了一种编译器,通过构建VDG来对程序进行表示、分析和转换VDG,然后从优化的VDG产生控制流图(CFG),这种方法相比于先前的方法简化了程序转换。发明内容
[0005]为了解决现有技术中存在的问题,本发明提出一种全新的符号表示图(SEG),在该图中,节点表示程序中的变量,边表示数据依赖和控制依赖。本发明提供了一种通过遍历符号表示图来高效地分析程序,并提高了检测缺陷的效率。[0006]根据本发明的一方面,提供了一种缺陷检测方法,包括:对待检测的程序进行预处理;生成待检测程序的符号表达式图,符号表达式图包括值节点、运算符节点,以及连接节点的数据依赖性边和控制依赖性边,其中,值节点包括终端值节点和非终端值节点,终端值节点表示当前函数外生成的未知的值或常量,非终端值节点表示当前函数内生成的值,并且每个非终端值与一个唯一的内存地址相关联,所述数据依赖性边是将节点连接到与其有直接数据依赖关系的值节点的有方向性的边,所述控制依赖性边是当存在限定变量的条件时将变量连接到条件的有方向性的边;以及对所述符号表达式图向后进行深度优先遍历,在发现缺陷时生成错误报告。[0007]其中,当该方法被用于检测空指针解引用时,从空指针结点开始对所述符号表达式图向后进行深度优先遍历,在发现空指针解引用时生成错误报告。在该方法中,当检测到
4
CN 109426614 A
说 明 书
2/14页
空指针时,为该空指针对应的空指针结点生成约束;到达空指针解引用地址,添加约束,并检查是否满足约束,如果是,则生成错误报告。然后,从空指针解引用地址返回到追溯点,并弹出解引用地址的约束,继续搜索空指针解引用地址,直到该符号表达式图遍历完成。[0008]而当该方法被用于检测缓冲区溢出时,对缓冲区使用回溯算法计算偏移量,所述偏移量为先序指针偏移量之和;检查缓冲区分配大小和所述偏移量是否满足约束,如果是,则生成错误报告。其中对每个缓冲区计算偏移量,并检查每个缓冲区的大小和对应的偏移量的布尔可满足性,如果相应的真值成立,则生成错误报告。[0009]其中,所述控制依赖性边指向的一侧为逻辑运算的运算符或布尔值节点。[0010]其中,用真和假来标记所述控制依赖性边,以表明逻辑运算的所需的结果。[0011]其中所述待检测程序是程序片段,并且所述符号表达式图是从底层向上构建的。[0012]其中所述预处理包括展开程序中的循环。[0013]根据本发明的第二方面,提供了一种生成符号表达式图的方法,包括以下步骤:根据输入的代码语句,构造节点,节点代表变量或常量或运算符;用有方向性的边将节点连接起来,以生成代表数据依赖性的边;当存在限定变量的条件时,用有方向性的边将变量连接到条件,以生成代表控制依赖性的边;以及根据输入的下一个代码语句,重复执行以上步骤,直到程序片段完成为止。[0014]其中,所述控制依赖性边指向的一侧为逻辑运算的运算符。[0015]其中,用真和假来标记所述控制依赖性的边,以表明逻辑运算的所需的结果。[0016]根据本发明的第三方面,提供了一种缺陷检测设备,包括存储器和处理器,其中,处理器配置成执行如上所述的生成符号表达式图和缺陷检测方法。[0017]根据本发明的第四方面,提供了一种计算机可读存储介质,该介质存储有计算机程序,该计算机程序被执行时,执行如上所述的生成符号表达式图和缺陷检测方法。[0018]根据本发明的第五方面,提供了一种缺陷检测系统,包括:预处理模块,对待检测的程序进行预处理;符号表达式图生成模块,生成待检测程序的符号表达式图,符号表达式图包括值节点、运算符节点,以及连接节点的数据依赖性边和控制依赖性边,其中,值节点包括终端值节点和非终端值节点,终端值节点表示当前函数外生成的未知的值或常量,非终端值节点表示当前函数内生成的值,并且每个非终端值与一个唯一的内存地址相关联,所述数据依赖性边是将节点连接到与其有直接数据依赖关系的值节点的有方向性的边,所述控制依赖性边是当存在限定变量的条件时将变量连接到条件的有方向性的边;以及检测模块,对所述符号表达式图向后进行深度优先遍历,在发现缺陷时生成错误报告。[0019]其中,在一些实施例中,所述检测模块还配置成用于检测空指针解引用,在检测到空指针时,为该空指针对应的空指针节点生成约束;到达空指针解引用地址,添加约束,并检查是否满足约束,如果是,则生成错误报告,然后从空指针解引用地址返回到追溯点,并弹出解引用地址的约束,继续搜索空指针解引用地址,直到该符号表达式图遍历完成。[0020]在一些实施例中所述检测模块还被配置成用于检测缓冲区溢出,对缓冲区使用回溯算法计算偏移量,所述偏移量为先序指针偏移量之和;检查缓冲区分配大小和所述偏移量是否满足约束,如果是,则生成错误报告;其中,对每个缓冲区计算偏移量,并检查每个缓冲区的大小和对应的偏移量的布尔可满足性,如果相应的真值成立,则生成错误报告。[0021]其中,所述控制依赖性边指向的一侧为逻辑运算的运算符。
5
CN 109426614 A[0022]
说 明 书
3/14页
其中,用真和假来标记所述控制依赖性边,以表明逻辑运算的所需的结果。
[0023]其中所述待检测程序是程序片段,并且所述符号表达式图是从底层向上构建的。[0024]其中所述预处理模块还配置成展开程序中的循环。[0025]应当理解的是,以上的一般性描述和后文的详细描述仅是示例性的,并不能限制本发明。
附图说明
[0026]下面将参照附图详细描述本发明的示例实施例,本发明的上述和其它目标、特征和优点将变得更加显而易见。
[0027]图1是根据本发明的一个实施例的稀疏程序的流程图。
[0028]图2A-2B示出了根据本发明的一个实施例的预建模阶段中展开循环的一个例子。[0029]图3示出了一段示例代码及其未修剪的HSSA形式。
[0030]图4示出了根据本发明的一个实施例生成的示例性的SEG。[0031]图5A-5B示出了为上述代码片段生成SEG图的示意图。[0032]图6A-6E示出了遍历SEG图,以对示例程序进行空指针解引用缺陷检测的示意图;[0033]图7示出了根据本发明的一个实施例的自动机示意图;[0034]图8A示出了为一段代码片段生成SEG图的示意图;
[0035]图8B至图8G示出了遍历SEG图以进行缓冲区溢出缺陷检测的示意图。
具体实施方式
[0036]现将参考附图更全面地描述本发明的示例性实施例。应理解,本文中的示例性实施例仅是提供用来帮助理解本发明,而不应以任何形式限制本发明。提供这些实施例是为了使本发明的描述更加全面和完整,并将示例性实施例的构思全面地传达给本领域的技术人员。附图仅为本发明的示意性图解,并非一定是按比例绘制。图中相同的附图标记表示相同或类似的部分,因而将省略对它们的重复描述。[0037]此外,本文描述的特征、结构或优点可以以任何合适的方式结合在一个或更多实施例中。在下面的描述中,提供许多具体细节从而给出对本发明的实施方式的充分理解。然而,本领域技术人员将意识到,可以实践本发明的技术方案而省略特定细节中的一个或多个,或者可以采用其它等效的方法、方式、装置、步骤等来代替。为了简明起见,对于本领域中公知的结构、方法、装置、实现或者操作,将不再赘述。
[0038]图1示出了根据本发明的实施例的缺陷检测方法的流程图。该方法包括:S101,对待检测的程序进行预处理;S102,生成待检测程序的符号表达式图,符号表达式图包括值节点、运算符节点,以及连接节点的数据依赖性边和控制依赖性边,其中,值节点包括终端值节点和非终端值节点,终端值节点表示当前函数外生成的未知的值或常量,非终端值节点表示当前函数内生成的值,并且每个非终端值与一个唯一的内存地址相关联,所述数据依赖性边是将节点连接到与其有直接数据依赖关系的值节点的有方向性的边,所述控制依赖性边是当存在限定变量的条件时将变量连接到条件的有方向性的边;以及,S103,对所述符号表达式图(SEG)向后进行深度优先遍历,在发现缺陷时生成错误报告。[0039]当以上所述的缺陷为空指针解引用时,在S103,从空指针结点开始对所述符号表
6
CN 109426614 A
说 明 书
4/14页
达式图(SEG)向后进行深度优先遍历,在发现空指针解引用时生成错误报告。在S104,当检测到空指针时,为该空指针对应的空指针结点生成约束;到达空指针解引用地址,添加约束,并在步骤S105 检查是否满足约束。如果在S105为否,则返回S103继续遍历SEG。如果在S105为是,则在S106生成错误报告,然后从空指针解引用地址返回到追溯点,并弹出解引用地址的约束。之后,返回S103,继续搜索空指针解引用地址,直到该符号表达式图遍历完成。[0040]其中,控制依赖性边指向的一侧为逻辑运算的运算符或布尔值节点。[0041]其中,用真和假来标记控制依赖性边,以表明逻辑运算的所需的结果。[0042]其中待检测程序是程序片段,并且符号表达式图是从底层向上构建的。[0043]其中预处理包括展开程序中的循环。[0044]下面,结合附图简要介绍本发明提出的精确空指针解引用(NPD) 算法的总体框架。该算法主要包括四个阶段:预建模(Pre-model)、先决分析(Prerequisite Analysis)、后建模(Post-model)和缺陷分析(Defect analysis)。[0045]在预建模阶段,主要从输入的程序中消除不感兴趣的结构,以简化后续分析。例如,循环展开、循环打破等都是在这个阶段执行的。[0046]接下来,在先决分析阶段,计算基本信息,特别是该阶段的后续分析中所需的整个程序信息。根据先决分析结果,生成调用图。调用图是本领域中常用的用来描述程序结构的图,这里不再详述。[0047]接着,在后建模阶段,使用先决分析阶段生成的调用图来进一步简化代码,并更新程序信息。例如,标记调用图中形成SCC(强连通分量) 的调用边,以便将来在不必进入循环的情况下,就能够对调用图中的迭代进行分析。[0048]最后,在缺陷分析阶段,主要算法是符号值流分析(SVFA),生成函数摘要信息,以完成函数内分析。此时,这些指针的值仍然是未知的。对符号指针表示图(SPEG)IR(中间语言)执行SVFA,其中SPEG IR 对点对关系(左值依赖)和变量的符号值(右值依赖)一起进行建模,可得到符号表示图(SEG)。该SEG是本发明中提出的一种全新的数据结构,下面将更加详细地描述SEG的生成过程和利用SEG进行缺陷检测的方法。
[0049]本发明中提出的SEG能够紧凑地将每个变量的值表示为外部存储器位置的变量的逻辑和算数表达式,例如,参数、全局变量和通过参数和全局变量可达的堆位置。SEG是一种有向无环图(简称DAG),是对所有变量的一种完整SSA表示。通过前向路径敏感的分析,从下向上构建 SEG,因此可以递增地评估SAT查询。还因为SEG的DAG性质,我们可以将特定的SEG子图替换为常数表示以加速约束解析。
[0050]使用SEG的流水线工作流程是非常灵活的,我们可以简单地添加更多阶段来实现特定功能。例如,将来我们可以将分析过程分阶段化,逐渐使用更准确的分析来细化错误报告。每个分析阶段仅验证来自上一个阶段的错误候选者。我们可以通过在预建模阶段和缺陷分析阶段之间添加一组阶段来实现这种功能。[0051]下面将介绍每个阶段中实现的主要算法,并重点介绍符号值流分析 (SVFA)。应理解,本文中提供的实例和细节仅是为了帮助理解,而不以任何方式对本发明的范围构成限制。
[0052]预建模阶段
[0053]在预建模阶段,例如,可使用开源的LLVM转换来对程序进行建模。表1示出了这里
7
CN 109426614 A
说 明 书
5/14页
使用的LLVM转换流程的完整列表。[0054]表1:
[0055]
该阶段的主要任务是展开和打破所有的循环,根据循环嵌套结构,从内环到外环。
近似循环对于有界模型检查至关重要,展开循环是最简单也是最粗暴的方式。在图2A和2B中示出了展开循环的一个例子。
[0057]图2A示出了展开循环之前的循环,该循环为规范的形式:该循环具有预读头部(Pre-header),并且只有一个调用锁存的节点能够返回到头部(header)。虚线箭头将循环内部存在的节点连接到循环外部的退出节点(exit node),并且所有退出节点都被布置了
[0056]
足够的函数,以保护来自循环的定义。当然,虚线箭头表示该条边并不存在。通过首先复制循环体(loop body)K次,然后为克隆的变量更新定义-使用(def-use)关系,来执行展开循环K次。
[0058]图2B示出了将图2A中的循环展开两次的结果,即,复制了两次。我们对代码执行三种类型的更新。首先,将来自第i个循环的锁存(latch) 复制到第i+1个循环的头部,为所有头部复制和更新
函数。其次,将新的值插入被克隆的变量的退出节点的
函数中。接下
来,从头部的锁存去除后边缘。这时,如果锁存不能退出循环,则变为悬挂节点,我们为锁存附加一个不可达的指令,并依赖死代码消除来清理无用的变量。[0059]先决分析阶段
[0060]该阶段主要设置来收集全局程序信息。要收集的非常基本的信息是调用图。我们使用传统指针分析方法来计算调用图,这里不再描述其细节。然而,我们仅使用自下向上的方法,这对于生成调用图是至关重要的,因为自上向下的方法速度过慢。[0061]后建模阶段
[0062]我们在先决分析之后插入另一个编码建模阶段,提供进一步简化的代码在缺陷分析阶段使用。在该阶段执行的所有算法都是响应于全局程序信息的更新,如果该信息有改变的话。在后建模阶段,不仅可以实现调用图SCC标记分析,如上文所述,标记在调用图中形成循环的后沿,还可以通过缺陷分析来利用这些信息来计算循环中函数的有界分析结果。可选地,还可以在该阶段增加其他重要的变换,如,常数传播(constant propagation)等。[0063]缺陷分析阶段
8
CN 109426614 A[0064]
说 明 书
6/14页
在该实施例中,缺陷分析的算法设计如下:
*[0065] [0066] [0075]该示例性算法的源代码的语法定义如上所示,其中ite是if-then-else 的缩写。该算法的第一条规则定义了该算法建模的类型,支持两种元素类型:布尔型和整型。在基本类型的基础上定义了C结构(C struct)、数组(array)和指针(pointer)等复合类型。应注意,当前算法中没有对浮点算术进行建模,尽管约束求解器Z3已经添加了对浮点数的支持。所有浮动变量都可以转换为整数变量,并将其整数值建模为未知数。[0076]其余规则定义了变量和变量组成的表达式。具体来说,该算法支持多步指针表达式v→f1.f2...fh,为未初始化变量和浮动变量建模的 unknown值,函数参数的parm值,以及全局变量的global值。由于LLVM 通过插入临时变量将长表达式转化为短表达式,因此,在此基础上,还可以将存储和加载语句写为*(p+f)=v和v=*(p+f),其中f是基本指针p的偏移量。 [0077]下面,将结合实例介绍根据本发明的基于可能的混叠分析的NPD方法。[0078]程序内分析通过执行价值流分析(value flow analysis),在函数内找到条件为null的空指针。[0079]价值流分析 [0080]下面给出示例性的价值流分析(VFA)的抽象域定义: [0081][0082][0083][0084][0085][0086][0087][0088][0089] Local+parameter variablesGlobal variables Abstract objects(new’ed memorry)Path conditionsAbstract valuesδ:ψ: VFA的任务是计算一个抽象存储位置可能具有的抽象值集合,即,如上所示的δ函 数。抽象值是分析涉及的具体值的抽象表示。VFA还计算抽象位置具有给定的抽象值时的条件。计算结果被表示为函数。为了简单起见,我们还将条件位置值对写为 其中 9 CN 109426614 A 说 明 书 7/14页 并且 作为例子,我们可以选择SSA作为制定VFA的开始,因为SSA能够支持稀疏分析,从 而可以显着提高分析性能。然而,由LLVM构建的 SSA只是转换了顶级变量,即,那些没有被指针指向的变量。堆内存位置也被LLVM忽略,因此堆内存位置之间的值流是不清楚的。因此,尝试解析指针表达式来构造一个完全编码所有内存位置的def-use关系的 SSA形式。[0091]这里的核心问题是分解负载和存储语句。假设指针p指向在可能的混叠分析阶段获得的对象o1,o2,…,ok,则一个直接的因式分解方法是:[0092]对于*(p+f)=v,可以用对象字段的一组直接赋值来替换它:o1.f= v,o2.f=v,...,ok.f=v。 [0093][0090] 对于v=*(p+f),可以用赋值替换它。函数 表示其参数之一可以赋值给v。 [0094]对象字段的因式分配由其原始指针表达式来注释,我们将访问这些表达式,以进行空指针引用检查。我们将数组建模为单个单元,因此,数组的每个加载和存储将被重定向到该单个单元。在完成对存储和加载的翻译之后,恢复对变量的所有可能的赋值。然后,我们运行标准的SSA 构造算法来插入对象域的 函数。所得到的IR称为完全基于堆的SSA (HSSA)。HSSA的一个例子如图3所示,在下文中将结合这个例子继续解释本发明的原理。[0095]图3示出了一段示例代码及其未修剪的HSSA形式。[0096]接下来,我们将图3所示的HSSA IR转换成图形形式,揭示价值计算结构,如,在抽象语法树中。我们称之为图形表示符号表达式(SEG)。 SEG是本发明提出的一种全新的数据结构。 [0097]图4示出了根据本发明的一个实施例生成的示例性的SEG。其中,灰色椭圆形节点表示终端值,未着色的椭圆形节点表示非终端值。实线和虚线代表数据和控制依赖性边。每个非终端值附加到控制依赖性边,以表示该值有效的条件。控制依赖性边的标签代表我们对条件的期望。为了清楚起见,忽略标记为true的控件依赖性边。在图4中,运算符用矩形灰色节点表示。[0098]形式上,SEG是一个4元组(V,O,D,C)。[0099]其中,V是一组值节点,节点的值分为终端值和非终端值。终端值表示在此函数之外生成的未知值。在该设计中,此函数可访问的参数、全局变量和堆位置的值是终端值,它们表示为图6底部的灰色节点。图6 中的椭圆形节点是非终端值,表示在此过程中生成的值。由于SEG的SSA 性质,我们还将唯一的内存位置与每个非终端值相关联,以将该值命名。[0100]O表示该算法中定义的所有运算符的运算符节点集合。[0101]D是一组数据依赖性边,在图4中以实线表示。[0102]C是一组控制依赖性边,在图4中以虚线表示。箭头侧的节点必须是逻辑运算的运算符节点。我们还用true或false来注释边,以表示逻辑运算的所需结果。[0103]终端值的集合也称为接口对象(IO),它们的正式定义如下:[0104] [0105] 10 CN 109426614 A 说 明 书 8/14页 是全局变量。IO的递归部分是通过以PIO作为根的指针取解引用可访问的存储器位置,例如, [0107]如下所示的算法1给出了构建SEG的伪代码。 [0108] [0109] 该算法以反向顺序(RPO)迭代基本块。对于每个基本块B,我们首先构建其路径条 其是对于来自 的所有路径p的路径约束 件 的分离。然而,这种路径条件可能非常冗长。压缩路径条件的想法是以递归形式重写其定义: 其中Bif是B的控制依赖基本块, 是使程序执行从Bif到B的条件。在算法1中,函数 GetBBCond(b)返回一对值(l,cin),其中l 是true或false标签,cin是B所依赖于的if条件。可以使用控制依赖图来容易地实现GetBBCond 函数。[0110]接下来,我们按顺序对每个基本块中的语句进行符号评估,并调用函数FindCreateExpr来逐步构建SEG。FindCreateExpr接受三个参数,它们是:运算符、操作数列表和路径条件。最相关的构造是 函数。我们必须计算门控函数γ,其中,γi是选择函数 的第i个元素的条件。使用下面的定理可以导出门控函数:[0111]假设xn=φ(x1,x2,…,xk), [0112][0113] 则有 其中,Predi(B)是B的第i个前导基本块。 11 CN 109426614 A[0114] 说 明 书 9/14页 如上所述,我们可以使用示例性的算法1构建根据本发明的SEG。由算法1构建的 SEG具有三个特征: [0115]1.我们将因子赋值解释为对象字段,作为强更新。例如, [0116]2.SEG是一个最大共享的图,SEG的每一个子图是唯一的,即,SEG 没有同构子图。FindAndCreateExpr函数可以避免相同的子图。一个例子是节点 [0117]3.由不同if语句中的两个或多个逻辑运算组成的路径条件紧凑地表示为逻辑运算控制依赖于另一逻辑运算。例如,!=运算符控制取决于<=运算符,它编码语句中的条件if(b<=0)和if(q!=NULL)。 [0118]重构每个变量的计算过程的原因为可以轻松地发现不可行的路径,并通过解析约束来排除错误的信息流。在本发明一实施例中,if(c>a) 和if(b≤0)的分支是不能同时进行的。因为,查询 SAT((c1=a0+b0)∧(c1>a0)∧(b0≤0))为false。 [0119]在下面的算法2中描述了使用SEG来确定NULL值存储器位置的有效方法。 [0120] 该算法是从NULL递归访问节点,从而为每个内存位置n计算Null 值条件 (NullCond(n))。这种方法的优点有两个方面。首先,可以利用Z3的增量解析能力,递增地将节点的控制依赖性添加到从第12行中的子节点上升的约束。因此,对第13行中的约束进行评估可以借用Z3 缓存的中间结果来评估孩子节点。其次,第13行SAT查询确保添加到第18行中的NullCond[n]的子约束真的可以导致Null值。 [0122]我们可以用NullCond(n)报告程序内的NPD错误。对于可能为NULL 的每个指针p,在路径条件ψ下,访问包含解引用的指针*(p+f)的所有语句。如果SAT(NullCond(p)∧p=NULL∧ψ),则我们报告错误。当空指针检查p≠NULL是ψ的一部分时,可以故意添加约束p=NULL以避免false警报。 [0123]下面结合一个具体实例来介绍本发明的缺陷检测方法。[0124]我们使用一段代码作为一个例子,该段代码片段包括三个语句: 12 [0121] CN 109426614 A[0125] 说 明 书 10/14页 … [0126]Z=φ(Z1,B1;null,B2);[0127]if(Z)X=Y+3;[0128]if(X>3)*Z;[0129]… [0130]其中,第一个语句Z=φ(Z1,B1;null,B2)表示在输入为B1情况下, Z=Z1;在输入为B2情况下,Z为空。第二个语句if(Z)X=Y+3表示在Z不为空的情况下,即,B1情况下,计算X的值,如果Z不为空则 X=Y+3。在Z为空的情况下,则X没有被赋值。第三个语句if(X>3)*Z 表示在X大于3的情况下解引用Z。 [0131]为上述待检测程序生成符号表达式图。如上文所述,符号表达式图包括值节点、运算符节点,以及连接节点的数据依赖性边和控制依赖性边,其中,值节点包括终端值节点和非终端值节点,终端值节点表示当前函数外生成的未知的值或常量,非终端值节点表示当前函数内生成的值,并且每个非终端值与一个唯一的内存地址相关联,数据依赖性边是将节点连接到与其有直接数据依赖关系的值节点的有方向性的边,控制依赖性边是当存在限定变量的条件时将变量连接到条件的有方向性的边。 [0132]图5A-5B示出了为上述代码片段生成SEG图的示意图。首先,如图 5A所示,对于第一个语句,Z=φ(Z1,B1;null,B2),为变量Z构建一个节点,并使用箭头61和62分别将Z节点连接到Z1和nil(空指针),该箭头代表数据依赖关系,我们将图5A中的箭头61和62称之为数据依赖性边。 [0133]对于第二个语句if(Z)X=Y+3,类似地,为变量X和Y、常数3、运算符+各构建一个节点,并用数据依赖性边连接这些节点。因为对X进行定义是有条件的,我们用控制依赖性边来将变量X连接到条件,在图 6B中以虚线箭头示出。实际上,每个节点都具有控制依赖性边,指向节点可以被定义的条件。[0134]最后一个语句if(X>3)*Z,在满足特定条件,即,X>3,的情况下,将节点*Z(Z的解引用)连接到Z。得到的SEG图如图5B所示。[0135]接下来,使用如上构建的SEG图来进行缺陷检测。通过在SEG图中从每个空指针源到每个解引用点进行搜索,可以找到空指针解引用。从图6A开始,从空节点开始沿着数据依赖性边,对SEG进行深度优先遍历。在该实例中,首先,如图6B所示,搜索空指针找到Z节点,并为 Z=null生成约束71,即,该约束条件为B1。然后,如图6C所示,搜索解引用点,添加约束72并检查约束是否被满足。如果满足,则生成错误报告。[0136]在访问解引用点之后,返回到追溯点Z,而不必从头开始遍历。在Z 点处,为解引用点弹出(即,去掉)上一个约束条件72,结果如图6D 所示。然后,如图6E所示,继续搜索其它空指针解引用地址并添加约束条件73,直到该SEG遍历完成为止。应注意,在访问解引用点之后不必从最开始的点搜索和构建约束。[0137]另一方面,还可基于SEG检测缓冲区溢出。缓冲区溢出的主要原因包括程序设计缺陷和危险库函数的使用。其中,程序的缺陷设计指的是在编写程序时,由于某些原因,没有考虑到会产生缺陷的因素,所以在设计时忽略掉这部分,导致存在程序缺陷的风险;而危险库函数的使用是指,某些库函数在执行时,由于没有考虑到该库函数特性,而导致影响程序本身的正确执行结果。 13 CN 109426614 A[0138] 说 明 书 11/14页 例如,以下示出一个缓冲区溢出代码片段: [0139] [0140] 从该代码片段中我们可以看到,一开始字符串缓冲区a只包含0长度的空字符串。 此时内存布局如下表: [0141] 程序运行,将空结束字符串“excessive”以ASCII编码写入缓冲区a 中。其中,该字 符串由9个字符字符组成,但在C风格字符串中包括空结束字符占10字节。由于复制时没有检测缓冲区长度,写入的数据同时覆盖了b的内存数据。如下表所示,现在的b的两个字节变成了65和0,对应ASCII编码的e和空结束字符。 [0143] [0142] [0144] 一方面,从程序设计缺陷的角度来说,因为在执行strcpy复制操作时,没有检测a的缓冲区空间是否足够,就直接进行复制,如果复制内容大于a的空间,就会导致溢出,也就导致原来在缓冲区中跟在a后面存储的b的值被替换掉;另一方面,从危险库函数的角度来说,例子中使用的strcpy函数不考虑复制对象和复制目标的大小是否一致,所以导致当复制目标的内存空间小于复制对象时,复制目标后的地址也被占用,而strncpy增加的参数n用于控制要复制的内容大小,所以strcpy就是一个危险库函数。[0146]有时操作系统检测到内存写入越界,并报出段错误(Segmentation Fault)且结束进程。当然,缓冲区溢出漏洞的完善,更多地还是看重程序的代码质量。在本例中,若将危险库函数strcpy替换为strncpy并加上相应限制,就不会引发此漏洞。相应地,修复后的代码片段如下: [0145] [0147] 14 CN 109426614 A[0148] 说 明 书 12/14页 对于缓冲区溢出,通常的分析方式是通过程序编译前的中间代码 (Intermediate Representation,IR)来构建控制流图(CFG)。但是对于缓冲区溢出问题而言,需要知道缓冲区大小以及欲写入内存数据的长度、以及触发时的程序可达性(Reachability)。对于可达性而言,可以用控制流图计算以及用程序可达性相关算法,如CFL-reachability算法等进行优化。由于程序的多变性,控制流会经常跨越于多个模块之间,因此可达性计算是一个前提条件。上文已提出了可达性计算的解决方式(例如,参数、全局变量和通过参数和全局变量可达的堆位置),在此不再赘述。 [0149]以下介绍基于SEG的缓冲区溢出检测方法。[0150]如上文所述,VFA的任务是计算一个抽象表示可能具有的抽象值集合,即上述VFA抽象域定义中的δ函数。同时VFA解析出程序所对应的抽象数值依赖,即具有该抽象值时的形成条件。为表示简单,我们将计算结果保存为函数。我们将特定条件的抽象值记为 其中 [0151] [0152]并且以下是从符号表示图获取抽象数值依赖的算法(请见下文的算法清 单)。 原理是从符号表示图中获得节点亲子信息,如果两个抽象值在函数表示图中相等,则将其相连并确定值等价或数值运算关系,最终得到一个符号值的所有符号依赖用于之后的计算。借助Z3工具的表达式简化能力,为了保证我们关注的符号值相等关系不被消元,在11行中我们让其自身相等以保留表达式。 [0154]缓冲区溢出的检测可以看做一个典型的源汇问题(Source-to-Sink),其可被描述为,内存单元被分配作为源头,缓冲区被使用作为汇集点。源头到汇集点此一路径可由先前得到的程序可达性中获取。因此,检查器可以被视为图7所示出的自动机,而汇集点为源头缓冲区内存指针通过值传递、别名、偏移量运算等方式最后被改写或读取指针对应的内存数据块。 15 [0153] CN 109426614 A[0155] 说 明 书 13/14页 知晓了源头到汇集点的程序控制流路径之后,我们就得到源头的缓冲区分配大小 s以及汇集点的被读取或被写入的长度l。当汇集点之前缓冲区经过了多次指针运算时,我们需要使用回溯算法获取真正的偏移量,即 [0156][0157][0158][0159][0160][0161] 其中, Δp=p-pred(p)即,最终偏移为先序指针偏移量之和。如果此时可以确定二者为常数并满足性质: 我们就可以认为发生了缓冲区溢出;如果不是,我们还需要进行符号约束演算。 [0162]当约束不是常数形式时,即,当源头的缓冲区大小或使用时的偏移量长度均未知、但具备数值依赖时,该问题可以被视为一个布尔可满足性问题(Satisfiability)。该问题被定义为布尔表达式的真值是否成立。对于缓冲区溢出检测而言,约束合取范式模内部还有涉及数值运算,例如: [0163]SAT((X+Y<3)∧(Y>3)) [0164]该问题被推广至实数运算范围,属于SMT(Satisfiability Modulo Theory)问题。有了数值流分析的结果,缓冲区溢出的断言为被定义为: [0165][0166] 对于每一个源头而言可能对应多个汇集点,因此需要逐一进行检查。在此,在一个实施例中,检查过程使用的是深度优先算法,并缓存约束以加速求解,算法描述如下:[0168]在此,第8行实际上是优化前的算法;实际运算时,直接退回上一步重新检查下一个叶子节点。利用Z3缓存的中间结果,可以迅速得出下一个邻近叶子结点的解。深度搜索每个缓冲区并缓存约束,以此方法遍历SEG,以得出汇总报告。[0169]图8A示出了以下代码的HSSA形式:[0170]len=10;[0171]buf=malloc(len); 16 [0167] CN 109426614 A[0172] 说 明 书 14/14页 buf[idx] [0173]buf[idx2] [0174]图8B至图8G则顺次示出了对应的SEG,以及相应的遍历过程。[0175]其中:图8B对应于操作[0176]push() [0177]cond(len=10) [0178]并缓存约束cond(len=10);[0179]图8C对应于操作[0180]push() [0181]cond(idx>=len)[0182]check() [0183]并缓存约束cond(len=10)AND cond(idx>=len);[0184]图8D对应于弹出操作,弹出约束AND cond(idx>=len);[0185]图8E对应于操作[0186]pop()[0187]push() [0188]cond(idx2>=len)[0189]check() [0190]并缓存约束cond(len=10)AND cond(idx2>=len);[0191]图8F对应于弹出操作,弹出约束AND cond(idx2>=len);[0192]图8G对应于操作[0193]pop()[0194]push()[0195]cond(other idx)[0196]…… [0197]以此类推,完成对缓冲区的遍历。[0198]相比于现有的动态检测方法(例如,Google的Address Sanitizer),上述对缓冲区溢出缺陷进行的静态分析方法能够直接定位到缺陷本身。由于现代程序复杂程度较高,高危安全漏洞往往不能被动态检查器检测到。而现有的静态检测方法包括数值范围分析,例如Sparrow、Seahorn 等工作,由于使用了抽象域过程间分析的拓宽算子(Widening Operator) 和缩紧算子(Narrowing Operator),与本发明提出的基于SEG的检测方法相比,跨模块分析层数太深会造成精度损失较大。[0199]通过以上所述的方法,在不必运行该程序的情况下即可找出可能存在的空指针解引用问题。使用SEG的工作流程具有灵活度高、速度快的优点。 [0200]以上通过结合具体例子示出和描述了本发明的示例性实施方式。应理解,本发明不限于本文描述的详细结构、设置方式或实现方法;本发明的保护范围仅由所附权利要求来定义,涵盖权利要求保护范围内的各种修改和变形。 17 CN 109426614 A 说 明 书 附 图 1/10页 图1 图2A 18 CN 109426614 A 说 明 书 附 图 2/10页 图2B 图3 19 CN 109426614 A 说 明 书 附 图 3/10页 图4 图5A 20 CN 109426614 A 说 明 书 附 图 4/10页 图5B 图6A 21 CN 109426614 A 说 明 书 附 图 5/10页 图6B 图6C 22 CN 109426614 A 说 明 书 附 图 6/10页 图6D 图6E 23 CN 109426614 A 说 明 书 附 图 7/10页 图7 图8A 24 CN 109426614 A 说 明 书 附 图 8/10页 图8B 图8C 25 CN 109426614 A 说 明 书 附 图 9/10页 图8D 图8E 26 CN 109426614 A 说 明 书 附 图 10/10页 图8F 图8G 27 因篇幅问题不能全部显示,请点此查看更多更全内容