和Rust一样好，编程更安全？三年实践、员工态度反转，英伟达用 SPARK 换掉 C

近日，知名编程语言 Ada 与 SPARK 所属公司 AdaCore 表示，英伟达的产品运行着许多经过正式验证的 SPARK 代码。对于安全较为敏感的应用程序或组件，英伟达安全团队正在用 SPARK 语言取代 C 语言。

在将 SPARK 模块与 C 中的等效模块进行了比较后，英伟达首席软件工程师 Cameron Buschardt 表示，SPARK 生成的程序集几乎与 C 代码中的程序集相同，“我根本没有看到任何性能差异。”

英伟达虽以 GPU 闻名，但也参与嵌入式系统，并为 GPU 本身编写固件。这是安全关键代码。安全对英伟达至关重要，但当前的网络环境并不安全：针对固件和硬件的网络攻击呈上升趋势，但开发和验证生态系统没有跟上这些攻击的规模，同时全行业缺乏安全代码设计人员和软件安全从业人员。这些让英伟达面临着既要提供更安全的产品⼜不会⼤幅增加开发时间和成本的挑战。

在全面审视自家软件开发方法后，英伟达思考哪些方面还需要改进，也因此英伟达开始注意到在开发关键嵌入式应用程序时，使用传统语言和工具集所带来的相应成本：

多年以来，嵌入式应用程序的开发仍然广泛使用 C 和 C++。但这些语言已有数十年历史，语言自身相对陈旧、不少分析工具无法正常适用，C 和 C++ 的规范也有不少歧义。如果无法明确验证，开发者永远不知道特定代码模块何时算是测试通过。这不仅令安全保证无从谈起，更难以量化权衡项目进展。

英伟达软件安全副总裁 Daniel Rohre 坦言，“我们还是喜欢可量化的结果。”不过如何把这样一个难以量化、甚至不知道是否最终完成的问题，转化成能以数字衡量的明确答案，是摆在英伟达软件安全团队前面的一大难题。

在查看了各种可实现量化的方法后，团队很快意识到不少方案需要依托于数学计算和形式证明，这类工具在过去十年间还发生了重大变化。

“我们希望接下来的验证以可证明性作为起点，而不再满足于‘已经测试过了’。安全性是几乎无法测试验证的，因为根本就没有终极可靠的标准。”Rohrer 表示，而形式证明则带来了强大的吸引力，能帮助英伟达确信其产品中不存在运行时错误和其他一些常见安全漏洞，且程序功能符合既定规范。

“我们能不能调整基本方法？如果可以，具体要使用哪些工具？”这些问题，就成了软件安全团队接下来的工作重点。

作为回应，安全团队给出的答案在 Rohrer 看来颇为“离经叛道”：如果我们不再用 C 语言，结果会如何？于是新的问题又冒了出来：还有哪些替代语言和工具，可以支持这些形式化方法？

在追寻答案的过程中，英伟达发现了 SPARK。

SPARK 是一种高级计算机编程语言，由定义明确的 Ada 子集组成。与之前的 Ada 一样，SPARK 就是为开发高完整性软件而生，强调以可预测且高度可靠的状态运行。SPARK 还提供一种名为“契约”（contract）的语言特性，能够为组件指定适用于静态验证的形式方法。

英伟达首席软件工程师、首批 SPARK 用户之一 Dhawal Kumar 表示，“从编程语言功能的角度来看，这些范式跟 C 和 C++ 非常相似。SPARK 是一种命令式编程语言，可用于编写面向过程或面向对象的代码，也有不少大型编程工具可供选择。”

归功于其独特设计，SPARK 开发的代码中不会存在未定义的行为。该语言带有一组内置检查，能确保代码遵守所有规则，因此不会发生运行时错误（例如缓冲区溢出）。

SPARK 的另一个关键特性就是支持形式验证。换句话说，通过使用 SPARK 和形式方法求解器，即可在数学上证明我们的 SPARK 代码行为完全符合规范。这样的过程，就被称为形式验证。

Dhawal Kumar 解释道，“SPARK 具备大多数其他编程语言所没有的功能，即在代码本体内指定程序要求、并使用相关工具集来确保这种合规性。简单来讲，这就是证明程序正确无误的能力。这一点非常重要。”

总的来说，SPARK 最能吸引英伟达的优势包括：

• SPARK 具有确定性。也就是说，形式证明可以确切消除运行时错误、保障规范合规。

• SPARK 代码能够与 C 链接。就是说英伟达不必一次性重新编码所有内容或非关键组件。SPARK 组件能够被轻松集成至 C/C++ 环境当中，这样英伟达就能灵活选择需要把哪些部分转化为能够形式验证的 SPARK 形式。

• SPARK 拥有可靠的生态系统。SPARK 的根源语言 Ada 本身就非常成熟，而且自 1980 年代以来经历过多次升级。开发者可以通过 AdaCore（Ada 和 SPARK 的全球权威机构）及其他组织轻松获得一流支持工具。此外，Ada 和 SPARK 还拥有上游开源软件（OSS）。

2018 年第四季度，英伟达开展了概念验证（POC）演习，希望深入研究 SPARK 语言、相关工具和可用的技术支持，借此确认其是否总体适用于英伟达的应用场景。

在初始概念验证中，英伟达软件安全团队将 SPARK 引入了两款应用程序：其一是裸机应用程序，充当其他几块安全处理器上所运行代码的信任根；其二则是实时操作系统（RTOS）应用，负责处理保护区域的大小调整。

概念验证团队在三个月内将两套代码库的几乎所有代码都由 C 转换成了 SPARK。之后团队发现，两款应用程序的安全性和稳健性都有了重大改进。由于 SPARK 出色的稳健性，加上将程序属性表示为“契约”的设计，英伟达发现新程序能够大大减少安全介入需求。另外，开发团队实际上很容易适应这种新的语言和工具。

