基于污点分析的数组越界缺陷的静态检测方法
作者:
作者单位:

作者简介:

高凤娟(1991-),女,学士,主要研究领域为软件工程,程序分析,软件测试,软件安全.
王豫(1991-),男,学士,主要研究领域为软件工程,程序分析,软件测试,软件安全.
陈天骄(1992-),男,硕士,主要研究领域为软件工程.
司徒凌云(1988-),男,博士,助理研究员,CCF学生会员,主要研究领域为软件工程,信息安全,静态分析,模糊测试.
王林章(1973-),男,博士,教授,博士生导师,CCF杰出会员,主要研究领域为软件工程,软件测试,软件安全.
李宣东(1963-),男,博士,博士生导师,CCF会士,主要研究领域为复杂软件建模与分析,软件测试与验证.

通讯作者:

王林章,E-mail:lzwang@nju.edu.cn

中图分类号:

基金项目:

国家重点研发计划(2017YFA0700604);南京大学优秀博士研究生创新能力提升计划B;江苏省研究生科研与实践创新计划


Static Checking of Array Index out of Bounds Defects in C Programs Based on Taint Analysis
Author:
Affiliation:

Fund Project:

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

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    随着移动计算、物联网、云计算、人工智能等领域的飞速发展,也涌现出了很多新的编程语言和编译器,但是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.

    参考文献
    相似文献
    引证文献
引用本文

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

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2020-01-02
  • 最后修改日期:2020-04-04
  • 录用日期:
  • 在线发布日期: 2020-06-11
  • 出版日期: 2020-10-06
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号