1、抽象解释及其应用研究进展陈立前1范广生1,3尹帮虎2王戟1,31（国防科技大学计算机学院长沙410073）2（国防科技大学系统工程学院长沙410073）3（高性能计算国家重点实验室（国防科技大学）长沙410073）（）Research Progress on Abstract Interpretation and Its ApplicationChenLiqian1,FanGuangsheng1,3,YinBanghu2,andWangJi1,31（College of Computer Science and Technology,National University of Defense
2、 Technology,Changsha 410073）2（College of Systems Engineering,National University of Defense Technology,Changsha 410073）3（State Key Laboratory of High Performance Computing(National University of Defense Technology),Changsha 410073）AbstractAbstractinterpretationisatheoryofabstractionandapproximationo
3、fthemathematicalstructuresusedintheformaldescriptionofcomplexsystemsandtheinferenceorverificationoftheirproperties.Sincebeingproposedin1970s,abstractinterpretationhasbeenwidelyappliedtomanyfields,includingsemanticmodels,programanalysisandverification,verificationofhybridsystems,programtransformation
4、,analysisofsystemsbiologymodels,etc.Inrecent years,abstract interpretation has made great progress in program analysis,neural network verification,completenessreasoning,improvementofabstractdomains,etc.Basedonthis,wesystematicallyreviewtheresearchprogressofabstractinterpretationanditsapplications.Fi
5、rstly,weoutlinethebasicconceptsofabstractinterpretationtheory,andreviewtherecentresearchprogressofabstractinterpretationtheoryandabstractdomains;then,wereviewthe recent research progress in abstract interpretation-based program analysis,verification and robust training ofneuralnetworks,analysisofdee
6、plearningprograms;afterthat,wealsoreviewtheprogressofsomeotherapplicationsofabstractinterpretation,includingtrustworthinessassuranceofsmartcontract,informationsecurity,andquantumcomputing;Atlast,potentialfuturedirectionsinthefieldofabstractinterpretationarepointedout.Key wordsabstractinterpretation；
7、programsemantics；programanalysis；formalverification；abstractdomain摘要抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论.抽象解释自 20 世纪 70 年代提出以来，在语义模型、程序分析验证、混成系统验证、程序转换、系统生物学模型分析等领域取得了广泛应用.近年来，抽象解释在程序分析、神经网络验证、完备性推理、抽象域改进等方面取得较大进展.基于此，系统综述了抽象解释及其应用的研究进展.首先概述了抽象解释理论的基本概念，介绍了抽象解释理论、抽象域的研究进展；然后概述了基于抽象解释的程序分析方面的
8、研究进展;之后概述了基于抽象解释的神经网络模型验证、神经网络模型鲁棒训练、深度学习程序的分析等方面的研究进展；又对抽象解释在智能合约可信保证、信息安全保证、量子计算可信保证等方面的应用收稿日期：20221107；修回日期：20221225基金项目：国家重点研发计划项目(2022YFA1005101)；国家自然科学基金项目(61872445,62032024,62102432)；湖南省自然科学基金项目(2021JJ40697)ThisworkwassupportedbytheNationalKeyResearchandDevelopmentProgramofChina(2022YFA100510
9、1),theNationalNaturalScienceFoundationofChina(61872445,62032024,62102432),andtheNaturalScienceFoundationofHunanProvince(2021JJ40697).通信作者：尹帮虎()计 算 机 研 究 与 发 展DOI：10.7544/issn1000-1239.202220925JournalofComputerResearchandDevelopment60（2）：227247，2023进展进行了介绍；最后指明了抽象解释未来可能的研究方向.关键词抽象解释；程序语义；程序分析；形式验证；抽
10、象域中图法分类号TP391抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论，由 PatrickCousot1-2和 RadhiaCousot1于 20 世纪 70 年代提出.抽象解释提供了一个通用的理论框架，使得人们能够在该框架下讨论不同形式化方法各自能提供的理论保证，如可靠性、完备性、不完备性等.例如，基于抽象解释，人们能够解释调试、演绎证明、模型检验、静态分析等方法的优势和局限性.目前，抽象解释在语义模型、不变式生成、程序分析验证、混成系统验证、程序转换、系统生物学模型分析等领域取得了广泛应用.在抽象解释的发展过程中，除了理论本身的发展完善，也涌现出
11、了一批优秀的抽象解释工具.20 世纪 90 年代，研究人员开发了基于抽象解释的静态分析工具 Polyspace，并成功商业化3.2003 年左右，Blanchet 等人4基于抽象解释开发了静态分析工具 Astre4，并商业化5，它主要用于检测 C 语言编写的运算密集型安全攸关嵌入式实时软件系统中运行时的错误（包括算术溢出、除零错、数组越界等），并成功对空客 A340（约 13.2万行C代码）、A380（约 35万行 C代码）等系列飞机的飞行控制软件进行了分析，实现了“零误报”，这是当时验证工具在验证规模上的重大突破.2015 年，Min等人6进一步开发了面向多线程并发程序的静态分析工具 Ast
12、reA，它作为 Astre 的并发版本，已实际应用于空客飞行系统软件，所分析程序的最大规模达百万行.近年来，抽象解释在理论与应用方面都取得了进一步发展.本文重点介绍最近 5 年抽象解释在理论、基于抽象解释的程序分析、基于抽象解释的可信人工智能和其他典型应用等方面的进展，并讨论抽象解释领域未来的发展方向.1抽象解释理论本节主要介绍抽象解释的基本概念、理论及抽象域方面的进展.1.1基本概念抽象解释为建立具体空间与抽象空间之间的联系提供了形式化的理论方法.我们将具体空间中推理对象的集合及其上的操作所构成的数学结构称为“具体域”，而将抽象空间推理对象的集合及其上的操作所构成的数学结构称为“抽象域”.抽
13、象解释理论利用 Galois 连接来形式化地描述具体域与抽象域之间的关系.对于给定的 2 个偏序集和，其中称为具体域，称为抽象域，函数:DD#与函数:D#D 构成的函数对(，)称为 D 与 D#之 间 的 Galois 连 接，当 且 仅 当x D，x#D#，(x)#x#x(x#)，称为抽象化函数，称为具体化函数.对于具体域 D 中的元素 x 和抽象域 D#中的元素 x#，若(x)#x#(亦即 x(x#)，则称 x#是 x的可靠抽象（也称上近似抽象）；对于具体域 D 上的函数 f 和抽象域 D#上的函数 f#，若 x#D#，(f)(x#)(f#)(x#)，则称 f#是 f的可靠抽象.抽象解释通
14、过在抽象域上计算抽象函数的不动点来获得抽象语义，并基于此进行推理.抽象解释提供了严格的理论来保证基于上近似抽象的推理的可靠性，即所有基于上近似抽象推理得出的抽象空间中的性质在具体空间中也必然成立.但是，由于上近似抽象引入了精度损失，抽象解释不保证所有在具体空间中成立的性质都能基于上近似抽象推理得到.1.2理论进展在理论框架方面，Cousot 等人7提出了一种称为 A2I（abstract2interpretation），也称元抽象解释的技术，它用于对基于抽象解释的程序分析作进一步的抽象解释，即应用抽象解释对程序分析工具的性质开展分析.A2I 既可离线应用也可在线应用.离线 A2I既可在分析程序
15、之前开展（如变量打包技术），也可在分析程序之后开展（如警告诊断）；在线 A2I 则既可在分析程序过程中开展（如面向数值抽象域的动态变量划分技术），也可用于优化底层程序分析的精度和效率，如应用 A2I，可以在原有程序分析基础上构建更加高效、更加精确的程序分析算法.换言之，A2I提供了一种通用的方法，使得不仅能应用抽象解释分析程序的性质还能应用抽象解释分析程序分析工具的性质.Bruni 等人8在抽象解释框架下提出了局部完备性（localcompleteness）概念，它只考虑特定的而非所有的输入，并定义了一种支持局部完备抽象解释推228计算机研究与发展2023，60（2）理的逻辑 LCLA，通过结
16、合上近似和下近似，可支持某些程序规约的正确性（程序不存在错误）和不正确性(程序存在错误)证明.该逻辑 LCLA通过APcQ 来表示，断言 Q 是 postc(P)的最强后置条件的下近似，且 使得 Q 在 抽 象 域 A 上 的 抽 象 和 postc(P)一 致.APcQ不仅保证了 Q 中的所有报警都是正报，还保证了若 Q 中没有报警则 c 是正确的.因为 LCLA逻辑对于非局部完备抽象域不适用，需要修复这些抽象域以满足局部完备性.为此，Bruni 等人9进一步提出了一种称为抽象解释修复（abstractinterpretationrepair）的方法，展示了如何利用局部完备性的概念以一种最优的方式来精化抽象域，以增强程序验证的精度.应用这种方法，并不要求在分析之前选择合适的抽象域，而是可以从任意抽象域开始，对其需达到的局部完备性逐步进行修复.抽象解释修复技术之于抽象解释，类似于反例制导抽象精化技术之于抽象模型检验.该工作给出了最优局部完备精化存在的充要条件.基于此，提出了 2 种修复策略，使得能够在一个给定的抽象计算上消除所有的误报：一种策略是随着具体计算进行前向修复；另一种是在抽象
