本文是其中的一部分TechXchange:RISC V和TechXchange:Ada和火花
英伟达往往会大肆宣传其系统芯片(SoC)解决方案的机器学习(ML)能力驱动AGX欧林它的目标是汽车应用。安全处理器是包的一部分,但它们对安全的应用程序至关重要。
英伟达的安全支持使用的是定制处理器,但它正在转向RISC-V为未来实现。该公司并不是唯一采用RISC-V的公司。西部数据公司是利用的SiFive的RISC-V为其存储解决方案提供了全面的设计。NVIDIA目前还没有改变SoC的核心处理器。这些仍然是Arm Cortex核心,但安全处理器本质上是与系统的其他部分隔离的,它运行自己的固件。
固件不会用C语言编写。它正在被完成SPARK, Ada编程语言的可证明子集.Ada 2012新增合同SPARK利用了这一特性。它允许程序员指定细节,比如过程输入和输出的特征。然后,编译器可以将这些规则用于对过程的调用,以及如何使用结果。
契约支持使编译器能够证明一个过程做了它想要做的事情,并且调用和使用结果的代码将按照语言定义中的契约和隐式契约所指定的方式操作。隐式语言检查的一个例子是Ada对数组和字符串进行的范围检查。C和c++代码的最大问题之一是缓冲区溢出,这在Ada中是不可能发生的。
包含契约信息并允许编译器进行检查的好处是,它还可以删除许多通常与Ada相关的运行时检查,因为它们是不必要的。例如,如果已知数组的索引永远不能超过数组的大小,则可以从运行时删除隐式数组访问范围检查。
Ada在航空电子设备中的应用是众所周知的,但它也适用于任何嵌入式应用程序。它在医疗和汽车等安全应用中非常有用。尽管自动驾驶汽车的代码量通常会超过一架先进的战斗机,但它需要同等程度的审查,以提供安全可靠的操作。让编译器检查代码是否在做预期的事情,而不是让人检查代码来做同样的家务,这是很有意义的。
英伟达软件安全副总裁丹尼尔·罗勒(Daniel Rohrer)表示:“自动驾驶汽车极其复杂,需要复杂的软件,需要最严格的标准。”“采取一些措施,比如将Ada和SPARK语言整合到英伟达的平台上,可以提高我们汽车安全的稳健性和安全性。”
C和c++仍然是嵌入式编程的主要语言。然而,使用也有好处Ada和SPARK,包括在查看总拥有成本(TOC)时节省的成本.开源的版本Ada和SPARK工具以及在线培训都是可用的.
> >网站资源
..> >图书馆:TechXchange
. . . .>> TechXchange:嵌入式软件
. . . . . .>>主题:Ada和SPARK