AdaCore and NVIDIA partner on security-critical firmware

February 06, 2019 //By Ally Winning
AdaCore and NVIDIA partner on security-critical firmware
AdaCore is working with NVIDIA to implement Ada and SPARK for select firmware used for safety and security-critical applications.

NVIDIA is in the process of migrating some product lines to a new architecture using the RISC-V ISA. The company will also upgrade select security-critical firmware software, rewriting it from C to Ada and SPARK. These moves will increase verification efficiencies to achieve compliance with the functional safety standard ISO-26262.

Ada and SPARK are designed to help meet the most stringent software requirements for safety and security. The Ada programming language has built-in features that detect code defects early in the software life cyclet. The SPARK language — a restricted set of Ada features designed to perform a formal mathematical proof — increases the certainty of catching defects early that might not have been detected otherwise. SPARK facilitates static analysis that can formally demonstrate certain properties of the code, ranging from correct data flows and the absence of run-time errors such as overflow, to more advanced assertions and satisfaction of functional requirements.

More information

Related news

AdaCore joins RISC-V Foundation

Ada competition results show path to improved code quality - AdaCore

DO-178C/ED-12C Guidance from AdaCore, as handbook download

Adacore improves static analysis tool, supports more environments

Vous êtes certain ?

Si vous désactivez les cookies, vous ne pouvez plus naviguer sur le site.

Vous allez être rediriger vers Google.