NVIDIA 与 AdaCore 携手利用 Ada 和 SPARK 编程语言保护软件安全。
软件定义了是什么在促使我们移动。从移动应用程序和实时地图到日益自动化的汽车，代码行已成为交通领域的基础。
随着软件变得越来越复杂，出现人为错误的可能性也越来越大，从而带来更多潜在的安全风险。
为确保这款至关重要的软件安全无虞，NVIDIA 正与 AdaCore 开展合作，这是一家为极其重视安全的软件提供开发和验证工具的供应商。通过在特定的固件元素中实施 Ada 和 SPARK 编程语言，我们可以减少人为错误发生的可能性。
两种语言的设计都考虑到了可靠性、稳健性和安全性。将这两种语言用于编程可以提高验证代码有无问题和漏洞这一过程的效率。
咨询公司 VDC Research 的一项研究显示，对于航天和汽车等安全性、可靠性和安全标准较高的行业，通过增强软件验证，以下优势可以转而节省近 40% 的成本和时间。
提前发现缺陷
Ada 具有各种内置功能，可在软件生命周期早期检测代码缺陷。这样会减少人为错误发生的可能性，还会减少开发后进行额外的测试和同行评审流程的需求。
作为 Ada 的子集，SPARK 能够以数学方式证明使用该语言编写的代码是否无误。这一证明可定义软件应用程序的运行方式。它还可以确定该实现是否符合该定义，同时发现可能通过其他方式尚未检测到的错误或漏洞。
通过将这些语言集成到 NVIDIA 硬件中，软件发生故障或被利用的可能性可降至最低。这一验证过程可在开发周期中较快地进行，从而减少浪费。
软件定义的安全
将 Ada 和 SPARK 语言集成到 NVIDIA 平台等措施有助于改进汽车安全的稳健性，特别是在汽车日益自动化的情况下。
软件在功能上必须与运行该软件的硬件一样安全，并要接受同样严格的标准和专家评估。借助用于执行验证的语言，这一过程逐渐融入开发周期，从而创建更顺畅的评审周期。
NVIDIA 软件安全部门副总裁 Daniel Rohrer 说：“自动驾驶汽车很复杂，需要远超最严格标准的复杂软件。Ada 和 SPARK 为解决这个生态系统的关键需求带来了令人兴奋的可能性。”