与安全评估员一道完成结果审查之后，英伟达还发现 SPARK 完全可以在安全环境下与 C 代码混合使用。更重要的是，安全评估员认为 SPARK 不仅表现过关，而且只要开发者接受过充足的培训，其在安全关键型应用程序中的表现甚至比 C/C++ 更优秀。

概念验证团队还根据测试结果评估了投资回报率（ROI），得出的结论是由 SPARK 转换带来的工程成本（培训、实验、新工具获取等）可以被应用程序的安全性和验证效率提升所抵消，因此转向 SPARK 将大有可为。

最后英伟达得出结论，SPARK 的支持基础设施非常出色。

概念验证完成之后，英伟达决定立刻将 SPARK 的成本节约与功能提升实践落地。从 2019 年开始，英伟达在其安全策略中为指定的固件使用 SPARK。与此同时，英伟达还开始培训更多 SPARK 开发人员，并最终建立起内部培训计划。随着公司内部 SPARK 专业知识的积累，语言转换成本将逐渐被抵消。

目前，多个英伟达团队正将 SPARK 引入众多应用程序，包括整体 GPU 固件镜像、BootROM 和安全监控程序固件中的镜像身份验证与完整性检查，以及用于嵌入式操作系统的隔离内核中的形式验证组件等等。

总体来看，目前的改造目标仍然是体量较小的代码，但这也是 SPARK 强类型、无运行时错误且在某些情况下可实现严格形式验证等优势的绝佳场景。

另外在量化采用 SPARK 带来的好处方面，英伟达的工程经理们纷纷表示，SPARK 提供的理论保证帮助他们增强了对产品质量的信心。

英伟达公司 GPU 软件安全高级经理 James Xu 的团队的职责是，确保英伟达 GPU 中的软件和固件处于行业领先的安全水平。

Xu 解释称，“我们之所以使用 SPARK，主要原因就是它能提供严格保证。其中一大关键价值就是不存在运行时错误。要知道，能相信自己的代码可以直接回避掉大多数常见陷阱，这可是很有吸引力的。在使用 SPARK 编码时，我们往往更有信心，因为这种语言本身就能防止人们犯下 C 语言编程时一些常见的错误。”

作为英伟达 GPU 固件安全团队负责人，Varun Kumar 的团队负责 GPU 组件的初始化和启动、安全引导、固件更新以及设备恢复证明等。如今 Kumar 带领着 20 名工程师按照 NIST SP800-193 平台固件弹性指南开发 SPARK 组件。他表示，Xu 提到的这些特性对于他们这些客户安全保障人士也很有吸引力。

与 James Xu 和 Varun Kumar 团队使用 SPARK 开发新组件不同，Cameron Buschardt 的主要工作是用 SPARK 编写出与 C 版本等效的模块。从结果来看，SPARK 版既未出现代码膨胀、也不存在性能降级。他表示，“由 SPARK 编写成的程序集几乎跟 C 语言版本完全相同。我没有发现任何性能差异，而且因为所有属性都得到了严格证明，所以我们压根不需要启用运行时检查。”

虽然现在看着效果不错，但 SPARK 的推广工作起初并不顺利，不少开发者和工程经理对其多少是抵触的。James Xu 认为这些都源自于对未知的担忧，工程技术和行政管理团队都有各自担忧的事情。

“Ada 和 SPARK 在某些领域缺乏知名度，所以人们会担心未来会不会影响工程资源的扩展能力、会不会影响到开发计划、会不会很难得到可靠的技术帮助等。虽然消除运行时错误这点听起来不错，但真能在实践中落地吗？对于逻辑错误，SPARK 又有哪些优势？另外，考虑到对这种语言并不熟悉，人们天然会觉得从 C 到 SPARK 会严重拖慢开发进度。”

英伟达用事实回应了大部分质疑。在培训方面，英伟达最初直接使用 AdaCore 提供的课程，不久之后便开发出了自己的内部培训计划。很快，参与学习的开发者数量就迅速增加。

事实证明，语言转换带来的影响远不像想象中那么严重。

James Xu 当初曾猜测 SPARK 的开发周期可能是 C 语言的两倍。但后来他发现，只要保证只在隔离良好且规模较小（但更有价值）的范围内使用 SPARK，那实际影响就可以“几乎忽略不计”。Xu 还强调，“有些开发者还担心项目进度会大大减缓，甚至觉得预算可能会超支。但事实证明这都不是问题。

在亲眼目睹了 SPARK 和形式化方法对工作和客户关系产生的积极影响之后，很多此前抱有怀疑态度的工程师迅速转变成了热情的支持者。

“说实话，刚开始那会我也非常怀疑。我在 SPARK 中第一次尝试证明非平凡算法，结果简直糟透了。但在经历了初步学习之后，我又对 SPARK 那种严格的可证明性无比钦佩。”Cameron Buschardt 表示，“SPARK 不仅允许我们构建一个组件，还承诺帮我们证明它的完备性。这是一场变革，是其他任何语言都无法带来的至高信任。”

从怀疑到支持的英伟达工程师有很多。Rohrer 表示，只要大家愿意直面挑战、亲身尝试，那么在克服了最初的思维惯性之后，他们就会意识到转向 SPARK 确实具有打破传统的变革性意义。

参考链接：

https://www.adacore.com/uploads/techPapers/222559-adacore-nvidia-case-study-v5.pdf

https://devclass.com/2022/11/08/spark-as-good-as-rust-for-safer-coding-adacore-cites-nvidia-case-study/