程序分析库DG：静态分析工具及软件影响研究

原始软件出版物DG：一个程序分析库马雷克·查卢帕捷克布尔诺马萨里克大学软件影响6（2020）100038A R T I C L E I N F O关键词：程序分析指向分析依赖分析依赖图程序切片A B标准DG是一个C++库，提供用于构建程序分析工具的元素。它的主要组成部分是一个点-要分析，有数据依赖性分析、控制依赖性分析和变量间关系分析。DG还包含一组用于显示和导出分析结果的工具以及LLVM位代码的程序切片器。它已成功地应用于多个研究项目。代码元数据当前代码版本v0.9.1用于此代码版本的代码/存储库的永久链接https://github.com/SoftwareImpacts/SIMPAC-2020-44可复制胶囊法律代码许可证MIT使用git的代码版本控制系统使用C++、Python的软件代码语言、工具和服务编译要求、操作环境依赖性python、C++编译器、LLVM 3.4或更新版本、cmake如果可用，链接到开发人员文档/手册https://github.com/mchalupa/dg/blob/master/doc/README.md问题支持电子邮件chalupa@fi.muni.cz1. 关于DG图书馆程序分析是一个广泛的研究领域，涉及自动导出计算机程序的属性，如变量的可能运行时值或程序中的断言是否可能失败。静态程序分析努力在不实际执行程序的情况下导出这些属性，这是非常有用的，例如，在早期开发阶段，当没有可执行的程序形式可用时。我们对静态程序分析领域的贡献是库DG包含几个基本程序分析和数据结构的实现，可以进一步由更复杂的工具使用分析是独立于输入编程语言进行内部编程的，但我们为所有分析提供了LLVM1前端，以便它们可以很容易地被外部工具使用此外，库本身包含几个工具，使用分析来分析LLVM位代码。这些工具之一是静态程序切片器[3]，也就是说，一种可以从程序中删除指令的工具，这些指令不会对程序的特定（用户指定的）行为产生任何影响电子邮件地址：chalupa@fi.muni.cz。2. 关键特征DG中实现的主要分析和数据结构如图1所示。在下文中，我们简要介绍它们及其相互作用。指向分析是程序分析的基石之一[4]。指向分析回答了“给定的指针可以引用哪些内存区域？”指向分析的结果可以用于广泛的领域，例如程序优化，错误检测或软件安全性[5在DG内部，我们使用指向分析来创建数据依赖分析的输入，并且我们可以在控制依赖分析和调用图构造中可选地使用它。Call-graph捕获关于给定函数可以调用哪些函数的信息[11]。如果被分析的程序包含通过函数指针的调用，则必须使用指向分析来解析函数指针调用的目标。1LLVM [1，2]是一种流行的类汇编程序表示，专为编译器构造而设计。它拥有强大的开发者社区支持。https://doi.org/10.1016/j.simpa.2020.100038接收日期：2020年10月9日;接收日期：2020年10月27日;接受日期：2020年10月30日2665-9638/©2020作者。由Elsevier B.V.出版。这是一篇开放获取的文章，使用CC BY许可证（http://creativecommons.org/licenses/by/4.0/）。可在ScienceDirect上获得目录列表软件影响杂志 首页：www.journals.elsevier.com/software-impactsM. Chalupa软件影响6（2020）1000382Fig. 1. DG库的结构。库模块之间的黑色箭头表示源模块被目标模块使用。如果箭头是虚线，则使用是可选的。紫色箭头表示该工具正在使用该模块数据依赖分析，也称为值流分析[12]，回答了这样一个问题������：“给定一条从内存中读取的指令，哪些指令可能写入了正在读取的值？”.数据依赖分析可以用来优化和并行化代码或加速其他程序分析[13对于使用指针的程序，需要进行指向分析来解析指令读取和写入的内存。控制依赖分析[14，19，20]为程序中的每个条件跳转计算一组可能由于该跳转而无法执行的指令。更准确地说，它回答了���“给定一条指令，可能导致不执行的最接近的条件跳转是什么？���”.如果用户还想计算来自不同函数的指令之间的依赖图[14，21]是有向图，其具有作为节点的指令，并且如果一个指令是（控制或数据）依赖于另一个。依赖图具有多种用途，例如，程序优化和并行化，或测试生成[14，22，23]。然而，主要用途之一是程序切片，即从程序中删除不影响指定行为的指令。在DG中，程序切片在工具llvm-slicer中实现。DG中的价值关系分析是计算关系（例如，（>0，=，等等）变量（分别为变量和常量）之间的关系，这些关系必须在程序的任何执行中保持。该分析可以用于例如，对指针执行简单的越界检查或执行常量传播。在DG中，我们可以使用此分析来细化指向分析的结果DG中的分析都是过程间的，2也就是说，分析计算整个程序的结果，而不是单独的函数。数据和控制依赖性分析也可以按需工作- 他们不会一次计算全部信息，而是计算它。按用户请求的部件数计算。DG中的每个分析都是一个独立的模块，包括分析本身的独立于语言的实现，以及2默认情况下，控件依赖性分析是过程内的。但是，有一个开关可以改变这种行为。从给定程序中创建分析输入的适配器在一个特定的编程语言和映射的分析结果回到输入程序。此时，我们有LLVM位代码的适配器。每个模块都提供了一个公共API来指定输入和处理结果。这使得DG可以通过编写一个适配器轻松集成外部分析，该适配器将外部分析的输入和输出转换为DG API。此时此刻，我们已经整合了来自SVF项目的指向分析[12]3. 限制DG的目标是从C编程语言生成的LLVM位代码中的程序。其他LLVM位代码，例如，由C++生成或者Rust，可能会有问题，因为它可能包含异常处理等功能，目前还不支持（但是，如果程序中没有这些功能，DG应该能够分析它）。此外，我们对并行程序的分析只有有限的支持。目前的另一个限制是我们的点到分析的可扩展性。然而，在我们开发出更好的指向点分析之前，这可以通过使用到SVF框架的绑定来克服（参见 上一节）。4. 影响概述DG最初是为了取代工具Symbiotic [24，25]中的程序切片器而创建的，Symbiotic是一种用于顺序C程序的错误查找工具，使用程序切片来减少输入程序。发生时DG的创建，没有其他合适的切片器用于LLVM位代码，Symbiotic中的切片器是不够的。 基于DG的程序切片器使Symbiotic能够用于研究[26 在行业[29]和竞争[30在所有这些场景中，Symbiotic使用DG来执行程序切片，以获得可能更小的输入程序，保留正在寻找的指定类型的错误。除了Symbiotic之外，DG还被用于Chopper [34]，另一个bug查找工具。与Symbiotic类似，Chopper使用DG来分割程序中只会阻碍其实现目标但对结果没有影响的部分。在这种情况下，程序切片是M. Chalupa软件影响6（2020）1000383用于减少函数内部需要探索的路径数量，以便找到与给定上下文兼容的路径最后，DG已被用于确定LLVM位代码的指令之间的依赖关系，在其他几个领域不同的程序验证和错误发现。这些领域包括网络安全[35-竞合利益作者声明，他们没有已知的竞争性财务利益或个人关系，可能会影响本文报告的工作致谢非 常 感 谢 DG 库 的 其 他 贡 献 者 ， 主 要 是 TomáJašek ， AnnaJechtáčková，LukáTomoviá，Martina Vitovská和LukáZaoral。这项工作得到了捷克科学基金会资助GA 18 - 02177 S的支持。引用[1]C. 拉 特 纳 ， V.S. Adve ， LLVM ： A compilation framework for lifetimeprogramanalysis& transformation ， in ： Proceedings of the 2nd IEEE / ACMInternationalSymposium on Code Generation and Optimization （ CGO '04 ） ，IEEE Computer Society，2004，pp. 75比88[2]LLVM项目网页。 网址https://llvm.org。[3]M. Weiser，Program slicing，IEEE Trans.软件。Eng. 10（4）（1984）352[4]O. Lhotak，Y. Smaragdakis，M. Sridharan，Pointer analysis（dagstuhl seminar13162），Dagstuhl Rep.3（4）（2013）91 http://dx.doi.org/10.4230/DagRep.3.4.91，URLhttp://drops.dagstuhl.de/opus/volltexte/2013/4169。[5]M. Hind， A. Pioli， 我应 该使 用哪 种 指针 分析 ？参 见 ：D.J. Richardson， M.J.Harold（编辑），软件测试与分析国际研讨会论文集，ISSTA 2000，美国俄勒冈州 波 特 兰 ， 2000 年 8 月 21-24 日 ， ACM ， 2000 年 ，pp.113http://dx.doi.org/10.1145/347324.348916[6]D. Avots，M.道尔顿，V.B. Livshits，M.S. Lam，用C指针分析提高软件安全性，在：G。罗曼，W.G.格里斯沃尔德湾Nuseibeh（Eds.），第27届软件工程国际会议（ICSE 2005），2005年5月15-21日332http://dx.doi.org/10.1145/[7]S.Z.盖耶角Lin，Client Driven Pointer Analysis，in：R. Cousot（Ed.），静态分析，第10届国际研讨会，SAS 2003年，圣地亚哥，CA，美国，2003年6月11-13日 ， 会 议 录 ， 在 ： 计 算 机 科 学 讲 义 ， 第 2694卷 ， Springer ， 2003年 ， pp.214http://dx.doi.org/10.1007/3-540-44898-5_12[8]S.Z.盖耶角林，错误检查与客户端驱动的指针分析，科学。Comput.程序. 58（1http://dx.doi.org/10.1016/j.scico。2005年2月5日[9]C.L. Conway，D. Dams，K.S.南条，C.W. Barrett，指针分析，条件可靠性，以及证明不存在错误，在：M。阿尔蓬特湾Vidal（Eds.），静态分析，第15届国际研讨会，SAS 2008，瓦伦西亚，西班牙，2008年7月16-18日。Proceedings，in：Lecture Notes in Computer Science ， vol. 5079 ， Springer ， 2008 ， pp.62http://dx.doi.org/10.1007/978-3-540-69166-2_5[10] C.拉特纳，V.S. Adve，自动池分配：通过控制堆中的数据结构布局来提高性能，V.Sarkar，M.W. Hall（Eds.），Proceedings of the ACM SIGPLAN 2005 Conferenceon Programming Language Design and Implementation ， Chicago ， IL， USA，June 12-15，ACM，2005，pp. 129http://dx.doi.org/10.1145/1065010.1065027[11] A. Milanova ， A. Rountev ， B.G. Ryder ， Precise call graph construction in thepresence of function points，第二届IEEE源代码分析和操作国际研讨会（SCAM2002），2002年10月1日，加拿大蒙特利尔，IEEE计算机协会，2002年，第100页。155http://dx.doi.org/10.1109/[12] Y. Sui，J.Xue，SVF：LLVM中的过程间静态值流分析，在：A. Zaks，M.V. Hermenegildo（编辑），2016年3月12日至18日在西班牙巴塞罗那举行的第25届建筑施工国际会议论文集，CC 2016，ACM， 2016年，pp.265http://dx.doi.org/10.1145/2892208.2892235[13] M.G.伯克河Cytron，程序间依赖性分析和并行化（回顾性），在：K.S. McKinley（Ed.），20 Years of the ACM SIGPLAN Conference on Programming LanguageDesign and Implementation 1979-1999 ， A Selection ， ACM ， 1986 ， pp.139http://dx.doi.org/10.1145/989393.989411[14] J.Ferrante，K.J. Ottero，J.D. Warren，程序依赖图及其在优化中的应用，ACM Trans. 程序. 浪系统9（3）（1987）319[15] P. Petersen ， D.A. Padua ， 数 据 依 赖 分 析 技 术 的 静 态 和 动 态 评 估 ， IEEETrans.ParallelDistrib。7（11）（1996）1121http://dx.doi.org/10.1109/71.544354[16] T.B. 托 克 ， S.Z. 盖 耶 角 Lin ， Efficient flow-sensitive interprocedural data-flowanalysis in the presence of points，in：A. Mycroft，A. Zeller（Eds.），2006年3月30日至31日在奥地利维也纳举行的第15届国际软件工程会议，作为欧洲软件理论与实践联合会议的一部分，2006年3月30日至31日，会议记录，在：计算机科学讲义中第3923卷，Springer，2006年，第3923页。17http://dx.doi.org/10.1007/11688839_3[17] R. Castillo，F. Corbera，A.G.纳瓦罗河Asenjo，E.L.在动态数据结构的递归程序中的完全定义使用分析，在：E。塞萨尔湾亚历山大，A. Streit，J.L.特拉夫角Cérin，A. Knüpfer，D. Kranzlmüller，S. Jha（Eds.），Euro-Par 2008研讨会-并行 处 理 ， VHPC 2008 ， UNICORE 2008 ， HPPC 2008 ， SGS 2008 ， PROPER2008，ROIA 2008和DPA 2008，Las Palmas de Gran Canaria，西班牙，2008年8月25-26日，修订的论文集，收录于：计算机科学讲义，第5415卷，Springer出版 社 ， 2008 年 ， 第 100 页 。 273http://dx.doi.org/10.1007/978-3-642-00955-6_32[18] H. Wang，T. Liu，X.关角，澳-地申角，澳-地 Zheng，Z. 杨，依赖性引导的符号执行，IEEE Trans.Softw.2000。工程43（3）（2017）252//dx.doi.org/10.1109/TSE.2016.2584063网站。[19] V.P. Ranganath，T. Amtoft，A. Banerjee，J.Hatcliff，M.B. 陈晓，控制依赖与切片的 新 基 础 ， 计 算 机 工 程 学 报 ， 2001 。 29 （ 5 ） （ 2007 ） 27 ，http://dx.doi.org/10.1145/1275497.1275502。[20] S. Danicic，R.W. Barraclough，M. Harman，J.Howroyd，J.吻你，M.R.控制依赖的统一理论及其在任意程序结构中的应用。 Comput. Sci. 412（49）（2011）6809http://dx.doi.org/10.1016/j.tcs.2011.08.033。[21] S. Horwitz ， T.W. 代 表 ， D.W. Binkley ， Interprocedural slicing usingdependencegraphs，ACM Trans. 程序. 浪系统12（1）（1990）26[22] E.F. 纳朱穆丹河 Mall，D. Samanta，一个基于依赖图的表示，面 向 对 象 程 序 的 测 试 覆 盖 率 分 析 方 法 。 Eng. Notes 34 （ 2 ） （ 2009 ）1http://dx.doi.org/10.1145/1507195.1507208[23] K. Hotta，Y. Higo，S. Kusumoto，识别，裁剪和建议表单模板方法重构机会与程序依赖图，在：T. Mens，A.克利夫河Ferenc（Eds.），第16届欧洲软件维护和再工程会议，CSMR 2012，匈牙利塞格德，2012年3月27-30日，IEEE计算机协会，2012年，第10页。53http://dx.doi.org/10.1109/CSMR.2012.16。[24] M.查卢帕湾作者声明：J.Vitovská，共生3：新的切片器和错误见证生成-（竞争贡献），在：M。J.Raskin（Eds.），系统构造与分析的工具与算法- 第22届国际会议，TACAS 2016，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2016，荷兰埃因霍温，2016年4月2日至8日，会议记录，在：计算机科 学 讲 义 ， 第 9636 卷 ， 施 普 林 格 ， 2016 年 ， 第 100 页 。946http://dx.doi.org/10.1007/978-3-662-49674-9_67。[25] M. Chalupa，LLVM Bitcode的切片（硕士https://is.muni.cz/th/vik1f/[26] M. Chalupa ， J.Strejcek， M. Vitovská ， 内 存 安 全 检 查 的 联 合 力 量 ， in ： M.Gallardo ， P. Merino （ Eds. ） ， Model Checking Software - 25th InternationalSymposium，SPIN 2018，Malaga，Spain，June 20-22，2018，Proceedings，in：Lecture Notes in Computer Science，vol.10869，Springer，2018，pp.115-132，http://dx.doi.org/10.1007/978-3-319-94111-0_7网站。[27] M. Chalupa，J. Strejček，软件验证中程序切片的评估，在：W. Ahrendt ， S.L.T. Tarifa （ Eds. ） ， IFM'19 ， 在 ： 计 算 机 科 学 讲 义 ， 卷 。11918，施普林格，2019年，pp. 101-http://dx.doi.org/10.1007/978-3-030-[28] M. Chalupa，J.Strejček，M. Vitovská，重新审视内存安全检查的联合力量，Int.J. Softw。工具技术转让22（2）（2020）115//dx.doi.org/10.1007/s10009-019-00526-2网站。[29] 红帽研究-AUFOVER项目，2020年，URLhttps://research.redhat.com/blog/research_project/aufover-2/。[30] M. 查 卢 帕 湾 Vitovská ， M. Jonás ， J.Slaby ， J.Strejcek ， Symbiotic 4 ： Beyondreachability - （ competition contribution ） ， in ： A. Legay ， T. Margaria（Eds.），系统构建和分析的工具和算法-第23届国际会议，TACAS 2017，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2017，乌普萨拉，瑞典，2017年4月22日至29日，会议记录，第二部分，在：计算机科学讲义，卷。10206，2017年，页 385http://dx.doi.org/10.1007/978-3-662-54580-5_28[31] M.查卢帕湾Vitovská，J. Strejček，共生5：助推仪器（竞争贡献），在：D.拜尔，M。Huisman（Eds.），第24届国际会议的工具和算法的建设和分析系统（TACAS'18），在：在计算机科学讲义，卷。10806，Springer，2018，pp.442-446M. Chalupa软件影响6（2020）1000384[32] M. 查 卢 帕 湾 Vitovská ， T. Jašek ， M.Šimácek ， J.Strejcek ， SYMBIOTIC 6 ：Generating test cases by slicing and symbolic execution，Int.J. Softw.工具技术转让（2020）http://dx.doi.org/10.1007/s10009-020-00573-0。[33] M. Chalupa，T. 亚谢克湖 Tomovietum，M. Hruška，V. Šoková，P. Ayaziová，J.Strejek，T. Vojnar，共生7：捕食者和更多的整合（竞争贡献），在：A。Biere，D. Parker（编辑），第26届系统构建和分析工具和算法国际会议论文集（TACAS 413http://dx.doi.org/10.1007/978-3-030-45237-7_31[34] D. Trabish ， A. Mattavelli ， N. 里 内 茨 基 角 Cadar ， Chopped SymbolicExecution，in：M. 肖 德 龙 岛 Crnkovic ， M.M.E.Harman （ Eds. ） ，ICSE350http://dx.doi.org/10.1145/3180155.3180251[35] M. Ahmadvand，A. Hayrapetyan，S. Banescu，A. Pretschner，使用不经意散列的实用完整性保护，在：ACSAC40//dx.doi.org/10.1145/3274694.3274732网站。[36] L. Cheng ， Program Anomaly Detection Against Data-Oriented Attacks （ Ph.d.thesis），VirginiaTech，2018，URLhttps://vtechworks.lib.vt.edu/handle/10919/84937.[37] H. Hamadeh，A. Almomani，A. Tyagi，基于新型可逆PUF的外包计算的概率验证 ， 在 ： A. Brogi ， W. Zimmermann ， K. Kritikos （ Eds. ） ， ESOCC30http://dx.doi.org/10.1007/978-3-030-44769-4_3[38] Z. Li，D. Zou，S. Xu，Z. Chen，Y. Zhu，H. Jin，VulDeeVulnerability：基于深度 学 习 的 细 粒 度 漏 洞 检 测 器 ， 2020 ， CoRRabs/2001.02350 。 arXiv ：2001.02350。网址http://arxiv.org/abs/2001.02350。[39] L. Cheng，K.田博士Yao，Orpheus：Enforcing cyber-physical execution semanticstodefendagainstdata-orientedattacks，in：ACSAC315http://dx.doi.org/10.1145/3134600.3134640[40] L. Cheng，K. Tian，中国粘蝇D.尧湖，澳-地Sha，R.A. Beyah， Checking isbelieving：Event- aware program anomaly detection in cyber-physical systems，2018，CoRRabs/1805.00074。arXiv：1805.00074。[41] B.邓，W。 吴湖，加-地 宋，网络功能中的冗余逻辑消除，在：A。Wang，中国山 核 桃 E. Rozner ， H. Zeng （ Eds. ） ， SOSR'20 ， ACM ， 2020 ， pp.34http://dx.doi.org/10.1145/3373360.3380832