This article is part of TechXchange: RISC V and TechXchange: Ada and SPARK
A whitepaper on the use of SPARK by NVIDIA is available from Adacore.
Nvidia tends to hype the machine-learning (ML) capabilities of its system-on-chip (SoC) solutions like its DRIVE AGX Orin that targets automotive applications. Often lost in the mix is the security processor that is part of the package but these are critical to safe and secure applications.
Nvidia's security support has used a custom processor, but it's moving to RISC-V for future implementations. The company isn't alone in its adoption of RISC-V. Western Digital is taking advantage of SiFive’s RISC-V designs across the board for its storage solutions. NVIDIA isn't changing the SoC’s core processors at this point. These are still Arm Cortex cores, but the security processor is essentially isolated from the rest of the system and it runs its own firmware.
That firmware will not be written in C though. It is being done in SPARK, a provable subset of the Ada programming language. Ada 2012 added contracts to that language and SPARK takes advantage of this feature. It allows programmers to specify details like the characteristics of procedure inputs and outputs. The compiler can then enforce these rules for calls to the procedure as well as how the results will be used.
The contract support enables the compiler to prove that a procedure does what it is desired, and the code that calls and uses the results will operate as specified by the contracts and implicit contracts within the language definition. An example of the implicit language checking is the range checking done by Ada for arrays and strings. One of the biggest problems with C and C++ code has been buffer overruns, which can't happen with Ada.
The advantage of including the contract information and allowing the compiler to do the checking is that it can also remove many of the runtime checks often associated with Ada, because they are unnecessary. For example, the implicit array access range checks can be removed from the runtime if it's known that an index to the array can never exceed the size of the array.
Ada’s use in avionics is well-known, but it's also ideal for any embedded application. It can be extremely useful in safety applications like medical and automotive. Though the amount of code in a self-driving car will typically exceed that in even an advanced fighter jet, it will need the same level of scrutiny to provide safe and reliable operation. It makes a lot of sense to have the compiler checking that the code is doing what's desired rather than having humans do that same chore by examining the code.
“Self-driving cars are extremely complex and require sophisticated software that needs the most rigorous standards out there,” said Daniel Rohrer, vice president of Software Security at Nvidia. “Taking measures like incorporating Ada and SPARK languages into Nvidia platforms can improve the robustness and assurances of our automotive security.”
C and C++ remain the primary languages for embedded programming. However, there are advantages to using Ada and SPARK, including cost savings when looking at the total cost of ownership (TOC). Open-source versions of Ada and SPARK tools are available as well as online training.
>> Website Resources
.. >> Library: TechXchange
.. .. >> TechXchange: Embedded Software
.. .. .. >> Topic: Ada and SPARK