Joining forces to meet the toughest
safety and security demands.
AdaCore is partnering with NVIDIA™ to implement Ada and SPARK programming languages for select safety-critical firmware used in their next-generation embedded systems platforms. Customer using products such as NVIDIA® Jetson™ for embedded artificial intelligence (AI) computing, NVIDIA DRIVE™ AGX for autonomous vehicle (AV) development, and Isaac™ for Robotics are able to use the same technology at the application level. At the core of NVIDIA’s embedded systems is a system on a chip (SoC) that integrates an ARM architecture central processing unit (CPU), graphics processing unit (GPU), memory controller and IO paths onto one package. AdaCore’s GNAT Pro Ada and SPARK compilers can compile code targeting the ARM CPU embedded on NVIDIA SoCs, and increase verification efficiencies to achieve compliance with the functional safety standard ISO-26262. Supported compilation modes include bare metal as well as Linux or QNX OSes.
NVIDIA's Journey to Adopting SPARK
Companies are facing significant challenges in increasingly hostile cybersecurity environments. NVIDIA has responded to these challenges by addressing the scarcity of expert software security resources through strategic initiatives. One such pivotal move was NVIDIA’s decision to transition from C/C++ to SPARK for their security-critical software and firmware components. Our case study delves into this transformative journey, exploring the strategic decisions and outcomes that have reshaped NVIDIA's approach to software security.
Learn how NVIDIA tackled cybersecurity challenges by switching from C/C++ to SPARK, enhancing software security and reliability. This case study offers actionable insights for adopting SPARK to strengthen your defenses against cyber threats.
Read the case study now.
Download 2.998 MB pdfGenerates Code that is Formally Verified to be Free of Vulnerabilities
The Ada programming language and its SPARK subset combined with its toolset is a platform that allows developers to formally guarantee properties of source code, such as the 100% absence of certain categories of vulnerabilities (buffer overflow, division by zero, references to uninitialized variables, memory corruption), and to prove custom functional assertions.
Increases Critical Code Performance
SPARK and Ada provide performance levels and footprints similar to other system-level languages such as C. However, SPARK allows the removal of proven checks from the final binary, reducing the need for defensive code and allowing for safer and more efficient code execution.
Reduces Development Costs
The demand for cost-effective tools and methodologies has greatly increased in the automotive and industrial domains over the past few years. Using Ada and SPARK reduces the cost of developing safety and security-critical software by automating many verifications that would otherwise need to be done through manual code reviews or testing. It also allows the detection of potential issues early in the development process, reducing the amount of errors needing to be fixed in later stages. For industries that have strong safety, reliability, and security standards, like aerospace and automotive, these benefits can translate to nearly 40 percent cost and time savings from enhanced software verification, according to a study by VDC Research.
Integrates Easily with Existing C Code
SPARK Ada provides advanced language interfacing capabilities, in particular with C and C++. C and C++ header files can be converted to Ada header files and vice versa. Calls between the two languages can be made directly without any intermediate layer, linked in the same binary with no performance penalty. This allows the progressive introduction of a new language into existing codebases and processes. In addition, the GNAT Pro Common Code Generator (CCG) allows projects to cross-compile Ada and SPARK applications to any hardware target that provides a C compiler, including targets that do not come with off-the-shelf Ada support.
IEC 61508 and ISO 26262 Qualified
Developers need higher integrity software to increase verification efficiencies and achieve compliance with the functional safety standard ISO-26262. The SPARK and Ada compiler, as well as the corresponding formal verification tool, have been qualified at the highest level of ISO 262626 (TCL-3) as well as IEC 61508 (T-3 for the compiler and T-2 for the verification tool). All three products have also been certified by TÜV SÜD, an independent, globally recognized organization that confirms that products meet national and international standards. This qualification enables these tools to be used in the most critical environment in industrial and automotive domains and demonstrates our commitment to support industrial projects on their own path to adoption.
The TÜV SÜD certification mark is widely acknowledged and respected as a trusted symbol of quality, safety, and sustainability.
Masten Space Systems
How Masten Space Systems is Using Ada and SPARK to Land on the Moon’s South Pole
