###
Journal of Software:2020.31(10):2983-3003

基于污点分析的数组越界缺陷的静态检测方法
高凤娟,王豫,陈天骄,司徒凌云,王林章,李宣东
(南京大学 计算机科学与技术系, 江苏 南京 210023;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023)
Static Checking of Array Index out of Bounds Defects in C Programs Based on Taint Analysis
GAO Feng-Juan,WANG Yu,CHEN Tian-Jiao,SITU Ling-Yun,WANG Lin-Zhang,LI Xuan-Dong
(Department of Computer Science and Technology, Nanjing University, Nanjing 210023, China;State Key Laboratory for Novel Software Technology (Nanjing University), Nanjing 210023, China)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 985   Download 767
Received:January 02, 2020    Revised:April 04, 2020
> 中文摘要: 随着移动计算、物联网、云计算、人工智能等领域的飞速发展,也涌现出了很多新的编程语言和编译器,但是C/C++语言依旧是最受欢迎的编程语言之一,而数组是C语言最重要的数据结构之一.当在程序中通过数组下标访问数组元素时,必须确保该下标在该数组的边界之内,否则就会导致数组越界.程序中的数组越界缺陷会使得程序在运行时导致系统崩溃,甚至使攻击者可以截取控制流以执行任意恶意代码.当前针对数组越界的静态检查方法无法达到高精度的分析,尤其是无法处理复杂约束和表达式,过多的误报额外增加了开发者的负担.因此,提出了一种基于污点分析的数组越界的静态检测方法.首先,提出流敏感、上下文敏感的按需指针分析方法,实现数组长度区间分析.然后,提出按需污点分析方法,实现数组下标和数组长度污染情况的计算.最后,定义数组越界缺陷判定规则,提出使用后向数据流分析方法,检测数组下标是否越界.在进行数组越界检测的过程中,为了处理程序中的复杂约束和表达式,在分析过程中将调用约束求解器来判断约束的可满足性.如果没有发现相应的语句,则报告数组越界缺陷警报.同时,实现了自动静态分析工具Carraybound,并通过实验展示了方法的有效性.
Abstract:During the rapid development of mobile computing, IoT, cloud computing, artificial intelligence, etc, many new programming languages and compilers are emerging. Even so, C/C++ language is still one of the most popular languages. And array is one of the most important data structures of C language. It is necessary to check whether the index is within the boundary of the array when using it to access the element of an array in a program. Otherwise, array index out-of-bounds will happen unexpectedly. When there are array index out-of-bounds defects existing in programs, some serious errors may occur during execution, such as system crash. It is even worse that array index out-of-bounds defects open the doors for attackers to take control of the server and execute arbitrary malicious code by carefully constructing input and intercepting the control flow of the programs. Existing static methods for array boundary checking cannot achieve high accuracy and deal with complex constraints and expressions, which lead to too many false positives. And it will increase the burden of developers. In this study, a static checking method is proposed based on taint analysis. First, a flow-sensitive, context-sensitive, and on-demand pointer analysis is proposed to analyze the range of array length. Then, an on-demand taint analysis is performed for all array indices and array length expressions. Finally, the rules are defined for checking array index out of bounds defects and the checking is realized based on backward data flow analysis. During the analysis, in order to deal with complex constraints and expressions, it is proposed to check the satisfiability of the conditions by invoking the constraint solver. If none statement for avoiding array index out-of-bound is found in the program, an array index out-of-bound warning will be reported. An automatic static analysis tool, Carray bound have been implemented, and the experimental results show that Carraybound can work effectively and efficiently.
文章编号:     中图分类号:TP311    文献标志码:
基金项目:国家重点研发计划(2017YFA0700604);南京大学优秀博士研究生创新能力提升计划B;江苏省研究生科研与实践创新计划 国家重点研发计划(2017YFA0700604);南京大学优秀博士研究生创新能力提升计划B;江苏省研究生科研与实践创新计划
Foundation items:National Key Research and Development Program of China (2017YFA0700604); Program B for Outstanding PhD Candidate of Nanjing University; Postgraduate Research & Practice Innovation Program of Jiangsu Province of China
Reference text:

高凤娟,王豫,陈天骄,司徒凌云,王林章,李宣东.基于污点分析的数组越界缺陷的静态检测方法.软件学报,2020,31(10):2983-3003

GAO Feng-Juan,WANG Yu,CHEN Tian-Jiao,SITU Ling-Yun,WANG Lin-Zhang,LI Xuan-Dong.Static Checking of Array Index out of Bounds Defects in C Programs Based on Taint Analysis.Journal of Software,2020,31(10):2983-3003