摘要
随着移动计算、物联网、云计算、人工智能等领域的飞速发展,也涌现出了很多新的编程语言和编译器,但是C/C++语言依旧是最受欢迎的编程语言之一,而数组是C语言最重要的数据结构之一.当在程序中通过数组下标访问数组元素时,必须确保该下标在该数组的边界之内,否则就会导致数组越界.程序中的数组越界缺陷会使得程序在运行时导致系统崩溃,甚至使攻击者可以截取控制流以执行任意恶意代码.当前针对数组越界的静态检查方法无法达到高精度的分析,尤其是无法处理复杂约束和表达式,过多的误报额外增加了开发者的负担.因此,提出了一种基于污点分析的数组越界的静态检测方法.首先,提出流敏感、上下文敏感的按需指针分析方法,实现数组长度区间分析.然后,提出按需污点分析方法,实现数组下标和数组长度污染情况的计算.最后,定义数组越界缺陷判定规则,提出使用后向数据流分析方法,检测数组下标是否越界.在进行数组越界检测的过程中,为了处理程序中的复杂约束和表达式,在分析过程中将调用约束求解器来判断约束的可满足性.如果没有发现相应的语句,则报告数组越界缺陷警报.同时,实现了自动静态分析工具Carraybound,并通过实验展示了方法的有效性.
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.
作者
高凤娟
王豫
陈天骄
司徒凌云
王林章
李宣东
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)
出处
《软件学报》
EI
CSCD
北大核心
2020年第10期2983-3003,共21页
Journal of Software
基金
国家重点研发计划(2017YFA0700604)
南京大学优秀博士研究生创新能力提升计划B
江苏省研究生科研与实践创新计划。
关键词
数组越界
静态分析
缓冲区溢出
约束求解
array index out-of-bounds
static analysis
buffer overflow
constraint solving
