软件学报ISSN1000-9825, CODEN RUXUE\ Journal of Software, 2019, 30(1): 80-109Idoi: 10. 13328/j cnki. jos. 0056511 ◎中国科学院软件研究所版权所有 Tel:+86-10-62562563 程序分析研究进展 回题回 张健2,张超,玄跻峰,熊莫飞,王千祥,梁彬’,李炼3,窦文生,陈振邦, 陈立前,蔡 计算机科学国家重点实验室(中国科学院软件研究所北京100190) (中国科学院大学北京10009) (清华大学网络科学与网络空间研究院北京100084) (武汉大学计算机学院湖北武汉430072) °(高可信软件技术教育部重点实验室(北京大学),北京100871) (华为技术有限公司,北京100095) 7(中国人民大学信息学院北京100872) 中国科学院计算技术研究所北京1001 因防科技大学计算机学院,湖南长沙410073) 通讯作者:张健, E-mail:zj@ 21osac cn 摘要:在信息化时代人们对软件的质量要求越来越高程序分析是保障软件质量的重要手段之一,日益受到学 术界和产业界的重视介绍了若干基本程序分析技术(抽象解释、数据流分析、基于摘要的分析、符号执行、动态 分析、基于机器学习的程序分析等)特别是最近10余年的研究进展进而介绍了针对不同类型软件(移动应用、并 发软件、分布式系统、二进制代码等)的分析方法最后展望了程序分析未来的研究方向和所面临的挑战. 关键词:程序分析软件质量保障;静态分析,动态分析 中图法分类号:TP311 中文引用格式:张健张超,玄跻峰,熊英飞,王千祥梁彬,李炼,窦文生,陈振邦陈立前,蔡彦程序分析研究进展软件 (1):80-109.http://www.jos.org.cn/1000-9825/5651.htm 英文引用格式: Zhang J, Zhang C, Xuan JI, Xiong YF, Wang Qx, Liang B,LiL, Dou ws, Chen ZB, Chen LQ,CaiY. Recent rogressinprogramanalysisRuanJianXueBao/journalofSoftware2019,30(1):80-109(inChinese).http://www.jos.org.cn/ 1000-9825/565lhtm Recent Progress in Program Analysis ZHANG Jian, 2 ZHANG Chao XUaN Ji-Fer XIONG Ying-Fei, WANG Qian-Xiang, LIANG Rin7 LI Lian2, 8 DoU Wen-Sheng 2. CHEN Zhen CHEN LI-Qian°, CAI Yan (State Key Laboratory of Computer Science(Institute of Software, Chinese Academy of Sciences), Beijing 100190, China) (University of Chinese Academy of Sciences, Beijing 100049, China) (Institute for Network Sciences and Cyberspace, Tsinghua University, Beijing 100084, China) 基金项目:国家重点基础研究发展计划(973)2014CB340701);中国科学院前沿科学重点项目( QYZDJ- SSW-SC036),国家自 然科学基金(61772308,U1736209,61872273,61672045,61472440,61632015,61872445,61502465) Foundation item: National Key Basic Research Program of China(973)(2014CB340701) Frontier Science Project of Academy of Sciences (QYZDJ-SSW-JSC036); National Natural Science Foundation of China (61772308, U1736209, 618 61672045,61472440,61632015,61872445,61502465) 本文由“软件学科发展回顾特刊”特约编辑梅宏教授、金芝教授、郝丹副教授推荐. 收稿时间:2018-08-08,修改时间:2018-08-30,采用时间:201809-25;j0s在线出版时间:2018-11-22 CNKI网络优先出版:2018-112307:1806,htp/ kns cnki.net/ kems/detai/.2560.TP20181123.0717006html
软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn Journal of Software,2019,30(1):80109 [doi: 10.13328/j.cnki.jos.005651] http://www.jos.org.cn ©中国科学院软件研究所版权所有. Tel: +86-10-62562563 程序分析研究进展 张 健 1,2, 张 超 3 , 玄跻峰 4 , 熊英飞 5 , 王千祥 6 , 梁 彬 7 , 李 炼 2,8, 窦文生 1,2, 陈振邦 9 , 陈立前 9 , 蔡 彦 1 1 (计算机科学国家重点实验室(中国科学院 软件研究所),北京 100190) 2 (中国科学院大学,北京 100049) 3 (清华大学 网络科学与网络空间研究院,北京 100084) 4 (武汉大学 计算机学院,湖北 武汉 430072) 5 (高可信软件技术教育部重点实验室(北京大学),北京 100871) 6 (华为技术有限公司,北京 100095) 7 (中国人民大学 信息学院,北京 100872) 8 (中国科学院 计算技术研究所,北京 100190) 9 (国防科技大学 计算机学院,湖南 长沙 410073) 通讯作者: 张健, E-mail: zj@ios.ac.cn 摘 要: 在信息化时代,人们对软件的质量要求越来越高.程序分析是保障软件质量的重要手段之一,日益受到学 术界和产业界的重视.介绍了若干基本程序分析技术(抽象解释、数据流分析、基于摘要的分析、符号执行、动态 分析、基于机器学习的程序分析等),特别是最近 10 余年的研究进展.进而介绍了针对不同类型软件(移动应用、并 发软件、分布式系统、二进制代码等)的分析方法.最后展望了程序分析未来的研究方向和所面临的挑战. 关键词: 程序分析;软件质量保障;静态分析;动态分析 中图法分类号: TP311 中文引用格式: 张健,张超,玄跻峰,熊英飞,王千祥,梁彬,李炼,窦文生,陈振邦,陈立前,蔡彦.程序分析研究进展.软件学报,2019, 30(1):80109. http://www.jos.org.cn/1000-9825/5651.htm 英文引用格式: Zhang J, Zhang C, Xuan JF, Xiong YF, Wang QX, Liang B, Li L, Dou WS, Chen ZB, Chen LQ, Cai Y. Recent progress in program analysis. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):80109 (in Chinese). http://www.jos.org.cn/ 1000-9825/5651.htm Recent Progress in Program Analysis ZHANG Jian1,2, ZHANG Chao3 , XUAN Ji-Feng4 , XIONG Ying-Fei5 , WANG Qian-Xiang6 , LIANG Bin7 , LI Lian2,8, DOU Wen-Sheng1,2, CHEN Zhen-Bang9 , CHEN Li-Qian9 , CAI Yan1 1 (State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China) 2 (University of Chinese Academy of Sciences, Beijing 100049, China) 3 (Institute for Network Sciences and Cyberspace, Tsinghua University, Beijing 100084, China) 基金项目: 国家重点基础研究发展计划(973)(2014CB340701); 中国科学院前沿科学重点项目(QYZDJ-SSW-JSC036); 国家自 然科学基金(61772308, U1736209, 61872273, 61672045, 61472440, 61632015, 61872445, 61502465) Foundation item: National Key Basic Research Program of China (973) (2014CB340701); Frontier Science Project of Chinese Academy of Sciences (QYZDJ-SSW-JSC036); National Natural Science Foundation of China (61772308, U1736209, 61872273, 61672045, 61472440, 61632015, 61872445, 61502465) 本文由“软件学科发展回顾特刊”特约编辑梅宏教授、金芝教授、郝丹副教授推荐. 收稿时间: 2018-08-08; 修改时间: 2018-08-30; 采用时间: 2018-09-25; jos 在线出版时间: 2018-11-22 CNKI 网络优先出版: 2018-11-23 07:18:06, http://kns.cnki.net/kcms/detail/11.2560.TP.20181123.0717.006.html
张健等:程序分析研究进展 ( School of Computer Science, Wuhan University, Wuhan 430072, China) (Key Laboratory of High Confidence Software Technologies of Ministry of Education(Peking University), Beijing 100871, China) Huawei Technologies Co. Ltd, Beijing 100095, China) '(School of Information, Renmin University of China, Beijing 100872, China) s(Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100190, China) (School of Computer, National University of Defense Technology, Changsha 410073, China) Abstract: In the information age, people are increasingly demanding high quality of software systems. Program analysis is one of the important approaches to guarantee the quality of software, and has been receiving attentions from academia and industry. This artic mainly focuses on the research progress in program analysis in the last decade. First, the article introduces the basic program analysis chniques, including abstract interpretation, data flow analysis, summary-based analysis, symbolic execution, dynamic analysis, machin learning-based program analysis, etc. Then, it summarizes program analysis approaches for different types of software systems, including mobile applications, concurrent software, distributed systems, binary code, etc. Finally, the article discusses potential research directions and challenges of program analysis in the future. Key words: program analysis, software quality assurance, static analysis; dynamic analy 随着信息化的不断发展,软件对人们生活的影响越来越大,在国民经济和国防建设中具有越来越重要的地 位如何提高软件质量,保证其行为的可信性,是学术界和工业界共同关注的重要问题要解决该问题应加强软 件开发过程管理,在全生命周期采取各种方法和技术提升软件质量由于软件系统的复杂性在编码实现完成之 后,甚至在软件产品发布、被广泛使用之后,往往还有各种各样的缺陷和漏洞各种软件测试和分析技术是发现 这些缺陷、漏洞的有效手段. 不同于很多黑盒测试方法,软件分析技术可深入软件系统内部细致地考察其结构及各个组成部分,进而发 现其各种特性,如性能、正确性、安全性等软件分析已逐渐发展成为程序语言和软件工程领域的一个重要研 究方向,并已影响到信息安全等相关领域进入21世纪以来,该方向进展显著,研究成果不断涌现软件分析不仅 可用来发现软件中的缺陷、漏洞,还可用于软件理解、修复以及测试用例生成等方面 软件包含程序和文档由于篇幅所限,本文主要介绍程序分析方面的研究特别是最近10余年该方向的 些重要工作本文将介绍程序分析的基本概念(分析对象、难度、评价等)、主要的基础性分析技术、针对不 类型分析对象的分析方法等最后简要提及一些挑战性问题以及新兴的研究方向 1程序分析简介 本节介绍程序分析的基本概念、程序及其性质多样性等进而解释程序分析的难度及其评价 基本概念 程序分析指的是:对计算机程序进行自动化的处理,以确认或发现其特性,比如性能、正确性、安全性等凹 程序分析的结果可用于编译优化、提供警告信息等,比如被分析程序在某处可能出现指针为空、数组下标越界 的情形等 传统上程序分析包括各种静态分析技术(类型检查、数据流分析、指向分析等)与动态分析技术所谓的静 态分析,是指对程序代码进行自动化的扫描、分析,而不必运行程序;与静态分析相对应的是动态分析技术其利 用程序运行过程中的动态信息分析其行为和特性 与程序分析密切相关的两类方法是形式验证及测试:前者试图通过形式化方法,严格证明程序具有某种性 质,目前,其自动化程度尚有不足,难于实用;测试方法多种多样在实际工程中广泛使用,这些方法也是以发现程 序中的缺陷为目的,它们一般都需要人们提供输入数据,以便运行程序观察其输出结果 12程序及其性质的多样性 程序分析内涵比较丰富,具有多样性 1)被分析对象的多样性
张健 等:程序分析研究进展 81 4 (School of Computer Science, Wuhan University, Wuhan 430072, China) 5 (Key Laboratory of High Confidence Software Technologies of Ministry of Education (Peking University), Beijing 100871, China) 6 (Huawei Technologies Co. Ltd., Beijing 100095, China) 7 (School of Information, Renmin University of China, Beijing 100872, China) 8 (Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100190, China) 9 (School of Computer, National University of Defense Technology, Changsha 410073, China) Abstract: In the information age, people are increasingly demanding high quality of software systems. Program analysis is one of the important approaches to guarantee the quality of software, and has been receiving attentions from academia and industry. This article mainly focuses on the research progress in program analysis in the last decade. First, the article introduces the basic program analysis techniques, including abstract interpretation, data flow analysis, summary-based analysis, symbolic execution, dynamic analysis, machine learning-based program analysis, etc. Then, it summarizes program analysis approaches for different types of software systems, including mobile applications, concurrent software, distributed systems, binary code, etc. Finally, the article discusses potential research directions and challenges of program analysis in the future. Key words: program analysis; software quality assurance; static analysis; dynamic analysis 随着信息化的不断发展,软件对人们生活的影响越来越大,在国民经济和国防建设中具有越来越重要的地 位.如何提高软件质量,保证其行为的可信性,是学术界和工业界共同关注的重要问题.要解决该问题,应加强软 件开发过程管理,在全生命周期采取各种方法和技术提升软件质量.由于软件系统的复杂性,在编码实现完成之 后,甚至在软件产品发布、被广泛使用之后,往往还有各种各样的缺陷和漏洞.各种软件测试和分析技术,是发现 这些缺陷、漏洞的有效手段. 不同于很多黑盒测试方法,软件分析技术可深入软件系统内部,细致地考察其结构及各个组成部分,进而发 现其各种特性,如性能、正确性、安全性等.软件分析已逐渐发展成为程序语言和软件工程领域的一个重要研 究方向,并已影响到信息安全等相关领域.进入 21 世纪以来,该方向进展显著,研究成果不断涌现.软件分析不仅 可用来发现软件中的缺陷、漏洞,还可用于软件理解、修复以及测试用例生成等方面[1]. 软件包含程序和文档.由于篇幅所限,本文主要介绍程序分析方面的研究,特别是最近 10 余年该方向的一 些重要工作.本文将介绍程序分析的基本概念(分析对象、难度、评价等)、主要的基础性分析技术、针对不同 类型分析对象的分析方法等.最后,简要提及一些挑战性问题以及新兴的研究方向. 1 程序分析简介 本节介绍程序分析的基本概念、程序及其性质多样性等,进而解释程序分析的难度及其评价. 1.1 基本概念 程序分析指的是:对计算机程序进行自动化的处理,以确认或发现其特性,比如性能、正确性、安全性等[2]. 程序分析的结果可用于编译优化、提供警告信息等,比如被分析程序在某处可能出现指针为空、数组下标越界 的情形等. 传统上,程序分析包括各种静态分析技术(类型检查、数据流分析、指向分析等)与动态分析技术:所谓的静 态分析,是指对程序代码进行自动化的扫描、分析,而不必运行程序;与静态分析相对应的是动态分析技术,其利 用程序运行过程中的动态信息,分析其行为和特性. 与程序分析密切相关的两类方法是形式验证及测试:前者试图通过形式化方法,严格证明程序具有某种性 质,目前,其自动化程度尚有不足,难于实用;测试方法多种多样,在实际工程中广泛使用,这些方法也是以发现程 序中的缺陷为目的,它们一般都需要人们提供输入数据,以便运行程序,观察其输出结果. 1.2 程序及其性质的多样性 程序分析内涵比较丰富,具有多样性. 1) 被分析对象的多样性
Journal of so/hare软件学报Vol.30,No., January2019 程序分析的对象既可以是源代码,也可以是二进制可执行代码对于源程序,根据其实现语言不同,可能需 要不同的分析技术比如C程序和Java程序的分析,其技术可能就不一样后者需要处理一些面向对象的结构 即使是同一种高级语言编写的程序,也可能具有不同的特性比如程序中是否有比较多的指针?是否使用并发 控制结构、通信机制?是否有大量的数值计算从规模看,被分析的程序可以是几百行的代码,也可以是几十万行 乃至于上千万行代码 2)程序性质的多样性 对不同类型的程序在不同的应用环境下,人们关注的性质也不一样以C程序为例,很多C程序会用到指 针,用于动态分配、释放内存对这样的程序,人们会关注空指针、内存泄漏等问题但对某些嵌入式系统来说, 程序中很少动态分配内存空间,却可能要处理中断另外一些C程序可能有大量的数值(浮点数)计算程序员可 能更关注其中是否存在溢出问题 13程序分析的难度及评价 由于程序语言的复杂性、程序性质的多样性自动化的程序分析往往具有相当大的难度根据Rce定理对 于程序行为的任何非平凡属性都不存在可以检查该属性的通用算法也就是说大量的程序分析问题都是不 可判定的比如,一般情况下,程序的终止性就是不可判定的也就是说,不存在一种算法,它能判断任何给定的程 序是否总能终止程序路径的可行性( path feasibility)是不可判定的如果存在输入数据使得程序沿着一条 路径执行,程序中该路径被称为是可行的( feasible)没有一种算法,它能判断程序中某条给定路径是否可行最 近 Cousot等人从抽象解释的角度形式化地证明了:从可计算性角度看,相比程序验证(只需要检查一个给定的 程序不变式是否正确)程序分析(需要综合出正确的程序不变式)是一个更难的问题具体而言:对于证明有穷域 上的程序断言,程序分析与程序验证是等价的问题但是对于无穷域上的断言程序分析比程序验证更难 鉴于程序分析的理论难度以及被分析程序的复杂度我们往往不要求对程序进行完全精确的分析这就可 能带来误报( false positive)、漏报( false negative)等问题:前者指的是报警信息指出的缺陷实际上不存在、不可 能发生;后者指的是程序中存在的某个缺陷,没有被程序分析工具所发现 对程序分析技术或工具进行评价,不仅要看其分析对象的规模、复杂度分析过程的效率还要看其对用户 的要求发现缺陷的严重程度,以及误报率、漏报率等 2程序分析方法和技术 本节主要介绍一些近期有重要进展的程序分析方法和技术,包括抽象解释、数据流分析、基于摘要的过程 间分析、符号执行、动态分析、基于机器学习的程序分析等这6项方法和技术的关系如图1所示 据流分析过程间 F执行‖动态分析 基础理论抽象解 Fig 1 Main program analysis techniques 图1主要的程序分析技术 程序分析总体可以分为静态分析和动态分析,涉及的基础理论包括抽象解释、约束求解、自动推理等而 静态分析的关键技术包括数据流分析、过程间分析、符号执行等最后近期机器学习技术被用于提升各种不 同的程序分析技术 除了这6种基本程序分析技术之外,还有一些其他广泛使用的程序分析技术也在近期有显著进展,如污点 分析、模型检验、编程规则检查等由于受篇幅所限,本文将不再对这些技术进行详述 2.1抽象解释 抽象解释是一种对程序语义进行可靠抽象(或近似)的通用理论该理论为程序分析的设计和构建提供了
82 Journal of Software 软件学报 Vol.30, No.1, January 2019 程序分析的对象既可以是源代码,也可以是二进制可执行代码.对于源程序,根据其实现语言不同,可能需 要不同的分析技术.比如,C 程序和 Java 程序的分析,其技术可能就不一样:后者需要处理一些面向对象的结构. 即使是同一种高级语言编写的程序,也可能具有不同的特性.比如,程序中是否有比较多的指针?是否使用并发 控制结构、通信机制?是否有大量的数值计算.从规模看,被分析的程序可以是几百行的代码,也可以是几十万行 乃至于上千万行代码. 2) 程序性质的多样性 对不同类型的程序,在不同的应用环境下,人们关注的性质也不一样.以 C 程序为例,很多 C 程序会用到指 针,用于动态分配、释放内存.对这样的程序,人们会关注空指针、内存泄漏等问题.但对某些嵌入式系统来说, 程序中很少动态分配内存空间,却可能要处理中断.另外一些 C 程序可能有大量的数值(浮点数)计算,程序员可 能更关注其中是否存在溢出问题. 1.3 程序分析的难度及评价 由于程序语言的复杂性、程序性质的多样性,自动化的程序分析往往具有相当大的难度.根据 Rice 定理:对 于程序行为的任何非平凡属性,都不存在可以检查该属性的通用算法[3].也就是说,大量的程序分析问题都是不 可判定的.比如,一般情况下,程序的终止性就是不可判定的.也就是说,不存在一种算法,它能判断任何给定的程 序是否总能终止.程序路径的可行性(path feasibility)也是不可判定的[4].如果存在输入数据使得程序沿着一条 路径执行,程序中该路径被称为是可行的(feasible).没有一种算法,它能判断程序中某条给定路径是否可行.最 近,Cousot 等人[5]从抽象解释的角度形式化地证明了:从可计算性角度看,相比程序验证(只需要检查一个给定的 程序不变式是否正确),程序分析(需要综合出正确的程序不变式)是一个更难的问题.具体而言:对于证明有穷域 上的程序断言,程序分析与程序验证是等价的问题;但是对于无穷域上的断言,程序分析比程序验证更难. 鉴于程序分析的理论难度以及被分析程序的复杂度,我们往往不要求对程序进行完全精确的分析.这就可 能带来误报(false positive)、漏报(false negative)等问题:前者指的是报警信息指出的缺陷实际上不存在、不可 能发生;后者指的是程序中存在的某个缺陷,没有被程序分析工具所发现. 对程序分析技术或工具进行评价,不仅要看其分析对象的规模、复杂度,分析过程的效率,还要看其对用户 的要求,发现缺陷的严重程度,以及误报率、漏报率等. 2 程序分析方法和技术 本节主要介绍一些近期有重要进展的程序分析方法和技术,包括抽象解释、数据流分析、基于摘要的过程 间分析、符号执行、动态分析、基于机器学习的程序分析等.这 6 项方法和技术的关系如图 1 所示. 提升手段 基于机器学习的程序分析 关键技术 数据流分析 过程间分析 符号执行 动态分析 基础理论 抽象解释 约束求解 自动推理 静态分析 动态分析 Fig.1 Main program analysis techniques 图 1 主要的程序分析技术 程序分析总体可以分为静态分析和动态分析,涉及的基础理论包括抽象解释、约束求解、自动推理等.而 静态分析的关键技术包括数据流分析、过程间分析、符号执行等.最后,近期机器学习技术被用于提升各种不 同的程序分析技术. 除了这 6 种基本程序分析技术之外,还有一些其他广泛使用的程序分析技术也在近期有显著进展,如污点 分析、模型检验、编程规则检查[6]等,由于受篇幅所限,本文将不再对这些技术进行详述. 2.1 抽象解释 抽象解释是一种对程序语义进行可靠抽象(或近似)的通用理论[7].该理论为程序分析的设计和构建提供了
张健等:程序分析研究进展 一个通用的框架并从理论上保证了所构建的程序分析的终止性和可靠性(即考虑了所有的程序行为)基于抽 象解释来设计程序分析,本质上是通过对程序语义进行不同程度的抽象,以在分析精度和计算效率之间取得权 衡这种由某种语义抽象及其上的操作所构成的数学结构称为抽象域抽象解释采用 Galois连接来刻画具体域 与抽象域之间的关系设D)和D,=)是两个给定的偏序集函数aD→D及yD→D构成的函数对(a)称为D 与D之间的 Galois连接,当且仅当vx∈D,x∈D,a(x)=”x2xx(x2),其中,D,)称为具体域(D",=)称为抽象域a 称为抽象化函数称为具体化函数由定义中的性质a(x)=x(亦即xxx)可知x是x的可靠抽象(又称上近 似)给定具体域(D,)和抽象域DP,)之间的 Galois连接(a外,对于具体域D上的函数∫和抽象域D"上的函数 f,当Vx∈D,(y(x)c(y/")(x)时我们称f是∫的可靠抽象抽象解释理论的一个重要思想是通过在抽象域上 计算程序的抽象不动点来表达程序的抽象语义在程序分析中,程序状态集合通过抽象域中的域元素来近似而 程序语义动作(如赋值、条件测试等)通过抽象域中的域操作(如迁移函数)来可靠建模此外,为了加速抽象域上 不动点迭代的收敛速度并保证不动点迭代的终止性抽象解释框架提供了加宽算子( widening)抽象解释框架能 够保证抽象域上迭代求得的抽象不动点是程序最小不动点(对应程序的具体聚集语义)的上近似换言之,抽象 解释提供了严格的理论来保证基于上近似抽象的推理的可靠性即:所有基于上近似抽象推理得出的性质在原 程序中也必然成立但是由于抽象带来的精度损失,不保证所有在原程序中成立的性质都能基于上近似抽象推 里得到 抽象域是抽象解释框架下的核心要素,一般是面向某类特定性质设计的到目前为止,已出现了数十种面向 不同性质的抽象域其中,具有代表性的抽象域包括区间抽象域、八边形抽象域、多面体抽象域等数值抽象域 此外还出现了若干开源的抽象域库,如 APRON、 ELINA、PP山等基于抽象解释的程序分析工具也不断 涌现,出现了 Polypase!2 Astree1等商业化工具和 Frama-C≌ alue analysis!、 CCCheck(code contract static checker) 51、 Interpol1等学术界工具随着这些工具的日益完善,抽象解释在工业界大规模软件尤其是嵌入式 软件的分析与验证中得到了成功应用典型的应用案例是, Astre成功应用于空客A340(约13.2万行C代码) A380(约35万行C代码)等系列飞机飞行控制软件的自动分析并实现了分析的零误报最近Asre的扩展版 本 street支持多线程C程序中运行时错误、数据竞争、死锁等的检测,并成功应用于 ARINC653航空电子 应用软件(约220万行代码)的分析总体而言基于抽象解释的程序分析主要面临提高分析精度、可扩展性两 方面的挑战 在提高分析精度方面,基于加宽的不动点迭代过程所导致的分析精度损失问题和抽象域本身表达能力的 !性是当前面临的主要问题 ·在缓解加宽所导致的精度损失方面,近年来的研究进展大致可以分为两种思路:(1)使用基于策略迭 代或抽象加速1的不动点迭代过程来取代传统的基于加宽的不动点迭代过程,以获得更精确的分 析结果,但是,该方法只适用于一些特殊类别的程序和抽象域(2)改进加宽/变窄算子及其迭代序列如 结合加宽变窄算子的交叠迭代策略21 ·在弥补抽象域本身表达能力的局限性方面最近的研究进展可分为3类:(1)将符号化方法与抽象方法 合起来利用SMT求解器2)、插值等技术来计算程序中语句迁移函数的最佳抽象,以改进抽象 域在语句迁移函数上的精度损失、(2)提高抽象域的析取表达能力如基于区间线性代数、绝对值约 束、集合差、非格结构、决策树等方法构造的非凸抽象域26,(3)提高抽象域的非线性表达能力,如 基于组合递推分析p28将符号化分析与抽象解释结合起来以生成多项式、指数、对数等形式非线性 不变式基于椭圆幂集来生成二次不变式等 在提高可扩展性方面如何有效降低分析过程中抽象状态表示与计算的时空开销是目前考虑的主要问题 在这方面最近的研究进展包括: 利用变量访问的局部性原理,降低当前抽象环境中所涉及的变量维数,并根据数据流依赖的稀疏性, 降低抽象状态的存储开销和传播开销基于该思想,最近Oh等人提出了一种通用的全局稀疏分析框 架,在不损失分析精度的前提下能够显著降低时空开销,并在静态分析工具 Sparrow上进行了应用,取
张健 等:程序分析研究进展 83 一个通用的框架[8],并从理论上保证了所构建的程序分析的终止性和可靠性(即考虑了所有的程序行为).基于抽 象解释来设计程序分析,本质上是通过对程序语义进行不同程度的抽象,以在分析精度和计算效率之间取得权 衡.这种由某种语义抽象及其上的操作所构成的数学结构称为抽象域.抽象解释采用 Galois 连接来刻画具体域 与抽象域之间的关系.设D,⊑和D# ,⊑# 是两个给定的偏序集,函数:DD# 及:D# D构成的函数对(,)称为 D 与 D# 之间的 Galois 连接,当且仅当xD,x# D# ,(x)⊑# x# x⊑(x# ),其中,D,⊑称为具体域,D# ,⊑# 称为抽象域, 称为抽象化函数,称为具体化函数.由定义中的性质(x)⊑# x# (亦即 x⊑(x# ))可知,x# 是 x 的可靠抽象(又称上近 似).给定具体域D,⊑和抽象域D# ,⊑# 之间的 Galois 连接(,),对于具体域 D 上的函数 f 和抽象域 D# 上的函数 f # ,当x# D# ,(f)(x# )⊑(f # )(x# )时,我们称 f # 是 f 的可靠抽象.抽象解释理论的一个重要思想是,通过在抽象域上 计算程序的抽象不动点来表达程序的抽象语义.在程序分析中,程序状态集合通过抽象域中的域元素来近似,而 程序语义动作(如赋值、条件测试等)通过抽象域中的域操作(如迁移函数)来可靠建模.此外,为了加速抽象域上 不动点迭代的收敛速度并保证不动点迭代的终止性,抽象解释框架提供了加宽算子(widening).抽象解释框架能 够保证抽象域上迭代求得的抽象不动点是程序最小不动点(对应程序的具体聚集语义)的上近似.换言之,抽象 解释提供了严格的理论来保证基于上近似抽象的推理的可靠性,即:所有基于上近似抽象推理得出的性质,在原 程序中也必然成立.但是,由于抽象带来的精度损失,不保证所有在原程序中成立的性质都能基于上近似抽象推 理得到. 抽象域是抽象解释框架下的核心要素,一般是面向某类特定性质设计的.到目前为止,已出现了数十种面向 不同性质的抽象域.其中,具有代表性的抽象域包括区间抽象域、八边形抽象域、多面体抽象域等数值抽象域. 此外,还出现了若干开源的抽象域库,如 APRON[9]、ELINA[10]、PPL[11]等.基于抽象解释的程序分析工具也不断 涌现,出现了 PolySpace[12]、Astrée[13]等商业化工具和 Frama-C Value Analysis[14]、CCCheck(code contract static checker)[15]、Interproc[16]等学术界工具.随着这些工具的日益完善,抽象解释在工业界大规模软件,尤其是嵌入式 软件的分析与验证中得到了成功应用.典型的应用案例是,Astrée 成功应用于空客 A340(约 13.2 万行 C 代码)、 A380(约 35 万行 C 代码)等系列飞机飞行控制软件的自动分析并实现了分析的零误报[17].最近,Astrée 的扩展版 本 AstréeA 支持多线程 C 程序中运行时错误、数据竞争、死锁等的检测,并成功应用于 ARINC 653 航空电子 应用软件(约 220 万行代码)的分析[18].总体而言,基于抽象解释的程序分析主要面临提高分析精度、可扩展性两 方面的挑战. 在提高分析精度方面,基于加宽的不动点迭代过程所导致的分析精度损失问题和抽象域本身表达能力的 局限性是当前面临的主要问题. 在缓解加宽所导致的精度损失方面,近年来的研究进展大致可以分为两种思路:(1) 使用基于策略迭 代[19]或抽象加速[20]的不动点迭代过程来取代传统的基于加宽的不动点迭代过程,以获得更精确的分 析结果,但是,该方法只适用于一些特殊类别的程序和抽象域;(2) 改进加宽/变窄算子及其迭代序列,如 结合加宽变窄算子的交叠迭代策略[21]. 在弥补抽象域本身表达能力的局限性方面,最近的研究进展可分为 3 类:(1) 将符号化方法与抽象方法 结合起来,利用 SMT 求解器[22,23]、插值[24]等技术来计算程序中语句迁移函数的最佳抽象,以改进抽象 域在语句迁移函数上的精度损失;(2) 提高抽象域的析取表达能力,如基于区间线性代数、绝对值约 束、集合差、非格结构、决策树等方法构造的非凸抽象域[25,26];(3) 提高抽象域的非线性表达能力,如 基于组合递推分析[27,28]将符号化分析与抽象解释结合起来以生成多项式、指数、对数等形式非线性 不变式,基于椭圆幂集来生成二次不变式[29]等. 在提高可扩展性方面,如何有效降低分析过程中抽象状态表示与计算的时空开销是目前考虑的主要问题. 在这方面,最近的研究进展包括: 利用变量访问的局部性原理,降低当前抽象环境中所涉及的变量维数,并根据数据流依赖的稀疏性, 降低抽象状态的存储开销和传播开销.基于该思想,最近,Oh 等人提出了一种通用的全局稀疏分析框 架,在不损失分析精度的前提下能够显著降低时空开销,并在静态分析工具 Sparrow 上进行了应用,取
Journal of software软件学报Vol.30,No.1, January2019 得了显著的可扩展性提升效果0,3 利用矩阵分解等在线分解优化策略来对抽象域操作的算法进行优化.基于该思想,最近, Singh等 人B23对常用的八边形抽象域、多面体抽象域的实现进行了优化优化后分析的性能取得了显著的 提升性能提升最大的达140多倍在此基础上, Singh等人还提出了一种通用的基于分解的优化策 ,能够在不改变基抽象域的基础上自动实现基于分解的优化从而无需人工重新实现基抽象域, 并基于这一思想实现了开源抽象域库 ELINA这种基于在线分解的方法不会造成精度损失 最近, Singh等人还提出了一种基于强化学习来加速静态程序分析的方法在每次迭代过程中,利用强化 学习来决策选择哪个转换子以在精度和不动点迭代收敛速度之间进行权衡在抽象域编码实现上 Becchi等 人最近改进了未必封闭多面体域(支持严格不等式约束)的双重描述法在表示中避免了松弛变量的引入,极 大地提高了分析效率并开发了多面体域的开源实现 PPLite 此外,将抽象解释应用到特定类型程序或特定性质的分析验证方面的研究也取得了不少进展,主要的关注 点包括复杂数据结构自动分析的支持、不同谱系目标程序的支持、活性性质分析的支持在复杂数据结构的自 分析方面最近的研究重点关注针对数组内容的精确分析、混杂数据结构的建模3、数值与形态混合的 程序分析围、关系型形态分析1在支持不同谱系目标程序方面最近的研究重点关注多线程程序的自动分 析1、中断驱动型程序的自动分析4、概率程序的分析:4、操作系统代码的安全和功能性分析13846 近年来在抽象解释领域出现了一些新的用来分析时序性质和终止性的方法下析在目标性质支持方面 未来,抽象解释技术将进一步在新的架构、语言、应用等实际需求驱动下不断发展值得关注的方向包括 对弱内存模型的分析验证、神经网络的分析与验证巧、大数据处理相关错误的分析、 Python程序的 自动分析等与约束求解、自动推理、人工智能等基础支撑技术的紧密结合,将是抽象解释后续的研究趋势 之一5961同时,降低误报率将依然是基于抽象解释的程序分析技术拓展实际应用的研究挑战和重点 2.2数据流分析 数据流分析通过分析程序状态信息在控制流图中的传播来计算每个静态程序点(语句)在运行时可能出现 的状态经典的数据流分析理论62用有限高度的格L来抽象表示所有可能状态的集合并对每个程序语句定 义一个单调的转移函数( transfer function),以计算其对程序状态的更新数据流分析可以是前向或后向,对应程 序状态信息在控制流图中的前向或后向传播在程序控制流图中,多个分支交汇的程序点状态为其所有前驱(或 后继,如果是后向传播)程序点状态的几表示不同执行路径下可能出现的所有程序状态 数据流分析为抽象解释的一个特例,其计算的状态信息(抽象域)局限于有限高度的格L,)数据流分析己 编译器实现中得到广泛应用常见的应用包括常数传播分析、部分冗余分析等相比于通用的抽象解释理 论,经典数据流分析的实现可以通过一个迭代计算框架来计算所有语句的输出直至不动点单调性和格的有限 高度保证了数据流分析迭代计算框架的收敛性而无需引入加宽算子编译器中的数据流分析多为过程内数据 流分析,全局过程间的分析可以使用基于摘要的方法,通过对函数自动分析摘要得以实现近年来,对数据流分 析方向的应用己不仅仅局限于编译优化,研究者们也提出了多种方法来高效实现过程间的上下文敏感的数据 流分析,主要包括如下两种方法 I) IFDS/IDE数据流分析框架 IFDS分析框架由Reps等人于1995年提出IFDS将抽象域(即数据流分析计算的状态信息)为满足分配 性的有限集合的一大类数据流分析问题转换为一个图可达问题,从而能够有效地进行上下文敏感的过程间分 析.IFDS框架基于程序过程间控制流图定义了一个超级流图( supergraph),其中,每个节点对应在一个程序点的 抽象域中的一个元素;而节点间的边表示该元素在过程间控制流图的传播对应着数据流分析中的转移函数通 过求解是否存在从程序入口到每个程序点的一个可达路径我们可以得到该程序点的状态信息基于该分析方 法的框架已经实现于开源分析系统,如Soot和wala中,并广泛用于包括 Android污点分析在内的多种应
84 Journal of Software 软件学报 Vol.30, No.1, January 2019 得了显著的可扩展性提升效果[30,31]; 利用矩阵分解等在线分解优化策略来对抽象域操作的算法进行优化.基于该思想,最近,Singh 等 人[32,33]对常用的八边形抽象域、多面体抽象域的实现进行了优化,优化后,分析的性能取得了显著的 提升,性能提升最大的达 140 多倍;在此基础上,Singh 等人还提出了一种通用的基于分解的优化策 略[34],能够在不改变基抽象域的基础上自动实现基于分解的优化,从而无需人工重新实现基抽象域, 并基于这一思想实现了开源抽象域库 ELINA.这种基于在线分解的方法不会造成精度损失. 最近,Singh 等人[35]还提出了一种基于强化学习来加速静态程序分析的方法,在每次迭代过程中,利用强化 学习来决策选择哪个转换子,以在精度和不动点迭代收敛速度之间进行权衡.在抽象域编码实现上,Becchi 等 人[36]最近改进了未必封闭多面体域(支持严格不等式约束)的双重描述法,在表示中避免了松弛变量的引入,极 大地提高了分析效率,并开发了多面体域的开源实现 PPLite. 此外,将抽象解释应用到特定类型程序或特定性质的分析验证方面的研究也取得了不少进展,主要的关注 点包括复杂数据结构自动分析的支持、不同谱系目标程序的支持、活性性质分析的支持.在复杂数据结构的自 动分析方面,最近的研究重点关注针对数组内容的精确分析[37]、混杂数据结构的建模[38]、数值与形态混合的 程序分析[39,40]、关系型形态分析[41].在支持不同谱系目标程序方面,最近的研究重点关注多线程程序的自动分 析[18]、中断驱动型程序的自动分析[42,43]、概率程序的分析[44,45]、操作系统代码的安全和功能性分析[38,46]、 JavaScript 等动态语言的分析[47]、二进制代码的分析[48]、Web 应用程序的安全性分析[49].在目标性质支持方面, 近年来,在抽象解释领域出现了一些新的用来分析时序性质和终止性的方法[5052]. 未来,抽象解释技术将进一步在新的架构、语言、应用等实际需求驱动下不断发展.值得关注的方向包括 对弱内存模型的分析验证[53,54]、神经网络的分析与验证[55,56]、大数据处理相关错误的分析[57]、Python 程序的 自动分析[58]等.与约束求解、自动推理、人工智能等基础支撑技术的紧密结合,将是抽象解释后续的研究趋势 之一[5961].同时,降低误报率将依然是基于抽象解释的程序分析技术拓展实际应用的研究挑战和重点. 2.2 数据流分析 数据流分析通过分析程序状态信息在控制流图中的传播来计算每个静态程序点(语句)在运行时可能出现 的状态.经典的数据流分析理论[62]用有限高度的格L,来抽象表示所有可能状态的集合,并对每个程序语句定 义一个单调的转移函数(transfer function),以计算其对程序状态的更新.数据流分析可以是前向或后向,对应程 序状态信息在控制流图中的前向或后向传播.在程序控制流图中,多个分支交汇的程序点状态为其所有前驱(或 后继,如果是后向传播)程序点状态的,表示不同执行路径下可能出现的所有程序状态. 数据流分析为抽象解释的一个特例,其计算的状态信息(抽象域)局限于有限高度的格L,.数据流分析已 经在编译器实现中得到广泛应用,常见的应用包括常数传播分析、部分冗余分析等.相比于通用的抽象解释理 论,经典数据流分析的实现可以通过一个迭代计算框架来计算所有语句的输出直至不动点.单调性和格的有限 高度保证了数据流分析迭代计算框架的收敛性,而无需引入加宽算子.编译器中的数据流分析多为过程内数据 流分析,全局过程间的分析可以使用基于摘要的方法,通过对函数自动分析摘要得以实现.近年来,对数据流分 析方向的应用已不仅仅局限于编译优化,研究者们也提出了多种方法来高效实现过程间的上下文敏感的数据 流分析,主要包括如下两种方法. 1) IFDS/IDE 数据流分析框架 IFDS 分析框架由 Reps 等人[63]于 1995 年提出.IFDS 将抽象域(即数据流分析计算的状态信息)为满足分配 性的有限集合的一大类数据流分析问题转换为一个图可达问题,从而能够有效地进行上下文敏感的过程间分 析. IFDS 框架基于程序过程间控制流图定义了一个超级流图(supergraph),其中,每个节点对应在一个程序点的 抽象域中的一个元素;而节点间的边表示该元素在过程间控制流图的传播,对应着数据流分析中的转移函数.通 过求解是否存在从程序入口到每个程序点的一个可达路径,我们可以得到该程序点的状态信息.基于该分析方 法的框架已经实现于开源分析系统,如 Soot[64]和 Wala[65]中,并广泛用于包括 Android 污点分析[66]在内的多种应
张健等:程序分析研究进展 用中 Reps等人的后续进一步扩展了该框架,通过已有抽象域为环境而计算得到新的属性用于过程间常数传播 等应用中,并形式化定义了上述图可达问题为上下文无关文法图可达问题上下文无关文法图可达问题对图中 的边进行标号,图中任意两点可达需要两点间的一条路径上的标号串满足事先定义的上下文无关文法多种不 同程序分析问题均可表示为对上下文无关文法图可达问题的求解近年来,包括指针分析68,69、并行程序分 析m,m等多种分析技术均通过求解上下文无关文法图可达问题来有效地加以实现 2)基于值流图的稀疏数据流分析方法 传统的数据流分析在程序控制流图上将所需计算的状态信息在每个程序点传播得到最终分析结果此过 程通常存在较多冗余操作,对效率,特别是过程间数据流分析效率会有很大影响为了进一步提高数据流分析的 效率,近年来,研究者们提出了多种稀疏的分析方法从而无需计算状态信息在每个程序点的传播即可得到与数 据流分析相同的结果该类分析技术D通过一个稀疏的值流图 alue flow graph)直接表示程序变量的依赖关 系,从而使得状态信息可以有效地在该稀疏的值流图上传播该值流图保证了状态信息可以有效地传播到其 要使用该信息的程序点并避免了在无效程序点的冗余传播,可大幅度提高效率 2.3基于摘要的过程间分析 摘要 summary)是可复用的程序模块分析结果,能够简要地刻画模块的外部行为创建摘要和利用摘要开展 分析的过程称为摘要分析在编写程序的过程中,一个程序模块往往需要调用其他程序模块对主调( caller)模块 的分析必然涉及到对被调模块(cale的分析与复用被调模块代码可提高软件生产效率类似,摘要分析期望复 用被调模块的分析结果也能提高分析主调模块的效率通过基于摘要的程序分析技术我们将被复用模块的分 析结果被构造成为摘要,并在分析主调模块时对其实例化以加快分析速度 传统摘要分析的研究主要关注模块化( modular)分析,即:在分析过程中将软件划分为多个模块,对各个模块 分别分析和创建摘要,然后合并摘要获得整体的分析结果这样在分析过程中创建摘要的技术也称为在线摘要 技术摘要分析在最近10年的主要进展是离线摘要技术,即在程序分析之前对常用代码库生成摘要,从而加快 使用这些代码库的客户端的分析速度离线摘要根据其自动化程度的不同,可以分成人工编写摘要和自动生成 摘要,分别在接下来的两小节中加以介绍 1)人工编写摘要 对于程序中一些难以分析的代码,例如第三方的库和系统代码等,可采用人工编写摘要的方式近似代码的 行为这种技术原先应用于程序验证中,比如ESC/Java通过用户提供的前置条件和后置条件来对程序进行模块 化验证 Flow!∽在处理调用系统代码和调用其他组件时,采用由人工来编写的近似摘要这样的摘要能够 模拟被调模块中的常见数据流路径这种方式没有考虑到用户编写的代码对被调模块的影响Ali和 Hotan7,8 提出了一种对库建立轻量级的上近似摘要这种摘要的建立,需要代码库满足分离编译假设( separate compilation assumption),无需应用代码即可编译代码库Java代码库普遍满足这项假设.在该假设约束下的Java 标准库被简化为一个人工编写的占位库而这个占位库的文件仅有80KB大小,远小于Java标准库的原本大小 Ali和 Hotak:3的方法改造了现有的全程序调用图构造算法,以占位库作为所有库函数的替代品,所有应用代 与库函数代码间的调用关系被简化为应用代码与占位库间的调用关系该方法既提升了效率(10倍以上),又 保证了正确性,并且有足够的精确度 2)自动生成摘要 在程序分析过程前创建摘要,通常是对程序常用的模块(如Java代码库)进行摘要分析,随后加速客户代码 的分析诸多的未知信息和代码库太大造成算法难以扩展 cousot从理论上总结了创建模块摘要的各种方 式该工作首先分析了创建模块摘要的主要问题是处理模块间的环形依赖在没有环形依赖时,我们可以按照依 赖关系给模块排一个顺序,每个模块只依赖于之前的模块,然后按顺序依次分析但是,由于环形依赖的存在, 有环形依赖的模块就只能被当作一个模块分析使得创建模块的摘要无法进行.文献「80]针对环形依赖给出了3 种解决方案
张健 等:程序分析研究进展 85 用中. Reps 等人[67]后续进一步扩展了该框架,通过已有抽象域为环境而计算得到新的属性,用于过程间常数传播 等应用中,并形式化定义了上述图可达问题为上下文无关文法图可达问题.上下文无关文法图可达问题对图中 的边进行标号,图中任意两点可达需要两点间的一条路径上的标号串满足事先定义的上下文无关文法.多种不 同程序分析问题均可表示为对上下文无关文法图可达问题的求解.近年来,包括指针分析[68,69]、并行程序分 析[70,71]等多种分析技术均通过求解上下文无关文法图可达问题来有效地加以实现. 2) 基于值流图的稀疏数据流分析方法 传统的数据流分析在程序控制流图上将所需计算的状态信息在每个程序点传播得到最终分析结果.此过 程通常存在较多冗余操作,对效率,特别是过程间数据流分析效率会有很大影响.为了进一步提高数据流分析的 效率,近年来,研究者们提出了多种稀疏的分析方法,从而无需计算状态信息在每个程序点的传播即可得到与数 据流分析相同的结果.该类分析技术[7276]通过一个稀疏的值流图(value flow graph)直接表示程序变量的依赖关 系,从而使得状态信息可以有效地在该稀疏的值流图上传播.该值流图保证了状态信息可以有效地传播到其需 要使用该信息的程序点,并避免了在无效程序点的冗余传播,可大幅度提高效率. 2.3 基于摘要的过程间分析 摘要(summary)是可复用的程序模块分析结果,能够简要地刻画模块的外部行为.创建摘要和利用摘要开展 分析的过程称为摘要分析.在编写程序的过程中,一个程序模块往往需要调用其他程序模块.对主调(caller)模块 的分析必然涉及到对被调模块(callee)的分析.与复用被调模块代码可提高软件生产效率类似,摘要分析期望复 用被调模块的分析结果也能提高分析主调模块的效率.通过基于摘要的程序分析技术,我们将被复用模块的分 析结果被构造成为摘要,并在分析主调模块时对其实例化,以加快分析速度. 传统摘要分析的研究主要关注模块化(modular)分析,即:在分析过程中将软件划分为多个模块,对各个模块 分别分析和创建摘要,然后合并摘要获得整体的分析结果.这样,在分析过程中创建摘要的技术也称为在线摘要 技术.摘要分析在最近 10 年的主要进展是离线摘要技术,即:在程序分析之前对常用代码库生成摘要,从而加快 使用这些代码库的客户端的分析速度.离线摘要根据其自动化程度的不同,可以分成人工编写摘要和自动生成 摘要,分别在接下来的两小节中加以介绍. 1) 人工编写摘要 对于程序中一些难以分析的代码,例如第三方的库和系统代码等,可采用人工编写摘要的方式近似代码的 行为.这种技术原先应用于程序验证中,比如 ESC/Java 通过用户提供的前置条件和后置条件来对程序进行模块 化验证.FlowDroid[66]在处理调用系统代码和调用其他组件时,采用由人工来编写的近似摘要.这样的摘要能够 模拟被调模块中的常见数据流路径.这种方式没有考虑到用户编写的代码对被调模块的影响.Ali 和 Lhoták[77,78] 提出了一种对库建立轻量级的上近似摘要.这种摘要的建立,需要代码库满足分离编译假设(separate compilation assumption),无需应用代码即可编译代码库.Java 代码库普遍满足这项假设.在该假设约束下的 Java 标准库被简化为一个人工编写的占位库,而这个占位库的文件仅有 80KB 大小,远小于 Java 标准库的原本大小. Ali 和 Lhoták[77,78]的方法改造了现有的全程序调用图构造算法,以占位库作为所有库函数的替代品,所有应用代 码与库函数代码间的调用关系被简化为应用代码与占位库间的调用关系.该方法既提升了效率(10 倍以上),又 保证了正确性,并且有足够的精确度. 2) 自动生成摘要 在程序分析过程前创建摘要,通常是对程序常用的模块(如 Java 代码库)进行摘要分析,随后加速客户代码 的分析.诸多的未知信息[79]和代码库太大造成算法难以扩展.Cousot[80]从理论上总结了创建模块摘要的各种方 式.该工作首先分析了创建模块摘要的主要问题是处理模块间的环形依赖.在没有环形依赖时,我们可以按照依 赖关系给模块排一个顺序,每个模块只依赖于之前的模块,然后按顺序依次分析.但是,由于环形依赖的存在,所 有环形依赖的模块就只能被当作一个模块分析,使得创建模块的摘要无法进行.文献[80]针对环形依赖给出了 3 种解决方案
Journal of software软件学报Vol.30,No.1, January2019 ·基于简化的分析:这个方案的思路是针对环形依赖导致的大模块上的分析通过标准的编译技术(如 partial evaluation)进行化简提高分析速度每个模块上的分析程序可以被当成是一个函数,然后,把这 些函数看成是标准程序之后就可以应用普通的程序分析进行化简了; ·最坏情况分析:每个模块分别分析,对于该模块所依赖的其他模块作最坏情况假设.这样的分析会导致 不精确,并且在多数情况下严重不精确; ·符号化关系型分析:把未知的信息做成符号化信息,然后把程序分析转变成符号化分析所有与符号化 相关的部分不进行计算 Smaragdakis等人提出了针对所有流不敏感指针分析的代码库预处理技术,属于基于简化的分析该工作 发现:当代码中存在符合图代码模式时,将模式中的冗余语句删除,进而避免冗余运算,加速代码分析 Rountev和 yder2提出了另一种代码库的简化方式,对库的摘要就是把库里面所有的赋值语句提取出来这个摘要本身 只是省掉了语法分析的时间然后在摘要上进行了两个优化 a)对于连续赋值,比如a=b,c=a,去掉中间变量,替换成c=b b)去掉与客户端无关的赋值语句 这两个优化能省掉4%69%的时间该方法仅支持上下文不敏感且流不敏感的分析 Rountev等人3提出的构件级别分析( (component-level analysis)对代码库的IFDS/DE框架进行了摘要分 析该方法采用 Sharir和 Pnueli提出的函数型分析方法,为过程内的数据流和过程间的部分数据流建立了摘 要对于过程间边相关的未知量,即虚函数调用( virtual function)和回调点( callback site),该方法在计算过程中不 予考虑该方法只考虑了函数中的局部变量 tubEroid在 FlowDroid的基础上采用了构件级别分析对库进行 了自动分析,支持多层字段敏感性无需手动编写摘要 Tang等人提出了条件可达性解决了传统摘要无法描述的回调函数问题具体而言该工作考虑了过程 间的数据依赖分析当代码库存在回调函数时,部分信息缺失导致已有方法难以为代码库建立有效的摘要.为了 处理回调函数带来的影响该工作提出了基于树邻接语言的可达性的摘要分析技术注意到包含回调函数信息 的可达性关系(称为“条件可达性关系”)可用于加速用户代码的分析为描述条件可达性关系该工作引入了原 本用于描述自然语言语法的形式语言一一树-邻接语言提出了树邻接语言的可达性分析技术树邻接语言可 性扩展了表达两点间可达关系的传统上下文无关语言可达性,具有表达4个点之间的可达关系的能力,从 更自然地描述了上述条件可达性关系实验结果表明:建立基于树-邻接语言的可达性摘要可以在合理的时间内 完成该技术所建立的摘要可以使得对用户代码分析的效率平均提高约8倍在后续工作中,ang等人进一步 将该方法扩展到了 Dyck-CFL可达性分析上该方法通过直接在较为通用的CFL可达性分析过程中引入带 条件边,使得大量基于CFL可达性的分析就可以直接支持条件摘要同时,该方法引入桥接边来避免条件组合爆 炸的问题通过这些处理,该方法避免了原有的Dyck-CFL分析中摘要不完整和分析效率不高的问题实验结果 表明,其分析速度相比树-邻接语言进一步提升了3倍多 由于模块含有大量的未知量,建立考虑所有情况的摘要在许多分析任务中非常困难所以,一些工作通过动 态程序分析或训练的方式建立了部分摘要 Palepu等人例提出了加速程序分析速度的动态依赖摘要技术 ynamic dependence summary),提前创建软件库的摘要用来快速创建程序切片尽管得到的是不充分的摘要, 导致生成的程序切片并不保证完全正确,然而在程序测试的实践中能够找到大部分的错误 Kulkarni等人采 用跨程序的训练办法为代码库建立不完整的摘要,以提高客户代码的分析速度该方法基于 Datalog语言,有效 地对中间计算过程进行剪枝并将剪枝结果记录于摘要中同时该方法还对 Datalog语言进行改造,使得利用摘 要进行分析时可以跳过中间计算过程该方法保证正确性的方式是人工编写时间复杂度较低的规则判断训练 得到的摘要是否能够保证正确:如果不能保证正确性,则不采用摘要来进行计算 上述工作都是针对整个代码库进行摘要分析当精度要求较高时分析完整的代码库比较困难部分工作只 对单个函数进行分析 Yorsh等人提出的框架可以为函数建立精确而简练的函数摘要在不同上下文环境中 采用函数摘要与重新分析函数所得到的最终结果相同,从而保证精确性框架中采用有限显式输入输出表来表
86 Journal of Software 软件学报 Vol.30, No.1, January 2019 基于简化的分析:这个方案的思路是针对环形依赖导致的大模块上的分析通过标准的编译技术(如 partial evaluation)进行化简,提高分析速度.每个模块上的分析程序可以被当成是一个函数,然后,把这 些函数看成是标准程序之后就可以应用普通的程序分析进行化简了; 最坏情况分析:每个模块分别分析,对于该模块所依赖的其他模块作最坏情况假设.这样的分析会导致 不精确,并且在多数情况下严重不精确; 符号化关系型分析:把未知的信息做成符号化信息,然后把程序分析转变成符号化分析.所有与符号化 相关的部分不进行计算. Smaragdakis 等人[81]提出了针对所有流不敏感指针分析的代码库预处理技术,属于基于简化的分析.该工作 发现:当代码中存在符合图代码模式时,将模式中的冗余语句删除,进而避免冗余运算,加速代码分析.Rountev 和 Ryder[82]提出了另一种代码库的简化方式,对库的摘要就是把库里面所有的赋值语句提取出来.这个摘要本身 只是省掉了语法分析的时间.然后在摘要上进行了两个优化. a) 对于连续赋值,比如 a=b;c=a;去掉中间变量,替换成 c=b; b) 去掉与客户端无关的赋值语句. 这两个优化能省掉 4%~69%的时间.该方法仅支持上下文不敏感且流不敏感的分析. Rountev 等人[83,84]提出的构件级别分析(component-level analysis)对代码库的 IFDS/IDE 框架进行了摘要分 析.该方法采用 Sharir 和 Pnueli[85]提出的函数型分析方法,为过程内的数据流和过程间的部分数据流建立了摘 要.对于过程间边相关的未知量,即虚函数调用(virtual function)和回调点(callback site),该方法在计算过程中不 予考虑.该方法只考虑了函数中的局部变量.StubDroid[86]在 FlowDroid 的基础上采用了构件级别分析对库进行 了自动分析,支持多层字段敏感性,无需手动编写摘要. Tang 等人[87]提出了条件可达性,解决了传统摘要无法描述的回调函数问题.具体而言,该工作考虑了过程 间的数据依赖分析.当代码库存在回调函数时,部分信息缺失导致已有方法难以为代码库建立有效的摘要.为了 处理回调函数带来的影响,该工作提出了基于树-邻接语言的可达性的摘要分析技术.注意到包含回调函数信息 的可达性关系(称为“条件可达性关系”)可用于加速用户代码的分析.为描述条件可达性关系,该工作引入了原 本用于描述自然语言语法的形式语言——树-邻接语言,提出了树-邻接语言的可达性分析技术.树-邻接语言可 达性扩展了表达两点间可达关系的传统上下文无关语言可达性,具有表达 4 个点之间的可达关系的能力,从而 更自然地描述了上述条件可达性关系.实验结果表明:建立基于树-邻接语言的可达性摘要可以在合理的时间内 完成,该技术所建立的摘要可以使得对用户代码分析的效率平均提高约 8 倍.在后续工作中[88],Tang 等人进一步 将该方法扩展到了 Dyck-CFL 可达性分析上.该方法通过直接在较为通用的 CFL 可达性分析过程[67]中引入带 条件边,使得大量基于 CFL 可达性的分析就可以直接支持条件摘要.同时,该方法引入桥接边来避免条件组合爆 炸的问题.通过这些处理,该方法避免了原有的 Dyck-CFL 分析中摘要不完整和分析效率不高的问题.实验结果 表明,其分析速度相比树-邻接语言进一步提升了 3 倍多. 由于模块含有大量的未知量,建立考虑所有情况的摘要在许多分析任务中非常困难.所以,一些工作通过动 态程序分析或训练的方式建立了部分摘要.Palepu 等人[89]提出了加速程序分析速度的动态依赖摘要技术 (dynamic dependence summary),提前创建软件库的摘要,用来快速创建程序切片.尽管得到的是不充分的摘要, 导致生成的程序切片并不保证完全正确,然而在程序测试的实践中能够找到大部分的错误.Kulkarni 等人[90]采 用跨程序的训练办法为代码库建立不完整的摘要,以提高客户代码的分析速度.该方法基于 Datalog 语言,有效 地对中间计算过程进行剪枝,并将剪枝结果记录于摘要中.同时,该方法还对 Datalog 语言进行改造,使得利用摘 要进行分析时可以跳过中间计算过程.该方法保证正确性的方式是人工编写时间复杂度较低的规则,判断训练 得到的摘要是否能够保证正确:如果不能保证正确性,则不采用摘要来进行计算. 上述工作都是针对整个代码库进行摘要分析.当精度要求较高时,分析完整的代码库比较困难.部分工作只 对单个函数进行分析.Yorsh 等人[91]提出的框架可以为函数建立精确而简练的函数摘要.在不同上下文环境中, 采用函数摘要与重新分析函数所得到的最终结果相同,从而保证精确性.框架中采用有限显式输入输出表来表
张健等:程序分析研究进展 示摘要并通过摘要组合操作,使得不同上下文之下分析过程的相似之处得以合并为更加简练的形式,从而利用 有限的数据结构表达无限可能的函数行为该框架采用了微转换子,微转换子可以编码的问题包括 IFDS/IDE问 题该框架还可以解决模块的线性常量传播问题和模块的类型状态叼检验问题 Dlig等人的工作是针对C的上下文敏感、流敏感、不考虑字段的函数指向分析核心问题是分析一个 函数时如何考虑所有可能的调用上下文解决方案是将函数参数所有可能的别名关系编码到一个二部图上 边是参数另一边是符号化的位置,表示彼此不交的内存地址集合,中间连上带约束的边,编码了不同的别名关 系当遇到语句的转移函数时则采用图上再加一层的方法来保证流敏感性,这样可以做到强更新函数调用处理 方面需要计算出被调函数的别名情况,实例化主调函数的摘要,再把调用函数的图和被调函数实例化的图拼起 来通过不动点算法计算出一个上近似的结果. 24符号执行 符号执行明是一种相对精确的程序分析技术传统的符号执行技术使用符号化输入代替实际输入以模 拟执行(不实际执行)被分析程序程序中的操作被转化为相应的符号表达式操作在遇到条件语句时,程序的执 行也相应地分叉以探索每个分支,分支条件则被加入到当前路径的路径条件( path condition)中通过调用SAT/ SMT求解器对路径条件的可满足性进行求解来加以判断:如果判定结果为可满足,则说明路径实际可行(存在 具体输入能够让程序产生此路径)如果判定结果为不可满足,则表明此路径不可行,终止对该路径的分析 在约束条件可被判定的情况下,符号执行提供了一种系统遍历程序路径空间的手段符号执行中的程序路 径精确刻画了程序路径上的信息,可基于路径信息开展多种软件验证确认阶段的活动,包括自动测试、缺陷查 找以及部分的程序验证等理论上相比于需要固定程序输入的分析方法符号执行通过符号分析可覆盖更 多的程序行为另一方面符号执行技术依赖于 SAT/SMT技术,求解器的能力是决定符号执行效果的关键因素 符号执行中,程序路径空间大小随着程序规模的扩大而呈指数级增长例如:单就串行程序而言,一个具有n个条 件语句的程序段就有可能包含2”条路径这也是制约符号执行能力的关键因 最初符号执行主要用于程序自动测试但受制于当时的计算能力和求解技术与工具的能力,符号执行技术 并没有得到实际的应用近年来随着计算能力的提高、 SAT/SMT技术和工具的蓬勃发展-10,号执行技术 得到了长足的进步,出现了以动态符号执行( concolic testing0210为代表的一批新的符号执行方法或技术,以 及以SAGE0、KLEE0、SP10、Pex10、S2E108为代表的符号执行工具 不同于传统的符号执行,动态符号执行0210实际运行被分析的程序在实际运行的同时收集运行路径上 的路径条件然后翻转路径条件得到新的路径条件通过对新的路径条件进行求解得到新的程序输入以再一次 运行被分析程序,从而探索与之前运行不同的程序路径由于在实际运行程序过程中动态符号执行在碰到复 杂或不可解的路径条件时,可以使用实际值来简化路径条件在碰到外部调用时,也可以通过实际执行来缓解外 部调用的问题因此在方法层面动态符号执行通过牺牲部分分析的可靠性来提高方法的可扩展性和可行性 目前符号执行技术仍然面临提高可扩展性( scalability)与可行性( feasibility)这两方面的挑战可扩展性挑 战是指如何在有限资源(比如时间、内存)的前提下提高符号执行的效率,更快地达成分析目标;可行性挑战是指 如何支持不同类型分析目标的符号执行权衡分析的可靠性与精确性已有的研究工作基本都是围绕这两个方 面展开 在可扩展性方面路径空间爆炸和约束求解是主要的两大难题在缓解路径空间爆炸方面,目前己有的工作 基本分为两个思路:(1)在具体目标下提供高效的搜索策略,使符号执行分析更快地达到目标,包括提高程序的 覆盖率10.09-11判断某个程序点是否可达1产生满足正规性质的程序路径11、探索程序不同版本的差 异部分14等,(2)通过约束输入范围、削减或合并路径来减小程序的路径空间,包括基于输入模版61n、程 序切片1-1.程序抽象(包括摘要技术}219、偏序约减,3、条件合并13213以及等价路径约减121 等一些方法在约束求解方面已有的工作也可分为两个方面(1)在调用求解器之前对路径条件的查询进行优 化,以减少求解器的调用次数或缩短求解时间包括查询缓存和重用01319、基于约束独立性的优化10,10、 增量式求解10,14等(2)支持复杂程序特征的高效编码,包括对机器数100、数组00浮点1145、字符
张健 等:程序分析研究进展 87 示摘要,并通过摘要组合操作,使得不同上下文之下分析过程的相似之处得以合并为更加简练的形式,从而利用 有限的数据结构表达无限可能的函数行为.该框架采用了微转换子,微转换子可以编码的问题包括 IFDS/IDE 问 题.该框架还可以解决模块的线性常量传播问题和模块的类型状态[92]检验问题. Dillig 等人[93]的工作是针对 C 的上下文敏感、流敏感、不考虑字段的函数指向分析.核心问题是分析一个 函数时,如何考虑所有可能的调用上下文.解决方案是将函数参数所有可能的别名关系编码到一个二部图上,一 边是参数,另一边是符号化的位置,表示彼此不交的内存地址集合,中间连上带约束的边,编码了不同的别名关 系.当遇到语句的转移函数时则采用图上再加一层的方法来保证流敏感性,这样可以做到强更新.函数调用处理 方面,需要计算出被调函数的别名情况,实例化主调函数的摘要,再把调用函数的图和被调函数实例化的图拼起 来.通过不动点算法计算出一个上近似的结果. 2.4 符号执行 符号执行[9497]是一种相对精确的程序分析技术.传统的符号执行技术使用符号化输入代替实际输入以模 拟执行(不实际执行)被分析程序,程序中的操作被转化为相应的符号表达式操作.在遇到条件语句时,程序的执 行也相应地分叉以探索每个分支,分支条件则被加入到当前路径的路径条件(path condition)中.通过调用 SAT/ SMT 求解器,对路径条件的可满足性进行求解来加以判断:如果判定结果为可满足,则说明路径实际可行(存在 具体输入能够让程序产生此路径);如果判定结果为不可满足,则表明此路径不可行,终止对该路径的分析. 在约束条件可被判定的情况下,符号执行提供了一种系统遍历程序路径空间的手段.符号执行中的程序路 径精确刻画了程序路径上的信息,可基于路径信息开展多种软件验证确认阶段的活动,包括自动测试、缺陷查 找以及部分的程序验证等[98].理论上,相比于需要固定程序输入的分析方法,符号执行通过符号分析,可覆盖更 多的程序行为.另一方面,符号执行技术依赖于 SAT/SMT 技术,求解器的能力是决定符号执行效果的关键因素. 符号执行中,程序路径空间大小随着程序规模的扩大而呈指数级增长.例如:单就串行程序而言,一个具有 n 个条 件语句的程序段就有可能包含 2n 条路径,这也是制约符号执行能力的关键因素. 最初,符号执行主要用于程序自动测试,但受制于当时的计算能力和求解技术与工具的能力,符号执行技术 并没有得到实际的应用.近年来,随着计算能力的提高、SAT/SMT 技术和工具的蓬勃发展[99101],符号执行技术 得到了长足的进步,出现了以动态符号执行(concolic testing)[102,103]为代表的一批新的符号执行方法或技术,以 及以 SAGE[104]、KLEE[105]、SPF[106]、Pex[107]、S2E[108]为代表的符号执行工具. 不同于传统的符号执行,动态符号执行[102,103]实际运行被分析的程序,在实际运行的同时收集运行路径上 的路径条件,然后翻转路径条件得到新的路径条件,通过对新的路径条件进行求解得到新的程序输入以再一次 地运行被分析程序,从而探索与之前运行不同的程序路径.由于在实际运行程序过程中,动态符号执行在碰到复 杂或不可解的路径条件时,可以使用实际值来简化路径条件.在碰到外部调用时,也可以通过实际执行来缓解外 部调用的问题.因此,在方法层面,动态符号执行通过牺牲部分分析的可靠性来提高方法的可扩展性和可行性. 目前,符号执行技术仍然面临提高可扩展性(scalability)与可行性(feasibility)这两方面的挑战:可扩展性挑 战是指如何在有限资源(比如时间、内存)的前提下提高符号执行的效率,更快地达成分析目标;可行性挑战是指 如何支持不同类型分析目标的符号执行,权衡分析的可靠性与精确性.已有的研究工作基本都是围绕这两个方 面展开. 在可扩展性方面,路径空间爆炸和约束求解是主要的两大难题.在缓解路径空间爆炸方面,目前已有的工作 基本分为两个思路:(1) 在具体目标下提供高效的搜索策略,使符号执行分析更快地达到目标,包括提高程序的 覆盖率[105,109111]、判断某个程序点是否可达[112]、产生满足正规性质的程序路径[113]、探索程序不同版本的差 异部分[114,115]等;(2) 通过约束输入范围、削减或合并路径来减小程序的路径空间,包括基于输入模版[116,117]、程 序切片[118121]、程序抽象(包括摘要技术) [122129]、偏序约减[130,131]、条件合并[132,133]以及等价路径约减[121,134136] 等一些方法.在约束求解方面,已有的工作也可分为两个方面:(1) 在调用求解器之前对路径条件的查询进行优 化,以减少求解器的调用次数或缩短求解时间,包括查询缓存和重用[105,137139]、基于约束独立性的优化[103,105]、 增量式求解[105,140]等;(2) 支持复杂程序特征的高效编码,包括对机器数[104,105]、数组[100,105]、浮点[141145]、字符
Journal of software软件学报Vol.30,No.1, January2019 串4、动态数据结构14-14等方面的支持 在可行性方面环境建模和多形态分析目标的支持是目前的主要问题在环境建模方面,已有的工作基本都 是在分析的精确性、可靠性、建模工作量以及可扩展性之间进行权衡和折中,包括手工建模030、自动合 成1、动态执行1、全栈执行108等在多形态分析目标方面主要是应对多语言和多应用领域的复杂性包括 二进制程序10815.2、脚本语言程序、分布式程序、数据库操作程序15、无线传感器网络程序156、 并发或并行程序35158、嵌入式程序19、PLC程序1等符号执行方法 同时,面向新的分析需求,也有一些新的符号执行技术出现,其中比较有代表性的是概率符号执行技 术16-16,其基本思想是通过符号执行来得到程序的路径,然后使用SMT解空间体积计算技术来计算每条路径 的路径条件的解的个数,通过每条路径对应的解的个数,可以计算每条路径的概率基于此可以开展包括低概 率缺陷查找、低概率路径的测试用例生成、生成程序的性能分布6、刻画代码变迁16等活动 随着符号执行技术近些年的发展符号执行技术在工业界也得到了实际的采纳和应用,其中有代表性的工 作有微软公司把自己开发的二进制动态符号执行工具SAGE用于Win7的测试发现了文件模糊测试中1/3的 16由于SAGE通常是微软公司最后使用的缺陷检测工具,因此这些由SAGE发现的缺陷,很多都没有被 之前在开发过程中使用的静态分析工具、黑盒测试工具所发现微软公司多个开发小组已把SAGE作为日常 具在使用,SAGE目前也被商业化为微软公司的安全风险检测( microsoft security risk detection)服务微软公司在 Visual studio2015中正式发布了基于动态符号执行的C#自动单元测试工具 IntelliTestl6,可大幅度提高C#程 序单元的测试效率C程序符号执行工具KLEE0对 GnU Coreutils程序集进行了自动测试可自动达到94%的 语句覆盖率并发现3个程序崩溃问题 analyze6s在开源软件中发现数百个真实缺陷并在工业界嵌入式系统 中发现两个缺陷2016年8月,在美国 DARPA举办的网络空间安全竞赛(CGC中最终排名前三的参赛队伍全 部使用了符号执行技术,用于自动发现并利用二进制程序中的漏洞美国 GrammaTech公司开发的商业程序分 析工具 Codesonar中也使用了符号执行技术,用以发现程序中的深层缺陷 未来,符号执行技术将进一步在软件工程、安全、系统、网络等相关领域的实际需求驱动下不断发展面 向大规模软件的高效符号执行方法、技术和工具将是下一步研究所面临的挑战和重点同时符号执行搜索策 略的更加智能化1也将是下一步的研究重点此外,与其他技术在不同层面的密切结合1013,以进一步提高 件分析效果,也将成为符号执行后续的研究趋势之 2.5动态分析 动态分析是指通过在指定测试用例下运行给定的程序,并分析程序运行过程或结果用于缺陷检测等与静 态分析相比,动态分析能够更好地处理编程语言中的动态属性例如指针、动态绑定、面向对象语言中的多态 与继承、线程交替等动态分析在一定程度上弥补了静态分析的不足之处 基本的程序动态分析可以简单地分为在线 online)动态分析与离线( Offline)动态分析在线动态分析是指 在程序的运行过程中分析当前程序行为;而离线动态分析需要记录程序的运行行为在程序运行结束后再进行 分析两者的基本思想都是通过对程序运行过程或者结果的分析,查找定位缺陷.具体来说,一方面可以将程序 运行结果和预知结果对比确定程序中是否含有缺陷;另一方面,可以通过插桩或其他监控技术分析程序的运行 行为,查找错误的行为前者很直观但是对于被触发了却没有反映在输出中的缺陷无法检测后者则可以直 观察到程序中缺陷的触发,即使该次触发并没有导致错误的输出但是后者需要提前定义错误的行为,其对于非 常见的缺陷无法检测已有文献中有大量这方面的介绍174 程序动态分析,从报告缺陷的准确性出发也可以分为(1)缺陷动态检测、(2)缺陷动态预测.一般所指的缺 陷动态査找方法是缺陷动态检测,是指在程序的运行过程中某个缺陷已经发生了之后的检测,即,缺陷已经反映 在程序行为中或者运行结果中其关注点是:如何设计检测算法等保证将所有己经发生的缺陷检测出来然而 程序中的不同缺陷不会都在有限的若干测试用例中被触发因此,为了提高缺陷动态检测的有效性需要从程序 若干次运行中预测出该程序潜在的某些行为,并判断这些潜在行为是否会触发缺陷这种方法称为缺陷的动态 预测例如:某个程序中存在一个缓冲区溢出缺陷,该缺陷只有在输入 Input大于128时发生那么,如果我们可以
88 Journal of Software 软件学报 Vol.30, No.1, January 2019 串[146]、动态数据结构[147149]等方面的支持. 在可行性方面,环境建模和多形态分析目标的支持是目前的主要问题.在环境建模方面,已有的工作基本都 是在分析的精确性、可靠性、建模工作量以及可扩展性之间进行权衡和折中,包括手工建模[105,106]、自动合 成[150]、动态执行[102]、全栈执行[108]等.在多形态分析目标方面,主要是应对多语言和多应用领域的复杂性,包括 二进制程序[108,151,152]、脚本语言程序[153]、分布式程序[154]、数据库操作程序[155]、无线传感器网络程序[156]、 并发或并行程序[135,157,158]、嵌入式程序[159]、PLC 程序[160]等符号执行方法. 同时,面向新的分析需求,也有一些新的符号执行技术出现,其中比较有代表性的是概率符号执行技 术[161163],其基本思想是:通过符号执行来得到程序的路径,然后使用 SMT 解空间体积计算技术来计算每条路径 的路径条件的解的个数,通过每条路径对应的解的个数,可以计算每条路径的概率.基于此,可以开展包括低概 率缺陷查找、低概率路径的测试用例生成、生成程序的性能分布[164]、刻画代码变迁[165]等活动. 随着符号执行技术近些年的发展,符号执行技术在工业界也得到了实际的采纳和应用,其中有代表性的工 作有:微软公司把自己开发的二进制动态符号执行工具 SAGE 用于 Win 7 的测试,发现了文件模糊测试中 1/3 的 缺陷[166].由于 SAGE 通常是微软公司最后使用的缺陷检测工具,因此,这些由 SAGE 发现的缺陷,很多都没有被 之前在开发过程中使用的静态分析工具、黑盒测试工具所发现.微软公司多个开发小组已把 SAGE 作为日常工 具在使用,SAGE 目前也被商业化为微软公司的安全风险检测(microsoft security risk detection)服务.微软公司在 Visual Studio 2015 中正式发布了基于动态符号执行的 C#自动单元测试工具 IntelliTest[167],可大幅度提高 C#程 序单元的测试效率.C 程序符号执行工具 KLEE[105]对 GNU Coreutils 程序集进行了自动测试,可自动达到 94%的 语句覆盖率,并发现 3 个程序崩溃问题;Canalyze[168]在开源软件中发现数百个真实缺陷,并在工业界嵌入式系统 中发现两个缺陷.2016 年 8 月,在美国 DARPA 举办的网络空间安全竞赛(CGC)中,最终排名前三的参赛队伍全 部使用了符号执行技术,用于自动发现并利用二进制程序中的漏洞.美国 GrammaTech 公司开发的商业程序分 析工具 CodeSonar 中也使用了符号执行技术,用以发现程序中的深层缺陷. 未来,符号执行技术将进一步在软件工程、安全、系统、网络等相关领域的实际需求驱动下不断发展.面 向大规模软件的高效符号执行方法、技术和工具将是下一步研究所面临的挑战和重点.同时,符号执行搜索策 略的更加智能化[169]也将是下一步的研究重点.此外,与其他技术在不同层面的密切结合[170173],以进一步提高 软件分析效果,也将成为符号执行后续的研究趋势之一. 2.5 动态分析 动态分析是指通过在指定测试用例下运行给定的程序,并分析程序运行过程或结果,用于缺陷检测等.与静 态分析相比,动态分析能够更好地处理编程语言中的动态属性,例如指针、动态绑定、面向对象语言中的多态 与继承、线程交替等.动态分析在一定程度上弥补了静态分析的不足之处. 基本的程序动态分析可以简单地分为在线(online)动态分析与离线(offline)动态分析[1].在线动态分析是指 在程序的运行过程中分析当前程序行为;而离线动态分析需要记录程序的运行行为,在程序运行结束后再进行 分析.两者的基本思想都是通过对程序运行过程或者结果的分析,查找定位缺陷.具体来说,一方面可以将程序 运行结果和预知结果对比,确定程序中是否含有缺陷;另一方面,可以通过插桩或其他监控技术分析程序的运行 行为,查找错误的行为.前者很直观,但是对于被触发了却没有反映在输出中的缺陷无法检测;后者则可以直接 观察到程序中缺陷的触发,即使该次触发并没有导致错误的输出.但是后者需要提前定义错误的行为,其对于非 常见的缺陷无法检测.已有文献中有大量这方面的介绍[174]. 程序动态分析,从报告缺陷的准确性出发,也可以分为:(1) 缺陷动态检测;(2) 缺陷动态预测.一般所指的缺 陷动态查找方法是缺陷动态检测,是指在程序的运行过程中某个缺陷已经发生了之后的检测,即,缺陷已经反映 在程序行为中或者运行结果中.其关注点是:如何设计检测算法等,保证将所有已经发生的缺陷检测出来.然而, 程序中的不同缺陷不会都在有限的若干测试用例中被触发.因此,为了提高缺陷动态检测的有效性,需要从程序 若干次运行中预测出该程序潜在的某些行为,并判断这些潜在行为是否会触发缺陷.这种方法称为缺陷的动态 预测.例如:某个程序中存在一个缓冲区溢出缺陷,该缺陷只有在输入 input 大于 128 时发生.那么,如果我们可以
张健等:程序分析研究进展 从某个 Input不大于128的输入下预测对应行为是一个潜在缺陷,其可能会在 Input大于128时发生进一步地, 我们可以构造一个满足预测条件的输入,再次运行程序去触发(验证)缺陷缺陷的动态预测在并发程序的动态 分析中经常用到,主要原因之一是:并发程序的运行除了与输入有关外,还与程序中线程之间的调度有关程序 缺陷的动态预测还会涉及到一些其他技术,例如,测试用例生成、约束求解、缺陷重现、线程调度等,其分析过 程与缺陷动态检测相比更为复杂 2.6基于机器学习的程序分析 经典的程序分析技术提供相对精确的分析结果,但同时也带来了包括路径组合爆炸、误报率较高等一系列 在实践中不可避免却难以应对的问题随着近年来通用计算设备能力的提高,海量的程序执行数据被存储和管 研究者采用机器学习、统计分析等系列技术提升现有的程序分析能力 现有的程序分析技术依赖于一定的启发式策略,如符号执行技术中的深度(或广度)优先搜索在动态分析 技术中,为了达到分析精度,这些策略可能带来较高的计算成本基于现有的标记数据(即已知分析结果的程序) 建立学习模型,机器学习技术可以学习新的可自适应的策略,减少启发式策略带来的成本消耗Li等人4为了 解决符号执行中的路径可达性问题,以最小化不满足性为目标,建立机器学习模型MLB,以减少经典的约束求 解方案在求解非线性约束及函数调用时的不足Kong等人面向自动机验证,研究了多个随机测试与符号执 行技术的整合策略通过调整状态转移概率优化动态符号执行Wang等人12提出了基于马尔可夫过程的动态 符号执行方法,以达到应用符号执行获得精确分析结果和应用随机测试覆盖搜索空间的平衡该方法采用贪心 算法获得优化模型的解,以期找到对应于近似最优性能的策略Chen等人1针对信息物理系统( cyber-physical system)的攻防模型,设计了基于程序变异的方案获得具有植入错误的模型训练数据以避免人工建立模型的巨 大成本Xong等人1提出了基于概率程序合成框架L2S该框架整合了包括程序合成的搜索空间、路径和潜 在解的概率估计方案能够按需地构建程序合成和修复技术,研究者可基于该框架深度定制和设计相关方法 在静态分析技术中,分析工具在获得较高的分析精度的同时,往往带来过高的误报率研究者建立了机器学 习模型,以剔除潜在的误报并减少静态分析的成本Heo等人1提出了基于异常点检测技术来滤除静态分析结 果中的误报该方法提取代码循环和函数调用中的特征,基于训练数据建立学习模型,识别潜在的误报并提升静 态分析的实用性Chae等人针对上下文敏感的指针分析,提出了基于分类器的自动特征抽取方案该方案可 有效提升现有的静态分析技术Oh等人8针对静态分析的精度和计算成本提出了基于贝叶斯优化的自适 应学习方案,并以此建立面向数据流和上下文的部分静态分析工具 Jeong等人设计了数据驱动的上下文敏 感的指针分析方案该方案通过非线性的上下文选择建立了识别上下文敏感函数的学习方法 3面向特定软件的程序分析技术 本节介绍程序分析技术在一些重点领域软件的应用,包括移动应用软件、并发软件、分布式系统、二进制 代码等方面的重要应用 3.1移动应用软件 近10年来,以智能手机为代表的智能终端以惊人的速度得以普及目前,以 Android和苹果iOS系统为代表 的智能手机数量和使用频度已远超个人计算机成为最流行的个人电子设备通过移动支付、购物和社交等各 式各样的移动应用,智能手机已经深度渗透进了人们的日常活动中相应地这些应用的运行状态和广大用户的 日常生活和工作有着直接的关系,也在很大程度上影响到了整个互联网的运转为此研究人员通过对移动应用 软件的程序分析,来检测其是否具有所期望的以安全性为核心的各种特性 1)污点分析技术 H于智能手机的使用特点移动应用的安全性分析常常可以归结为应用代码上跟踪敏感数据流的动态/静 态污点分析( taint analysis问题 动态污点分析最具代表性的 Android应用动态污点分析技术是 Taint Droid82,其通过修改的 Dalvik
张健 等:程序分析研究进展 89 从某个 input 不大于 128 的输入下预测对应行为是一个潜在缺陷,其可能会在 input 大于 128 时发生.进一步地, 我们可以构造一个满足预测条件的输入,再次运行程序去触发(验证)缺陷.缺陷的动态预测在并发程序的动态 分析中经常用到,主要原因之一是:并发程序的运行除了与输入有关外,还与程序中线程之间的调度有关.程序 缺陷的动态预测还会涉及到一些其他技术,例如,测试用例生成、约束求解、缺陷重现、线程调度等,其分析过 程与缺陷动态检测相比更为复杂. 2.6 基于机器学习的程序分析 经典的程序分析技术提供相对精确的分析结果,但同时也带来了包括路径组合爆炸、误报率较高等一系列 在实践中不可避免却难以应对的问题.随着近年来通用计算设备能力的提高,海量的程序执行数据被存储和管 理;研究者采用机器学习、统计分析等系列技术提升现有的程序分析能力. 现有的程序分析技术依赖于一定的启发式策略,如符号执行技术中的深度(或广度)优先搜索.在动态分析 技术中,为了达到分析精度,这些策略可能带来较高的计算成本.基于现有的标记数据(即已知分析结果的程序) 建立学习模型,机器学习技术可以学习新的可自适应的策略,减少启发式策略带来的成本消耗.Li 等人[144]为了 解决符号执行中的路径可达性问题,以最小化不满足性为目标,建立机器学习模型 MLB,以减少经典的约束求 解方案在求解非线性约束及函数调用时的不足.Kong 等人[175]面向自动机验证,研究了多个随机测试与符号执 行技术的整合策略,通过调整状态转移概率优化动态符号执行.Wang 等人[172]提出了基于马尔可夫过程的动态 符号执行方法,以达到应用符号执行获得精确分析结果和应用随机测试覆盖搜索空间的平衡.该方法采用贪心 算法获得优化模型的解,以期找到对应于近似最优性能的策略.Chen 等人[176]针对信息物理系统(cyber-physical system)的攻防模型,设计了基于程序变异的方案,获得具有植入错误的模型训练数据以避免人工建立模型的巨 大成本.Xiong 等人[177]提出了基于概率程序合成框架 L2S.该框架整合了包括程序合成的搜索空间、路径和潜 在解的概率估计方案,能够按需地构建程序合成和修复技术,研究者可基于该框架深度定制和设计相关方法. 在静态分析技术中,分析工具在获得较高的分析精度的同时,往往带来过高的误报率.研究者建立了机器学 习模型,以剔除潜在的误报并减少静态分析的成本.Heo 等人[178]提出了基于异常点检测技术来滤除静态分析结 果中的误报.该方法提取代码循环和函数调用中的特征,基于训练数据建立学习模型,识别潜在的误报并提升静 态分析的实用性.Chae 等人[59]针对上下文敏感的指针分析,提出了基于分类器的自动特征抽取方案.该方案可 有效提升现有的静态分析技术.Oh 等人[179,180]针对静态分析的精度和计算成本,提出了基于贝叶斯优化的自适 应学习方案,并以此建立面向数据流和上下文的部分静态分析工具.Jeong 等人[181]设计了数据驱动的上下文敏 感的指针分析方案.该方案通过非线性的上下文选择,建立了识别上下文敏感函数的学习方法. 3 面向特定软件的程序分析技术 本节介绍程序分析技术在一些重点领域软件的应用,包括移动应用软件、并发软件、分布式系统、二进制 代码等方面的重要应用. 3.1 移动应用软件 近 10 年来,以智能手机为代表的智能终端以惊人的速度得以普及.目前,以 Android 和苹果 iOS 系统为代表 的智能手机数量和使用频度已远超个人计算机,成为最流行的个人电子设备.通过移动支付、购物和社交等各 式各样的移动应用,智能手机已经深度渗透进了人们的日常活动中.相应地,这些应用的运行状态和广大用户的 日常生活和工作有着直接的关系,也在很大程度上影响到了整个互联网的运转.为此,研究人员通过对移动应用 软件的程序分析,来检测其是否具有所期望的以安全性为核心的各种特性. 1) 污点分析技术 由于智能手机的使用特点,移动应用的安全性分析常常可以归结为应用代码上跟踪敏感数据流的动态/静 态污点分析(taint analysis)问题. 动态污点分析:最具代表性的 Android 应用动态污点分析技术是 TaintDroid[182],其通过修改的 Dalvik
