形式化方法 ｜编译器形式化验证

Posted 2021-04-26 软件工程研究与实践

作为用于产生代码的工具，编译器的实现和维护自然经过了“精雕玉琢”，因此编译器的正确性问题容易被人们忽视。但了解实际情况的人都知道，编译器的“误编译”问题是司空见惯、习以为常之事。对于许多领域来说，由于一般不会引发本质的问题，又是小概率事件，人们也往往容易忽视误编译所带来的影响。然而，对于安全关键系统而言，则必须考虑因编译器引入的错误，否则花大力气在源程序级的验证工作可能在目标程序级失效。实际上，如航空领域的RTCA DO-178B/C标准，编译器属于需要鉴定的工具类软件，需要按照机载软件的要求一样对待。

就我们所能了解到的（或许不全面），在国内，安全关键领域的编译器来源主要有两种途径。一是直接向国外购买被这些领域高度认可的编译器，比如Wind River（风河）和Green Hills（绿山）的编译产品，这些编译器均有相关行业标准的认证，无论是在安全性增强还是在各类优化方面都很有代表性。抛开是否真正的安全可信不说，这一来源的最大问题是非自主可控，其次是一些关键部分对我国禁售，极大制约了国内关键行业软件的发展需求，也不可避免地要承受很高的安全风险。另一来源是获得业界认可的开源编译器，如GCC和LLVM，通过对其限定或改造（如关闭某些优化选项、限定版本、改造前端对语言特性进行约束、增加某些静态检查功能、以及插入运行时检查代码，等等）来适应行业内部的安全性需求。然而，这些开源编译器往往十分庞大（有成百上千万行代码），其实是另类的不能自主可控。实际上，仅编译器自动测试工具Csmith（XuejunYang等）截至2011年2月，以及EMI/SPE（Zhendong Su等）截至最近，就发现了GCC和LLVM的共计近1700个编译错误。从国家发展大局考虑，这两种选择均不是解决根本问题之路。如此困境，是我国软件业的发展长期以来严重失衡的结果，不止编译器，重要的工具软件，国货几乎全无。积重难返，出路何在？若登高望远，或许能见几丝曙光，终获重生？

事实上，现行的（包括上面提到的）这些编译器，其正确性/可靠性保障基本上是采用大量的测试以及严格的软件过程管理来实现的，并不能杜绝“误编译”，一旦真出现这种情况，难免发生灾难性的后果。对编译器进行正确性验证，而不仅仅是测试，是解决问题的根本途径。最严格的验证手段莫过于采用形式化方法，近年来，有关编译器形式化验证的研究工作取得了长足的进步，达到了实用化水平，为未来新的工业标准制定奠定了强有力的基础。CompCert编译器是经过形式化验证的可信编译器的杰出代表。该编译器将C的一个重要子集Clight翻译为PowerPC汇编代码（后来也支持IA32和ARM后端，目前已扩展至可支持64位处理器），其编译过程划分为多个阶段，每个阶段的翻译正确性都借助证明辅助工具Coq进行了证明，且这些证明可由独立的证明检查器检查，这是迄今最强的形式化验证手段，达到了人们所能期望的最高可信程度。Xuejun Yang等关于Csmith的研究工作表明：CompCert在正确性方面的表现明显优于常用的开源或商用C编译器。因CompCert编译器的杰出成就，其主要设计者Xavier Leroy获得了2016年度的十年前最有影响POPL论文奖(Most Influential POPL Paper Award)。

相对CompCert所采取的直接对翻译过程进行验证的方法，编译器验证的另外一种重要方案是翻译确认(translation validation)，由Amir Pnueli 等于1998年首先提出。翻译确认的方法不是直接验证翻译程序，而是用统一的语义框架为翻译过程的源和目标代码建模，两个模型之间定义一种特定的语义等价关系/模拟等价关系，设计一种可自动证明二者等价性的确认程序（返回成功与否，成功时或给出证明脚本，不成功时或给出反例）。根据不同的语义模型，确认程序可以通过自动求解或证明、符号计算、模型检查、静态分析等方式来实现模型间的等价性确认。

