及时编译奥雷利奥·巴里埃引用此版本：奥雷利奥·巴里埃。及时编译的正式验证。其他[cs.OH]。雷恩高等师范学校，2022年。英语。NNT：2022ENSR0038。电话：03987749HAL ID：电话：03987749https://theses.hal.science/tel-03987749提交日期：2023年HAL是一个多学科的开放存取档案馆，用于存放和传播科学研究论文，无论它们是否被公开。论文可以来自法国或国外的教学和研究机构，也可以来自公共或私人研究中心。L’archive ouverte pluridisciplinaireT Hese德博士学位L’ÉCOLE NORMALESUPÉRIEURE和科尔 D八角形第601章数学与信息与通信科学与技术通过奥勒拉·巴里埃及时编译2022年12月19日在IRISA发表并答辩论文答辩前的报告员：Andrew Appel教授评审团组成：主席：检查员：安德鲁·上诉教授泽维尔·勒罗伊教授斯蒂芬·默茨研究总监马格努斯·梅林副教授艾伦·施米特研究总监曼努埃尔·塞拉诺研究总监Dir.论文：桑德琳·布莱兹大学教授-雷恩第论文共同导师：大卫·皮查迪研究者3R总结在FRancais本文以法文摘要开始。本文件的其余部分以英文编写，从第8页开始。即时编译（或即时编译）是一种越来越流行的运行程序的技术。自20世纪60年代以来，动态编译器（或JIT）就已经存在[Aycock 2003]，但它们的使用对于Python [PyPy 2022]、JavaScript [V8 2022]、Julia [Julia 2022]、R [R2022]、Lua [LuaJIT 2022]或MATLAB[MathWorks 2022]等动态语言尤其普遍。今天，JIT也被用于静态语言，如Java [ HotSpot2022 ]或Linux内核中的eBPF语言[ eBPF 2022 ]。JIT为动态语言提供了出色的性能，因此大多数现代Web浏览器都使用JIT来运行所访问网页上的程序。Firefox使用SpiderMon键[Firefox2022b]，Google Chrome和Chromium使用V8 [V82022]，Safari的WebKit引擎使用JavaScriptCore [WebKit2022]。所有这些示例都使用动态编译来运行JavaScript程序。这些网络浏览器拥有数十亿但由于它们的复杂性，它们的JIT容易受到许多错误和漏洞的影响。此类漏洞太多，无法在此处详尽列出[Firefox2022a]。如果攻击者知道JIT中的缺陷，他们可以创建并分发利用该缺陷的JavaScript程序。例如，该团队还发现了在Google Chrome漏洞被修补之前这些攻击可能会产生严重的后果，例如然而，Web浏览器在今天是必不可少的4Web浏览器及其JIT并不是敏感程序的唯一示例，已经设计了许多技术来检测或防止具有严重后果的软件错误。 最直观的方法是在一组随机生成或选择的输入上测试程序。 该测试可以发现许多错误，但如果不测试程序的所有可能输入，就不能保证没有错误，而这通常是不可能的。为了获得更强的保证，形式化方法旨在证明程序图的性质有了适当的抽象或模型，就有可能在不执行程序的情况下对程序进行数学推理例如，Astrée静态分析仪被用于确保两种空客飞机的主电气飞行控制软件中不存在一类错误[ Delmas和Souyris 2007 ]。形式化方法包括许多技术，如演绎验证是在证明助手中表示数学定义和推理的过程。证明助手是用于以数学严谨性陈述和验证证明的程序 它们要么是自动的，如Why3 [Filliâtre 2012]，要么是F *[Swamyet al. 2013年]，或互动，如Coq [Coq 2022]，Isabelle/HOL [Nipkow等人，2013年] 2002年]和ACL2 [Kaufmann等人。 2000年]。 与手工证据不同，在有助手的情况下，不可能忘记书面证据中的一个案例。如果你信任一个证明助手，用它来编写和验证证明会带来很大的保证，并且不为了使用形式化方法（如演绎程序验证）对程序执行进行数学推理，必须定义形式语义，即对程序行为的严格描述。已经为几种编程语言定义了形式语义，例如C [Nor-rish1998，Blazy和Leroy 2009，Krebbers和Wiedijk 2011]、JavaScript [Bodin et al. 2014]或WebAssembly [Watt等人，2021]。为了证明程序属性，可以使用该程序的形式语义和程序逻辑。例如，使用C的形式语义和称为分离逻辑的程序逻辑，用C编写的加密原语在Coq中被证明是正确的要信任在计算机上运行的程序，您不仅要信任该程序的源代码，还要信任它。5也适用于其执行机制。例如，许多编程语言都是静态编译的。静态编译程序包括在执行程序之前将其在静态编译的情况下，必须确保编译器没有在它转换的程序中引入错误。为了验证这一特性，可以使用形式化方法来证明这种转换保留了编译程序的形式语义。这 CompCert [Leroy 2009 a]，CakeML [Ku-mar等人，2009年]。 2014]和VELLVM [Zhao等人，2014] 2012]是经过正式验证的编译器的示例。 例如，CompCert将用C编写的程序编译为多个目标架构（如x86、ARM、PowerPC和RISC-V）的汇编程序。CompCert是用Coq编写的，转换程序的Coq代码可以被提取为OCaml可执行程序。CompCert还包含一个机械化的Coq证明，它将编译程序的形式语义与编译器输入程序的形式语义联系起来。编译器是复杂的程序，它们的形式验证特别困难。但是，此检查是确保构建没有引入任何错误的最安全方法大多数编译器都没有经过验证，因此没有此保证。单靠测试不足以发现所有的编译器bug，正如一项使用随机生成的输入程序检测C编译器bug的研究所表明的那样[ Yang et al.2011 ]。在两个主要的C编译器GCC和LLVM中发现了数百个bug，但在CompCert的正式验证部分没有发现任何bug。这些结果表明，测试编译器传统上 ，编程语言长期以来要么被编译，要么被解释。为了解释一个程序，我们使用了一个解释器，另一个程序，它一个接一个地读取、翻译和执行输入程序的指令，直到它的执行结束。动态编译是另一种混合了编译和解释的运行时机制。它的特点是混合执行和优化执行程序。6切割。例如，一些JIT从解释程序开始，然后在运行时将程序的一部分因此，JIT的执行是解释和执行动态生成的本机代码的混合。JIT是使用特定现代技术的特别复杂的软件。首先，JIT通常包含完整的静态解释器和编译器（有时甚至是多个静态编译器，如We- bKit [WebKit2014]）以及协调它们交互的附加机制。此外，JIT使用自己的优化和技术来实现更快的执行时间。例如，许多现代JIT使用推测性操作优化来专门化动态编译的代码这种推测包括预测程序的未来行为，并使用该预测来生成更快的专用代码。尽管JITs存在漏洞并且使用越来越多，但与传统的静态编译器相比，JITs几乎没有经过正式的这种缺乏正式化的首先，JIT比静态编译器更新得更多，也更复杂其次，没有标准的方法来设计JIT，每个实现都有自己的组件（不是所有的JIT都包含解释器，就像早期的V8版本编译所有执行的代码一样）、优化或架构。最后，诸如推测性优化之类的JIT特定技术通常被降级为实现细节，没有足够的文档或抽象来形式化它们。本论文的内容执行速度不应该是bug的同义词JIT中的此类错误可能会产生严重后果。在本文中，我们证明了形式化方法可以应用于JIT，以确保它们的正确性。由于JIT重用了静态编译的技术，我们重用了形式化验证的静态编译证明技术来证明JIT的正确在我们的工作中，我们开发了经过验证和可执行的JIT原型我们做出以下贡献：形式化JIT：我们为现代JIT设计了一个体系结构，包含每个关键元素，并为每个组件提供了一个清晰的规范我们的体系结构包含动态解释和编译的混合，7和推测性优化。我们为包含推测的JIT操作的programs提供了一个形式化的语义，这是一种很少被记录的机制。新的验证挑战我们确定了正式JIT验证中的四个新挑战。首先，JIT中的优化是动态的，这与传统编译器的情况不同。 我们采用CompCert中使用的模拟技术来实现这些优化。其次，推测性优化是JIT的一个特性因此，我们使用前面定义的形式语义提供了几个推测优化的正确性证明。第三，现代JIT的一些组件我们设计了一个特定的编码来表示和推理Coq中的不纯JIT最后，JIT必须生成本机代码，并且通常依赖于静态编译器 我们将证明可以在JIT中重用CompCert代码和正确性证明。新的证明技术对于这些挑战中的每一个，我们都提出了正确性的证明我们所有的证明都已在Coq Proof Assistant中机械化我们证明了一个定理，该定理保证JIT对程序的执行符合所一个经过验证和可执行的JIT我们在Coq中的JIT开发可以提取到OCaml中并执行。因此，我们开发了一个JIT原型，它运行的程序具有现代JIT的所有特征，同时还伴随着我们的工作揭开了现代JIT所使用的复杂技术的神秘面纱我们的开发使我们8一个熟人首先，也是最重要的，我要感谢我的顾问，桑德琳·布拉齐和大卫·皮查迪。你给了我无限的支持和无数的机会。我学到了很多，真的很喜欢和你一起工作。对于你的指导，你的帮助，你的支持，我最深切的感谢。我也要向我的博士评审团表示衷心的感谢，因为我很荣幸有这样一个专家小组。我特别感谢我的评论家安德鲁·阿佩尔和泽维尔·勒罗伊。我们的讨论，您的意见，问题和报告帮助塑造了这篇论文。我有幸与Olivier Flückiger和Jan Vitek合作这个机会对我的博士学位起了令人难以置信的决定性作用，也是对JIT的精彩介绍。 我的研究对我们的共同工作很有帮助，谢谢。我也感谢Roméo La Spina为我们的JIT所做的工作最后，我想衷心感谢整个凯尔特/伊壁鸠鲁队在这些难忘的岁月。我想和你一起工作。9TABLE来自C组图12表模拟表151导言171.1动机171.2论文和稿件201.2.1四个JIT特定的验证挑战1.2.2合作和出版物221.3大纲232及时编译的背景252.1及时编译器中的猜测262.1.1推测性优化示例262.1.2非优化和堆栈更换282.2各种JIT设计302.3JIT形式化的相关工作323CompCert编译器35的背景3.1正式验证的C编译器353.1.1CompCert优化383.1.2CompCert定理393.2CompCert41的仿真框架4设计正式验证的JIT474.1形式化JIT体系结构474.2作为公鸡状态机4.3作为外部启发式的54104.4JIT正确性定理554.5动态优化57内容表4.5.1嵌套模拟技术574.5.2测试外部反向模拟604.5.3JIT优化器规范625形式验证的推测性优化655.1CoreIR，一种具有推测性的665.1.1CoreIR语法695.1.2CoreIR语义705.2操作推测性指令745.2.1锚点插入745.2.2假设插入765.2.3恒定传播765.2.4移除锚点775.2.5延迟假设插入775.2.6与推测内联795.3投机操纵的正式验证805.3.1锚钉插入的正确性815.3.2假设插入的正确性845.3.3恒定传播的正确性865.3.4移除锚点的正确性895.3.5延迟插入的正确性假设895.3.6与推测一致的正确性915.4正式验证的JIT后端编译器936不纯公鸡JIT95的正式验证6.1不纯JIT的一元编码966.1.1需要一种新的提取方法966.1.2JIT作为不完整的公鸡程序986.1.3JIT不纯基元100的最小接口6.2指定效应的现有解决方案：状态和错误单子101116.3在Coq中写入不纯JIT的解决方案：Free Monads1026.4自由单子的单子规范和语义1046.5有效JIT106的不纯实现6.6通过改进促进正确性证明1076.7过渡的非原子性：从x86到Rescue的小步骤语义内容表6.8不纯程序验证的相关工作1137JIT后端编译器的正式验证1177.1将RTL程序拆分为直接重用CompCert证明7.2混合语义：与多个局域网有关的相互重叠的处决片段7.3RTL第125代的正确性7.4本机代码生成128的正确性7.5正式验证的JIT后端编译器1308评估1338.1合成所有模拟1338.2可信代码库1368.3我们的公鸡JIT实现1388.3.1实施和证明重复使用1398.3.2我们的不纯基元C库1408.3.3评估1409结论1459.1摘要1459.2前景1479.2.1重新编译和上下文调度1499.2.2直接呼叫和构建1509.2.3用于现实语言的正式验证的JIT151附录参考书目15712TABLEF.伊古尔斯2.1一个简单的循环，其中类型保持不变262.2图2.1的解释说明272.3图2.1中循环的优化迭代，包括推测性优化2.4JIT执行的时间表293.1CompCert体系结构373.2恒定传播优化之前和之后的RTL程序3.3CompCert40中简化的小步骤语义3.4CompCert正确性定理413.5反向模拟图433.6进步保护433.7前瞻性模拟图433.8CompCert前后向定理443.9作曲前向模拟454.1JIT设计的关键组件484.2CoreIR程序计算前10个正方形的示例4.3作为状态机的JIT体系结构4.4提取JIT转换的OCaml循环524.5JIT小步骤语义规则544.6分析的外部参数544.7JIT正确性定理574.8外部模拟关系584.9定义外部模拟关系⇒ext594.10 外部模拟图615.1投机的例子675.2CoreIR70的语法135.3CoreIR小步骤操作语义715.4锚点插入后的运行示例7514图表5.5假设插入76后的运行示例5.6恒定传播后的运行示例775.7移除锚点78后的运行示例5.8延迟假设插入785.9CoreIR计划，其中对G的调用应在F79中内联5.10 为正确的推测内联合成5.11 锚点插入的不变关系⇒ 825.12 锚点插入的堆栈不变825.13 锚点插入的⇒关系示例835.14 假设插入的不变关系⇒ 855.15 假设插入的堆栈不变855.16 锚点指令的响亮语义规则875.17 从前向响亮模拟到后向模拟875.18 假设插入延迟的约关系905.19 在内联代码92中匹配去优化5.20 中点正确性946.1使用本机代码生成97的JIT的纯组件和非纯组件6.2设置公鸡状态和错误单子1026.3自由单子的定义1036.4免费的单子构造函数并使用它们编写有效的JIT1036.5代表性基元的Coq一元规范1056.6将自由计算转换为状态和错误计算1056.7JIT小步骤语义规则1066.8A C基元实现及其Coq单子规范6.9在OCaml106中执行免费计算6.10 两个原始规范的1086.11 非原子状态机定义1106.12 为NASM110中的非原子跃迁提供小步长语义6.13 NASM JIT111的小步骤语义规则6.14 不纯JIT正确性定理1137.1将CoreIR函数转换为两个RTL函数120157.2由JIT后端编译Fun11217.3混合语义的语义状态12316图表7.4混合语义学的一些代表性规则7.5在将函数F转换为RTL块127时保留不变7.6在混合语义学中保留原始调用7.7后端正确性1308.1组成我们所有的模拟1348.2JIT实现的1398.3推测LuaLite的类型变量1418.4Lua Lite执行的性能比较，运行时在142秒内8.5在CoreIR143中打印主编号17TABLE S的模拟1JIT反向模拟（纯版本）552JIT63中的动态优化器正确性3锚钉插入的正确性814立即插入的正确性假设845恒定传播的正确性886移除锚钉的正确性897延迟插入的正确性假设908与推测性指令内联的正确性919JIT中间端正确性9310交换规范的细化定理10911JIT反向模拟（不纯版本）11312CoreIR和CoreIR程序上的混合语义的等效性12513RTLblock第126代的正确性14从RTLblock128生成RTL的正确性15本机代码生成的正确性12816JIT后端正确性13117第一章一、引言1.1动机及时编译是一种运行程序的技术，近年来越来越受欢迎。自20世纪60年代以来，即时编译器（或JIT）就已经存在[Aycock2003]，但它们的使用已经大大扩展到动态语言 ， 如 Python [PyPy2022] 、 JavaScript [V82022] 、 Julia [Julia2022] 、 R [R] 、 Lua[LuaJIT2022]或MATLAB [MathWorks2022]。 JIT也用于静态语言，如Java [HotSpot2022]，以及Linux内核中的其他用例，如eBPF [eBPF 2022]。 JIT为动态语言提供的性能解释了当今大多数现代Web浏览器使用JIT来运行它们在Web上找到的程序。Firefox使用SpiderMonkey [Firefox2022b] 、 Google Chrome 和 Chromium 使 用 V8 [V82022] 以 及Safari的WebKit引擎使用JavaScriptCore [WebKit2022]，所有这些都使用即时编译来运行JavaScript程序。这些Web浏览器总共拥有数十亿用户，但由于软件复杂，它们的JITs容易受到许多错误和漏洞的影响。此类漏洞数量太多，无法详尽列出[Firefox 2022a]。例如，Project Zero团队 发 现 恶 意 软 件 使 用 JavaScriptCore 中 的 JIT 错 误 在 Safari 上 执 行 恶 意 代 码 [ProjectZero2019;2020]。该团队还报告了在报告和修复漏洞之前被利用的Chrome漏洞[ProjectZero2021a]。 Web浏览器的性质使它们暴露于对手的设置，因为它们的JITs可以执行在Web上找到的任何输入程序。了解JIT漏洞的攻击者可以设计一个针对它的JavaScript程序。例 如 ， SpiderMon-key 中 的 漏 洞 在 针 对 Coinbase 公 司 的 网 络 钓 鱼 攻 击 中 被 利 用[Coinbase2019]。发送给公司员工的电子邮件包含一个链接，当使用Firefox打开时，该链接将运行一个利用JIT错误在公司计算机上安装恶意软件的程序然而，网络浏览器在我们的日常生活中被大量使用，有时用于敏感的应用程序，这些应用程序不会受到错误的影响
我的内容管理
展开
