软件学报

作者：高凤娟，王豫，陈天骄，司徒凌云，王林章，李宣东

单位：高凤娟，南京大学 计算机科学与技术系, 江苏 南京 210023;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002311,王豫，南京大学 计算机科学与技术系, 江苏 南京 210023;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002302,陈天骄，南京大学 计算机科学与技术系, 江苏 南京 210023;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002303,司徒凌云，南京大学 计算机科学与技术系, 江苏 南京 210023;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002304,王林章，南京大学 计算机科学与技术系, 江苏 南京 210023;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002305,李宣东，南京大学 计算机科学与技术系, 江苏 南京 210023;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 21002306

关键词：数组越界;静态分析;缓冲区溢出;约束求解

基金：国家重点研发计划（2017YFA0700604）；南京大学优秀博士研究生创新能力提升计划B；江苏省研究生科研与实践创新计划

随着移动计算、物联网、云计算、人工智能等领域的飞速发展，也涌现出了很多新的编程语言和编译器，但是C/C++语言依旧是最受欢迎的编程语言之一，而数组是C语言最重要的数据结构之一.当在程序中通过数组下标访问数组元素时，必须确保该下标在该数组的边界之内，否则就会导致数组越界.程序中的数组越界缺陷会使得程序在运行时导致系统崩溃，甚至使攻击者可以截取控制流以执行任意恶意代码.当前针对数组越界的静态检查方法无法达到高精度的分析，尤其是无法处理复杂约束和表达式，过多的误报额外增加了开发者的负担.因此，提出了一种基于污点分析的数组越界的静态检测方法.首先，提出流敏感、上下文敏感的按需指针分析方法，实现数组长度区间分析.然后，提出按需污点分析方法，实现数组下标和数组长度污染情况的计算.最后，定义数组越界缺陷判定规则，提出使用后向数据流分析方法，检测数组下标是否越界.在进行数组越界检测的过程中，为了处理程序中的复杂约束和表达式，在分析过程中将调用约束求解器来判断约束的可满足性.如果没有发现相应的语句，则报告数组越界缺陷警报.同时，实现了自动静态分析工具Carraybound，并通过实验展示了方法的有效性.

来源：2020年第10期

《软件学报》期刊编辑部

查看软件学报杂志2020年第10期