🔥 热搜 🔥
百度今日热点微信公众平台贴吧opggdnf私服百度贴吧知乎dnf公益服百度傻逼
分类
社会娱乐国际人权科技经济其它
🔥 热搜 🔥
百度今日热点微信公众平台贴吧opggdnf私服百度贴吧知乎dnf公益服百度傻逼
分类
社会娱乐国际人权科技经济其它
查看原文
其他

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

OSC开源社区 2022-11-27
收录于合集
#开源 386 个
#编程语言 35 个
#代码 53 个
出品 | 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


【OSCHINA 2022 中国开源开发者问卷】来啦
你的反馈将有助于反映中国开源的全貌
问卷结尾还可抽取我们的周边好物哦~
期待来自你的反馈！

往期推荐



GitHub 被起诉

微软贡献Linux内核代码，可运行多个Windows

刚标准化就被废弃，谷歌：不爱了


这里有最新开源资讯、软件更新、技术干货等内容点这里 ↓↓↓ 记得 关注✔ 标星⭐ 哦~

您可能也对以下帖子感兴趣

文章有问题？点此查看未经处理的缓存