2015年雷恩第一大学由布列塔尼欧洲大学盖章为的等级雷恩第一大学博士提及：信息学马蒂斯博士学院提交人：文森特·拉波特联合研究单位6074 - IRISA计算机科学和随机系统研究所UFR计算机科学电子学对低级语言的静态分析的改进这是由M.约翰·格雷戈里·莫里塞特康奈尔大学教授/报告员M.安德斯·默勒教授-奥胡斯大学/报告员并于2015年11月25日在雷恩获得陪审团由以下人员组成：M.安德斯·默勒Professeur-AarhusUniversity/r贡献者M.泽维尔·勒罗伊研究负责人-INRIARocquencourt/检查员M.安托万·明大学教师专业-ParisvI/考官玛丽-洛尔·波特大学教师专业-NSIMAG/考官桑德琳·布拉齐因此，它们是统一的，而不是统一的，而不是统一的。来自雷恩1号/特海塞导演M.大卫·皮查迪Professeurdesuniversitěs-NSRennes/thěse的联合导演i内容物英语中的Rěsuměěskuvii1程序的静态验证vii2低级语言分析IX3我们能信任静态分析仪....................................................................................x4对本文件的xi1引言11.1软件的静态验证11.2低级语言分析21.3信任静态分析仪41.4本文件的贡献和结构52背景72.1Coq7中基于抽象解释的静态分析简介2.1.1玩具语言的语法72.1.2设置为建议82.1.3抽象数据类型82.1.4类型类112.1.5混凝土语义学122.1.6抽象语义学142.1.7流量敏感分析仪152.1.8非关系价值分析182.2CompCert192.3结论233Coq25中C类语言静态解析器的模块化构造3.1抽象域库263.1.1抽象域接口273.1.2抽象域示例：间隔283.1.3抽象域函子293.2固定点分辨率313.3数字抽象333.3.1数字环境的抽象343.3.2构建数字环境的非关系抽象。343.3.3数值抽象：实例和函子383.4记忆抽象40ii.3.4.1规格403.4.2基本实施423.5实验评估443.6相关工作和结论45内容物4经验证的价值分析&自我修改程序4.1通过抽象解释进行484.2Gooo ★51.................................................................................................................................................................4.2.1抽象语法514.2.2语义学544.3摘要口译员564.3.1内存抽象域564.3.2抽象语义学594.3.3固定点计算614.3.4抽象解释器的声音634.4案例研究和分析扩展644.4.1基本示例644.4.2第一个资料片：处理旗帜654.4.3第二个扩展：跟踪分区664.4.4第三个扩展：抽象解码684.5相关工作704.6结论和观点715C型记忆的精确抽象735.1背景735.2内存域概述755.2.1存储单元765.2.2指向域77的点5.2.3下置（关系）数值域775.2.4转换785.3技术细节785.3.1指针表达式795.3.2指向域79的点5.3.3数字转换805.3.4负载消除805.3.5变形金刚825.3.6分配存储845.4声音855.4.1功能性记忆855.4.2指向域87的点5.4.3具体化关系885.4.4关键引理89iii5.5扩展905.5.1局部变量905.5.2实现&类型Punning905.5.3空指针的情况925.6结论946实践956.1用Gotos96抽象解释结构化程序6.2程序间分析98内容物6.3进度验证1016.3.1非阻塞单子1016.3.2内存域中的进度验证1026.3.3数值域的进度验证1046.3.4进度检查总结1046.4更多数字域1046.4.1搬运机集成商1066.4.2多面体域1066.4.3域之间的通信1076.5使用分析仪1086.5.1常见陷阱1086.5.2样本结果1106.6结论1137结论1157.1摘要1157.2观点1167.2.1改进Verasco分析仪116的可用性7.2.2弱细胞和总结1177.2.3并发程序的经验证的静态分析119参考书目121v图列表2.1gE的语法，一种带有结构化表达式的玩具控制流图形语言2.2计算析因函数8的程序示例2.3设置为建议92.4gE表达式的语义132.5gE程序的语义132.6通用post-fixpoint求解器152.7CFM程序的语法202.8C#小调语句的语法2.9由CompCert22编译时完成的两个C程序3.1分析仪体系结构概述273.2弱晶格变宽的特征273.3弱晶格的规格283.4区间域，抽象有符号机器积分器3.5底部30域的晶格结构3.6定点检查器323.7数字表达式语法（nexpr）343.8数字表达式的语义353.9关系数字域363.10 非关系数字域373.11 抽象内存域413.12 CFM41的抽象语义3.13 分析的健全性定理423.14 有界间隔数（按程序和分析器有界）454.1自修改程序：作为字节序列（左）;在一些执行步骤之后（中间）;源程序集（右）。.................................................................................................. 494.2迭代定点计算514.3Goto ★52..............................................................................................................................................................4.4解码二进制代码534.5Goo oo ★54的......................................................................................................................................................4.6混凝土语义学554.7签署Go oo ★57的法案备忘录.................................................................................................................4.8抽象变换器示例594.9Go oo★60的小步骤语义.............................................................................................................................4.10 第61章第一次见面....................................................................................................4.11 主循环的theGoto★ analyzer62...................................................................................4.12 多级运行时代码ge.ne. R.A.I.第............................................................................... 65号4.13 阵列边界检查65vi4.14 假设转移函数的实现66vii图列表4.15 多态程序674.16 自修改Goo oo ★programcom推杆Fibonacci数字69...............................................4.17 摘要说明694.18 非分支694.19 抽象条件跳转694.20 自我修饰示例摘要705.1内存域接口745.2内存域草图765.3类型网格和抽象值点795.4转换（不包括在内）815.5假设的实施835.6假设83的测试案例5.7更新单元格：分配和存储845.8抽象内存规范875.9类型打孔示例905.10 C程序检查空指针5.11 处理空指针的抽象类型网格6.1Verasco分析仪的全球架构966.2C#小调摘要解释器的976.3用于过程间分析的内存域运算符996.4非块单子1016.5可达到混凝土状态1036.6权限字段1036.7Verasco分析仪105中的进度检查总结6.8阵列112的两种7.1Verasco116证明安全的不正确C程序viii法语中的Rěsuměğtendu1 程序的静态验证软件无处不在，到处都有错误。当程序的行为与预期不同时，就会发生错误这可能是由于这也可能是由于最后，这可能是运行时错误在许多情况下，我们接受了一个错误的但是，如果这是一个关键程序，则错误的后果当软件的不正确行为可能威胁到其用户或其运行时环境的安全性或完整性时，软件被称为"关键"软件这样的软件存在于许多系统中，从安全编程错误是多种多样的，有许多原因，并且已经提出了许多补救措施来避免它们或限制它们的影响。值得注意的是，编程语言在其设计中可以避免整个错误族例如，由许多语言提供的自动内存管理[JHM11]避免了与内存管理相关的任何安全错误如果编程错误无法避免，则可以通过动态安全策略检查来限制其后果：当编程错误导致不正确的行为时，程序将在没有任何警告的情况下停止。造成更多问题。例如，缓冲区溢出[Ale96]的一些后果可以通过使用金丝雀[Cow+98]来避免，金丝雀允许：在运行时，在一定程度上验证存储在堆栈上的返回地址的完整性。类似地，存储器访问协议可以通过在编译时注入到程序中的完整性测试来动态地强加[CCH06]。在像Java这样的高级语言中，程序系统地检查对数组元素的访问是否在其边界内，并满足类型规则：任何违反都会产生一个错误，该错误可以被程序处理或中断。S’assurer ainsi lors de l’exécution du bon déroulement d’un programme a un coût,puisque幸运的是，有些检查是多余的，这可以静态地证明：在运行之前法语中的Rěsuměğtenduviii[WWM07] 另一种方法是静态地证明不受控制的操作是安全的（例如，对数组元素的访问在其边界内），并且仅当静态分析的结果不够精确时才注入控制语句。C’est l’approche suivie par exemple dans CCured低级语言的设计也可以考虑到安全性。 在这些语言中，所有的程序都是先验安全的：编译器拒绝它不能证明安全的程序程序员必须显式注释程序中需要动态验证安全属性的部分。这些动态或混合方法非常有效地防止了编程错误的转移，并限制了这些错误的后果，例如在"心脏出血"缺陷[CVE 13]的情况下：受影响的服务器能够通过访问表的边界来泄漏kibi-bytes的秘密数据（密码、加密密钥等然而，动态地防止错误发生并不总是足够的：在关键的上下文中，程序不应该因为编程错误而此外，在允许分解抽象的低级语言中，动态验证并不总是可能的，或者只是以一种不合理的方式。C’est也就是说，必须在程序执行之前预测其所有可能的行为，同时考虑到任何可能的环境。静态分析器是自动检查程序文本并推断有关程序执行的属性的工具;例如，不可能发生给定系列的有各种各样的静态分析仪，有不同的用途一些这样的覆盖率[Bes+10]旨在发现尽可能多的编程错误：它们应用于正在开发的程序，这些工具并不声称是正确的：有些分析师做出务实的假设，只有当这些假设得到满足时才是正确的例如，同样，应用于用C编写的Microsoft Windows设备驱动程序的静态驱动程序验证器[Bal+06]也是正确的，前提是被扫描的程序以安全的此分析器验证特定程序（设备驱动程序）是否满足特定属性（驱动程序有些分析器是正确的。例如，ASTR E[Mau 04;Cou+05]用于检查程序，以证明它被空中客车公司用来证明其一些飞机的电气飞行控制程序的安全性。在这篇论文中，我们集中在正确的静态分析的程序，这必须面对以下两个困难：它是不可判定的;另一方面，这样的分析器必须可靠。根据赖斯定理，没有一个正确的静态分析器可以对所有的变量产生精确的结果。ix2低级程序。这样的分析器必须求助于近似，并且在许多情况下失败。因此，设计静态分析需要找到一个中间地带：哪些程序将被精确地分析，在哪些情况一个有用的分析器必须在许多情况下放弃（一个无限的），但必须足够精确的目标程序类别。分析仪的另一个重要特性是它的效率：它必须在足够短的时间内提供准确的结果L’interprétation abstraite2 低级语言的分析静态分析器依赖于低级语言只提供很少的抽象，即使它提供了抽象这表明最好然而，这一些程序直接用低级语言编写，要么是因为在这种情况下，在它存在的情况下，它可能是不可用的，例如，由于知识产权的原因然而，程序通常是用主要为程序员设计的语言编写的，并且在它们可以被机器执行之前，它们经历几次转换，统称为编译，以产生适合于机器执行的形式的相应程序下图显示了最初用Scade语言编写的航空电子程序编译过程中的各个步骤这个编译过程本身可能是错误的，并在编译的程序中引入错误，或者更简单地说，使从源代码获得的分析结果无效概念优化执行因此，可以在尽可能低的级别进行分析，以便在执行程序时将其操作为最终形式。Reps [BR 08; RBL 06]和我们在第4章中特别使用了这种方法。它的主要优点是分析的程序和执行的程序之间的距离最小。但没有合适的近似值可以选择：什么是分析给定程序族的正确抽象此外，大多数静态分析都是为其他语言设计的。CRTL阶段二进制装配工法语中的Rěsuměğtendux一个高级分析器，它提出了一些抽象（函数、变量、类型只要因此，在可能的情况下（即当源代码可用时），明智的做法是分析更高级别形式的程序，并证明在该更高级别形式上建立的属性在编译过程中有两种方法来建立这样的证明：验证编译和翻译验证。L’emploi 一个经过验证的编译器是一个带有正确性定理的编译器例如，CompCert编译器确保编译然而，编译后的程序必须在运行时没有翻译验证[PSS98;Nec 00]包括验证这需要在每次运行分析器时进行额外的计算该方法用于分析仪的验证。麻雀[Kan+14]L’exemple3 我们能信任静态分析仪吗？依赖静态分析器来证明特定程序是安全的似乎是值得怀疑的 更糟糕的是，为了这最后一个性质是先验地更微妙的建立。同样，为了正式确定一个程序在运行时不会产生错误，或者它计算出的东西是正确的，我们必须首先正式编程语言的形式语义是对程序含义它精确地定义了程序如何将其结果与被分析程序的行为相关联的静态分析器的正确性证明通常是与分析器的实现工作分开的这就产生了两个问题：一方面，手动证明容易出错并且难以验证;另一方面，在验证的模型和实现的程序之间存在差异。这两个问题都可以通过使用证据支持工具来解决。xi4 本文件的贡献和组织如公鸡[Coq15]。这样的工具主要是一个怀疑定理证明器：它可以用来陈述性质和证明，并且给定一个证明项--一个表示证明陈述有效的语法对象即使证明者具有自动化的证明查找和决策过程来帮助用户构建证明项，也只需要信任验证证明项的通常较小的核心此外，Coq是一种纯函数式编程语言：程序和属性可以用相同的形式来这些程序可以直接在Coq中运行，但也可以提取它们以生成可以链接到其他程序的OCaml程序这些可以执行输入和输出，从而与外部世界通信CompCert编译器是从Coq开发中提取的一个值得注意的程序示例由该编译器操作的编程语言（从C到汇编）的语法和语义以及编译过程都是用Coq定义的，因此也是用Coq编写的属性可以引用编译器的有效代码来声明其正确性因此，被检查的程序和正在执行的程序之间的间隙机械化证明最近已经成功地应用于各个领域：数学结果，如开普勒猜想[Hal+15]、出卖定理[Gon 07]和费特-汤普森定理[Gon 13];操作系统实现的验证[Kle+10]。静态分析的机械化验证在过去通常应用于数据流分析的经典框架，而不是Klein和Nipkow通过数据流分析提出了Java字节码的类型推断Bertot等人[BGL06]已将此分析框架应用于编译器优化，Cachera等人也已将此分析框架应用于编译器优化。[Cac+05]至控制流分析。 Vafeiadis等人[VN11]使用简单的数据流分析来验证它消除了并发C程序中的同步障碍。David Pichardie在他的博士论文[Pic05]中提出了一种基于抽象解释来验证静态分析仪校正的他将这种方法应用于分析器，这些分析器处理用微型语言编写的程序在本文中，我们扩展了这种方法来构建和验证正确的基于抽象解释的静态分析器，这些分析器处理可执行程序：二进制代码或源代码，这些程序可以由经过我们的分析以现实语言为目标，并考虑到分析低级语言所固有的复杂性4 本文件在这篇论文中，我们展示了如何将机械化验证方法应用于构建以法语中的Rěsuměğtenduxii玩具二进制语言（第4章）。在本文档中，我们描述了几个静态分析器，所有这些分析器都已通过Coq Proof l'assistant证明是正确的它们的校正是相对于目标语言的语义建立的在可能的情况下第2章介绍了Coq中静态分析器的形式化验证：如何定义编程语言的语法和语义，基于抽象解释的静态分析器的一般形式是什么，以及如何进行这种分析器的正确性在第3章中，我们提出了一个通用的方法，我们将在整个文档中应用该方法。在本章中，该方法被应用于相对简单的语言（CompCert编译器的CSG中间表示的子集：没有全局存储器、没有在第4章中，我们使用相同的方法，并重新使用以前的分析器的组件（特别是接口和抽象数字域的实现），研究了在分析之前结构（特别是它们的控制流图）未知的程序的分析我们对二进制程序的正确反汇编问题感兴趣，并为一种玩具二进制语言构建了一个经过验证的静态虽然非常简单，但受x86汇编程序的启发，这种 然后，它可以证明被分析的程序是安全的，第5章回顾了结构化程序（以不可变控制流图的形式呈现）的分析，但这些程序在弱结构化存储器上运行：变量不是简单的不相交实体，而是可以通过指针部分访问的最后，第6章专门介绍了C minor语言的解析器，它与C非常接近它自动证明了CompCert校正定理的前提。本文中介绍的所有程序都可以在相关网站[Web]上在线获得。这项工作特别是，为了完整起见，本文介绍了其他博士生的贡献— 第3.5节中介绍的CFM分析的实验评价由AndréMaroneze[Mar14]进行。— 第6.4.2节中介绍的Verasco解析器的抽象多面体域是AlexisFouilhé[FB14]的作品。— 第6章介绍的Cminor的过程内迭代器（§6.1）、理想整数和机器整数之间的抽象数域的函子（§6.4.1）以及域之间通信通道的机制（§6.4.3）都是雅克-亨利·乔丹（Jacques-HenriJourdan）的作品。xiii第一章引言1.1 软件的静态验证软件无处不在，到处都有bug。当程序的行为与预期不同时，会出现错误。这可能是一个设计或使用问题：软件用于一个特定的目的，而它是为一个不同的目的设计的。该错误可能是由功能错误引起的：程序功能不正确，无法完全满足其规格。此错误可能是运行时错误;在这种情况下，程序崩溃。在许多情况下，一个有缺陷的软件不是一个问题;在大多数情况下，它是一个不愉快的问题。然而，当出现故障的软件是安全关键型的时，错误的后果可能是严重的。当软件的错误行为会危及其用户或运行时环境的安全性或完整性时，软件被称为"安全关键"。这样的软件可以在许多地方找到，包括安全气囊，电传飞行航空电子设备，铁路信号，和动力装置控制。编程错误有许多原因，并且已经有许多尝试来防止它们或限制它们的影响。编程语言的设计本身可以帮助避免整个错误家族。对于实例，自动内存管理[JHM11]，由多种语言提供，避免了与内存管理相关的所有安全错误（例如，双重免费，免费后使用。如果无法避免编程错误，则可以通过动态执行安全策略来减轻其后果：在编程错误导致错误行为的情况下，程序将中止而不会造成任何进一步的伤害。例如，可以通过使用canaries[Cow+98]来避免流缓冲[Ale96]的一些后果，canaries[Cow+98]允许在运行时检查存储在堆栈上的返回地址的完整性（在一定程度上）类似地，可以通过在编译时引入的完整性检查[CCH06]来动态地强制执行内存访问协议。像Java这样的高级语言系统地检查数组访问是否有边界并遵守类型规则：任何违反都会导致错误，可能会被程序本身捕获或阻止它。安全属性的这种运行时强制执行是有成本的，因为它可能会增加运行程序的执行时间、代码大小或内存足迹。幸运的是，一些检查可以被静态地证明是不必要的：在执行之前，仅仅通过查看源代码，就可以证明一些检查不会失败：然后，它们可以被删除。这就是优化编译器所做的;例如，Java HotSpot™编译器系统地插入检查，然后尝试通过自动证明不需要它们来删除它们[WWM 07]。另一种方法是静态地证明未检查的操作是安全的（例如，数组访问是在边界内），并在静态分析结果不够精确时插入检查。CCured[Nec+05]和WIT[Akr+08]采用了这种方法，他们编写了仪器C程序来执行安全检查。低水平第一章引言2语言的设计也可以考虑到安全性，例如Cyclone[Jim+02;Gro+05]或Rust[Rus t]。在这些语言中，安全性是默认值：编译器将拒绝无法证明安全的程序。程序员必须显式注释程序中必须动态检查安全属性的部分。这些动态或混合方法在防止漏洞利用和避免编程错误的一些不良后果方面非常有效，例如在心脏出血漏洞[CVE13]的情况下：有缺陷的服务器通过越界读取阵列悄悄地泄漏了大量的秘密数据（用户密码、秘密加密密钥在没有这种动态避免错误的情况下，它不是万能的：在关键设置中，程序不应该因为编程错误而停止或崩溃。此外，在允许破坏抽象的低级语言中（程序员是可信的），动态检查是不可能的或极其昂贵的。因此，为了确保一个程序是有意义的，并且它的执行不会产生错误，必须对该程序进行静态研究。这意味着在程序的任何执行之前预测所有可能的行为，考虑任何可能的环境。静态分析器是自动检查程序文本和有关程序执行的推断属性的工具，对于某些族中没有错误的实例。有一个广泛的这样的工具，不同的喜欢。一些类似于覆盖率工具[Bes+10]的工具旨在尽可能多地发现编程错误：它们应用于软件的开发版本，以便在开发过程中尽可能早地发现错误。这样的工具并不假装是健全的：如果它们没有发现错误，并不意味着没有错误。一些分析师做出了实际的假设，并在他们的指导下得到了倾听。例如，针对智能手机应用程序的Infer工具[Cal+15]假设不存在类似地，静态驱动程序验证器[Bal+06]以用C编写的Microsoft Windows的设备驱动程序为目标，它被认为是被解析的程序内存安全的。 此分析器验证特定软件（设备驱动程序）是否满足特定要求（是否正确使用了驱动程序API）。最后，一些分析师是健全的。例如，AstrE[Mau 04;Cou+05]喜欢验证软件，以证明它们不会产生任何运行时错误。它被空中客车公司用来证明其一些飞机的电传飞行计划。在这项工作中，我们的重点是这样一个健全的静态验证程序，这面临着以下两个问题：手头的问题是不可判定的;分析器应该是可靠的。根据赖斯定理，没有一个静态分析器能对所有程序产生精确的结果。在许多情况下，它必须近似而不能产生任何有用的结果。设计一个静态分析，涉及正确的交易：什么样的程序被准确地分析，在什么情况下，分析器放弃。一个有用的分析器必须（无限期地）在许多情况下给出，但对感兴趣的程序族要足够精确。分析器的另一个敏感特性是它的效率：它必须足够快地给出有意义的答案。摘要解释[CC77]提供了一个理论框架来构建具有不同精度和成本的静态分析1.2 低级语言分析静态分析器依赖于目标编程语言提供的抽象（变量、函数、对象、类型、自动内存管理等），以获得准确和合理的结果。低级语言不具有抽象功能，或者程序员是31.2 低级语言允许打破他们。这将建议更好地分析用高级语言编写的程序。然而，这并不总是可能的，甚至是可取的。有些程序是直接用低级语言编写的，因为它们需要打破抽象的能力，所以只需要低级服务，如对高级语言、硬件驱动程序或操作系统的标准库和运行时支持。在这种情况下，不存在可以分析的高级别伪影即使它存在，它也可能不可用，例如出于知识产权原因。程序通常是用友好的语言编写的。程序员，在他们实际上可以在机器上运行之前，他们进行几次转换，统称为编译，以友好的形式为执行机器生成相应的程序。右边的图片描绘了最初用Scade编写的航空电子程序汇编中的各个步骤。 此编译过程本身可能是错误的并引入错误，或者更简单地使从源代码获得的分析结果无效。因此，分析可以在最低可能级别进行，在程序执行时对其进 行操 作。 值 得 注意的是，代表们采用了这种方法[BR08;RBL 06]，并在第4章中进行了应用。设计优化装配执行它的主要优点是分析的程序和运行的程序之间没有差距这也是它的主要反馈：程序是在一个非常低的层次上分析的，在这个层次上，编程语言（如果可以这样称呼的话）很少或没有抽象的特征，并且很难对程序的形状做出任何假设。不能选择足够的近似值：分析给定系列程序的正确抽象域是此外，大多数静态分析是为具有一些抽象（函数、变量、类型......）的高级语言设计的;并且分析器可以依赖这些抽象来精确：当被分析的程序不遵守抽象时，它可以被设计为非常不精确：当它遵守抽象时，分析是尽可能精确的，并且当它不遵守抽象时，分析很快就会得到结果，而正确，非常困难因此，在可能的情况下进行分析是明智的（即，当源代码可用时）程序的高级形式，并证明编译过程保留了该高级形式上的属性。有两种方法来建立这样的属性：验证编译和翻译验证。已验证编译器的使用可以证明在源程序上建立的属性对于已编译程序的所有执行都是合理的。一个经过验证的编译器是一个带有正确性定理的编译器;它被证明一次，并在编译器的所有例如，CompCert编译器保证编译不会在编译程序中引入行为，并保留在源代码上建立的任何安全编译后的程序必须没有运行时错误，幸运的是，这是静态分析器可以推断的一种属性。翻译验证[PSS 98;NEC 00]包括验证特定结果是否正确用于特定程序。这涉及分析器每次运行时的附加计算。这种方法已应用于Sparrow分析仪[Kan+14]的验证。CompCert的示例表明，这两种方法可以结合使用：在验证另一个编译过程的同时验证一个编译过程（作为注册表分配，用于实例）。CRTL阶段二进制第一章引言41.3 信任静态分析器依赖静态分析器来证明给定程序是安全的可能看起来可疑。由于静态分析器本身是一个程序，因此也容易出现错误。更糟糕的是，为了相信某个程序是安全的，我们现在必须相信另一个程序在功能上是正确的。这最后一个属性先验地很难建立。同样，抽象解释是设计静态声音分析器的一种方法。因此，为了正式确定一个程序不会产生错误，或者它计算的是正确的东西，我们需要正式地赋予程序以意义。程序设计语言的形式语义是对程序意义的数学描述。它精确地定义了一个程序是如何执行的，它计算了什么功能。静态分析器的健全性证明将其结果与被分析程序的行为联系起来，通常是一种纸上的工作，与实现工作不同。这引起了两个问题：首先，证明工作容易出错，难以检查;其次，验证的模型和实现的程序之间存在差距。这两个问题都可以通过求助于像Coq [Coq15]这样的证明助手来解决。这样一个工具首先是一个怀疑定理证明器：它可以用来写陈述和证明，并给出一个证明项--一个传达某些陈述所持有的论点的语法对象--Coq可以检查它的有效性。即使定理证明器具有一些自动化的证明搜索和决策过程，以帮助用户在构建证明项的过程中，我们只需要信任一个执行证明检查的简化内核。Coq也是一种纯函数式编程语言：我们可以用单一的形式体系编写程序和属性。这些程序可以直接在Coq内部运行，但它们也可以被提取到OCaml编程语言，以便与其他可以执行输入和输出并与外部世界通信的程序链接。CompCert编译器是从Coq开发中提取的程序的一个值得注意的例子由编译器操作的编程语言的语法和语义（从C到汇编）以及编译过程在Coq中完成，因此也用Coq编写的属性可以引用编译器的实际代码来声明其正确性。在验证的代码和运行的代码之间不再存在间隙。机械化证明最近已经被成功地应用于各种领域：开普勒猜想[Hal+15]、双色定理[Gon 07] 和 费 特 - 汤 普 森 定 理 [Gon 13] 等 数 学 结 果 ; 操 作 系 统 实现的 验证[Kle+10]。静态分析的机械化验证工作主要基于经典的数据流框架，而不是更一般的抽象解释。Klein和Nipkow实例化了Java字节码类型推理的数据流框架[KN 06];Coupet-Grimal和Delobel [CD 04];以及Bertot等人。[BGL06]用于编译器优化，Cachera等人[Cac+05]用于控制流分析。Vafeiadis等人[VN11]依靠简单的数据流分析来验证针对C程序的竞争对手David Pichardie博士[Pic05]提出了一种基于抽象解释验证静态分析器健全性的方法。他将这种方法应用于分析在小型语言和为说明目的而编写的程序上操作的程序。
我的内容管理
展开
