软件学报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]在内的多种应