近日，在 AdaCore 上一篇关于 NVIDIA 正尝试使用 SPARK 语言取代 C 语言的案例研究，引发了大家关注。

本次案例研究聚焦于 NVIDIA 面对网络安全问题时存在的挑战，并尝试使用 SPARK 语言实现一些对安全较为敏感的应用程序或组件。同时，还说明了 NVIDIA 在关键组件开发中加大对 SPARK 的使用的方法，以及 NVIDIA 通过采用 SPARK 获得的好处及对潜在 SPARK 采用者的建议。

图源：AdaCore 官网截图

安全性几乎无法通过测试来验证

NVIDIA 软件安全副总裁 Daniel Rohrer 曾坦言：“安全性是几乎无法通过测试来验证的。“随后，NVIDIA 安全团队开始寻找方案来应对日益恶劣的网络安全环境，并质疑过往的软件开发和验证策略，也意识到面向测试的软件验证，根本无法确保安全性。

Daniel Rohrer 还表示：“希望强调可证明性作为首选的验证方法，而不是测试。”

值得庆幸的是，可以从数学的角度，依托数学计算和形式证明代码的行为完全符合其规范，也因此使 NVIDIA 开始研究了 SPARK 。

从 C 转换为 SPARK 的原因：安全性和稳健性得到重大改进

SPARK 作为一种编程语言和一套验证工具，可以满足高保证软件开发的需求。SPARK 基于 Ada，既能对语言进行了子集化以删除无法验证的功能，又能扩展合同和方面的系统以支持模块化的形式验证。

早在 2018 年， NVIDIA 就进行了概念验证 （POC） 演习。在短短三个月内，两个安全级别较低的应用程序上实现了从 C 到 SPARK 的迁移。

在对投资回报评估后， NVIDIA 安全团队得出结论：伴随着培训、实验、新工具等新技术的提升，应用程序安全性和验证效率的也得到了提高。两个应用程序，在安全性和稳健性两个方面的重大改进。

由于 POC 的结果验证了最初的策略，SPARK 的使用也在 NVIDIA 内部迅速传播。现有的 50 名经过专业培养的开发人员在 SPARK 中实现了大量组件，许多 NVIDIA 产品现在都附带了 SPARK 组件。

网友：性能与 C 相比，没有看到任何性能差异？

然而，在 Hacker News 上，关于 NVIDIA 安全团队正尝试用 SPARK 语言取代 C 语言的案例，也引发了大家激烈的讨论：

• “相信如果我们摆脱了 C 语言，所有软件安全问题都会得到解决”；

• “有许多 C 语言开发人员会坚持认为他们已经获得了足够的经验，永远不会编写易受各种内存安全漏洞攻击的代码”；

• “性能与 C 相比，我根本没有看到任何性能差异”。

未来，SPARK 还将给 NVIDIA 及其客戶提供哪些保证，我们拭目以待。

参考链接：

https://www.adacore.com/papers/nvidia-adoption-of-spark-new-era-in-security-critical-software-development

https://blog.adacore.com/nvidia-security-team-what-if-we-just-stopped-using-c

https://news.ycombinator.com/item?id=33504206

《新程序员001-004》全面上市，对话世界级大师，报道中国IT行业创新创造！

☞前 Twitter 工程师爆料：“2015 年，我曾被要求构建一个最不道德的东西！”
☞“放弃科技公司 CEO ，我选择辞职做了仓库搬运工！”
☞做操作系统最重要的是生态