查看原文
其他

NVIDIA 安全团队:如果我们停止使用 C 会怎样?

CSDN 2022-11-11

整理 | 朱珂欣       责编 | 张红月
出品 | CSDN(ID:CSDNnews)

近日,在 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

— 推荐阅读 —

☞涉及上千人,人均71万补偿,扎克伯格承认因决策失误致Meta首次大规模裁员
Adobe将对上万种颜色收费:每月50元,否则文件变黑;Meta被裁员工将至少获71万补偿;C# 11 正式发布|极客头条
程序员将两台 40 年前的电脑改造成了手风琴,还能弹奏!

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

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