对比直接对翻译过程进行验证和翻译确认，两种方案各有利弊。前者是一种比较完美的解决方案，原理上可以保证源程序的一般性质都可以保持到目标程序，然而其缺点是难以扩展，一旦编译过程有所变化，证明脚本就可能需要大范围修改。翻译确认的方法只对编译器各翻译阶段的输入和输出代码作检查，而不关心编译过程的具体实现，因而具有较好的可重用性。然而，因确认程序本身是编译器的一部分，它必须是一个自动化的过程，这从理论上决定了它可能出现误报(false alarm)，从而使程序员无所适从。如果翻译过程仅限于实现某种代码优化，则产生的误报可以不反馈给程序员，取消相应的优化即可，这种情况对程序员的体验影响不大。实际上，根据各个翻译步骤的不同特点，将这两种方案混合使用是十分有益的做法，比如主体翻译过程采用直接验证，而优化过程采用翻译确认。

从应用角度看，CompCert编译器无论从源语言（C语言子集）大小，还是从目标代码质量，均可满足多数嵌入式应用系统的软件需求。最近几年，不断有基于CompCert的翻译确认工作，实现了更多的优化算法。这些工作在改进CompCert性能的同时，还有一个值得关注的共同特点，就是对确认程序也进行了严格的形式化验证，能够确保不出现误报，可达到与验证整个翻译过程同样的效果。当然，不像这些基于CompCert的翻译确认，已有的许多翻译确认工作，并不容易对确认程序进行严格的形式化验证，但这并不妨碍其实际应用。目前已有许多针对GCC和LLVM的翻译确认工作，对于进行确认的优化算法来说，误报率多在5%以下，某些优化甚至达到0.01%。试想，如果我们在怀疑某项GCC优化是否会带来安全隐患而犹豫是否将其关闭时，完全可以考虑实现一个低误报率的确认程序，没误报就实施优化算法，有误报就关闭（不做）该项优化。

下面介绍我们自己在编译器形式化验证方面的工作，一款基于Lustre的语言到C语言的可信编译器L2C的研发。

传统的常规语言，如C语言，一直以来是安全关键领域中使用最为普遍的开发语言。人们为安全有效地使用C语言下了很大功夫，积累了非常丰富的经验。尽管用各种办法来使基于C语言的系统开发更加安全高效，但毕竟C语言程序层次较低，不易使人们聚焦于问题本身，开发效率受到很大影响，并且也难于验证，于是基于模型/模型驱动的开发逐步兴起并成为业界主流，由模型自动生成的代码（C代码为主）占比已据主导地位。比较著名的建模语言/工具如Simulink，Scade等。

有一类建模语言称为同步语言，特别适合于实时控制系统的开发。所有同步语言均遵循同步假设，即每个周期内的计算（从输入值得到输出值）都是瞬间完成的。另外，同步语言的语义被要求具有确定性。同步假设以及确定性可以极大地简化实时系统的验证。Esterel，Argos，Lustre和 Signal是几种有代表性的同步语言。其中，Esterel是命令式语言，Argos 是基于并行和分层自动机的图形化语言；Lustre和Signal是陈述式语言，具有数据流特征，常称为同步数据流语言。Lustre是函数风格的语言，而Signal是关系型的语言。这些同步语言各自的特点有利于进行一些实质性的静态检查甚至于形式化分析和验证，从而有益于产生安全的代码。在基于同步语言的开发工具中，最著名的是Scade，其代码生成器KCG将一种基于Lustre的建模语言翻译到C语言，KCG应该是获得民用航空软件生产许可（DO-178B/C）的第一个商用代码生成器。目前，Scade工具已渗透到我国航空、航天、轨道交通及核电等安全关键领域。

