NVIDIA尝试使用SPARK语言取代C语言

2022-11-08 13:11

出品 | OSC开源社区（ID：oschina2013)

知名编程语言 Ada 与 SPARK 所属公司 AdaCore 发布了一则关于 NVIDIA 的案例，案例显示：NVIDIA 的产品运行着许多经过正式验证的 SPARK 代码，NVIDIA 安全团队正尝试使用 SPARK 语言取代 C 语言，来实现一些对安全较为敏感的应用程序或组件。

SPARK 是一种编程语言和一组验证工具，旨在满足高保证软件开发的需求。SPARK 基于 Ada 语言，它既对 ada 语言进行子集化以删除无法验证的功能，又扩展了合约和方面的系统，进一步支持模块化、形式化验证。
SPARK 语言一般用于可预测和高度可靠操作的系统中的高完整性软件，它有助于开发需要高安全性或业务完整性的应用程序。

早在 2018 年， NVIDIA 就针对 “从 C 转换为 SPARK” 这一过程进行了概念验证 (POC) 练习，在三个月内将两个低级别的安全敏感应用从 C 转换为 SPARK 代码。在对投资回报进行评估后，该团队得出结论：随着新技术的增加（培训、实验、新工具等），应用程序安全性和验证效率也得到了提高，转换为 SPARK 代码的两个应用程序实现了安全稳健性的重大改进。

（有关评估结果的更多信息，请参阅 NVIDIA 的进攻性安全研究 D3FC0N 演讲：https://blog.adacore.com/when-formal-verification-with-spark-is-the-strongest-link）。

由于 POC 的结果证明从 C 转换为 SPARK 的可行性，SPARK 语言的使用在 NVIDIA 内迅速传播开来。现在已有超过 50 名受过专业培训的开发人员使用 SPARK 中实现了许多组件，且许多 NVIDIA 产品现在都附带 SPARK 组件。

另外，SPARK 有一项很有趣的特性：它可以代码本身中指定程序需求的能力，并使用相关的工具集来确保代码实现地功能与它的需求相匹配。NVIDIA 更多地使用 SPARK 来实现最关键的组件，确保它没有运行时错误，并确保它符合受信任根应用程序的规范。

此外，完整的案例研究涵盖了一些有趣的主题，比如与 C 相比，SPARK 的性能 “根本没有看到任何性能差异 “。

相关链接：https://www.adacore.com/uploads/techPapers/222559-adacore-nvidia-case-study-v5.pdf