与C语言编译器的情形类似，人们同样不会止步于像Scade这样的安全级代码生成器。基于高级建模语言代码生成器的形式化验证近年来已受到极大关注。Amir Pnueli 等首提翻译确认方法时，就是以Signal作为示范例子，即编译器源语言是同步语言Signal，目标语言是C。近年来，Van Chan Ngo和Jean-Pierre Talpin等基于翻译确认的思想进一步开展了Signal到C的编译器验证工作，特别是在时钟特性的保持方面取得了很好的进展。同时，也有人基于翻译确认的方法研究Simulink代码生成器的形式化验证。

当然，更理想的方法是像CompCert那样对翻译过程本身进行验证，法国的Marc Pouzet项目组以及我们的L2C项目组，基于这种方法开展了Lustre代码生成器形式化验证的工作。前者将一种具有Lustre语言关键特征的小语言MiniLS，翻译至一种基于对象的中间语言，采用Coq构造其核心翻译过程并进行正确性证明。最近，Timothy Bourke等在这一工作基础上，开展了将这一中间语言翻译至Clight（见CompCert项目）的验证工作，实现了相应的原型系统。L2C项目正式启动于2010年9月，致力于基于Lustre的语言到C语言的可信代码生成器（或称L2C编译器）的研发，从一开始便以Clight作为目标语言，从而与CompCert实现对接。L2C项目组创立时主要是面向国内核电领域的实际需求，分别于2013年6月和2015年4月完成两个版本的验收，在合作伙伴（国内某核电企业）研制的自主核级数字化仪控平台中得到应用，后者已完成阳江5号机组和石岛湾高温气冷堆示范工程核级DCS设备的交付并确定将在华龙一号示范工程的多个机组中应用，取得了良好的经济和社会效益。

除了可用于国内核电领域的版本，目前L2C编译器也正在研发开源版本。如果条件允许，L2C项目后续发展规划主要考虑满足国内关键行业（核电、航空、航天、轨道交通等）需求的通用可信编译器以及相关配套工具（静态分析/仿真/调试/WCET分析/图形语言等）。与著名的Scade工具相比，L2C编译器在成熟度以及源语言表达能力方面有所欠缺。但从形式化方法应用的角度来看，二者各有千秋。Scade基于模型检查实现了较强的源程序静态分析功能，这是L2C目前尚未涉足的。L2C基于定理证明对完整的代码生成过程进行了形式化验证，而Scade代码生成器的可靠性保障则一直依赖于测试与过程管理等传统方法。从目前的实际效果来看，L2C项目的实施结束了Scade在合作企业（之前也是Scade客户）的业务渗透。

说到这里，可以回过来思考一下前面提到过的问题，即国产核心工具软件的发展之路何在？仅就安全关键领域的编译或代码生成工具而言，要想与国外这一轮发展了几十年的商业产品（风河、绿山、Scade、MATLAB/Simulink等）竞争，机会似乎很渺茫。那么下一轮乃至下下一轮呢？我国作为未来几十年里关键领域（比如核电）最大的市场，是不是应该一直任由外商定价，换回非自主可控且留有安全隐患的核心代码开发工具？形式化方法于编译器项目中的成功应用，无疑代表了一种未来新技术变革的趋势。工业界也早已意识到形式化软件开发的潜力，在一些安全关键领域的安全级软件开发标准中也逐步新增了形式化方法相关的目标或者相应的补充说明（如RTCA的DO-178C和DO-333）。虽然有关条款目前尚属于非强制的，但很赞同裘老师专稿中的一句话：未来某些标准强制性地要求严格证明，不是不可能的事情。工业界需要有一个慢慢适应的过程，但无论如何，我们应该早点作好准备。修正软件产业发展失衡的老路，刻不容缓！有谁能甘心在未来安全关键领域的新技术变革时代，在包括编译器在内的核心工具软件方面还继续受制于人呢？

（注：本文微信抬头图片源于 Xavier Leroy 的POPL2011 特邀报告。）