After clicking “Watch Now” you will be prompted to login or join.


Click “Watch Now” to login or join the NVIDIA Developer Program.


Exterminating Buffer Overflows and Other Embarrassing Vulnerabilities with SPARK Ada on Tegra

Quentin Ochem, AdaCore

GTC 2020

Since 2018, NVIDIA has been actively investigating the SPARK Ada programming language to develop their most sensitive pieces of firmware. We'll explain how users of the NVIDIA hardware can also benefit from this language choice when developing applications for the Tegra SoC. The benefits of the technology, from a cyber security point of view, will be demonstrated through the use of formal methods, allowing trivial proof of properties, such as absence of buffer overflows. We'll describe using this technology on top of ARM processor cores, as well as methodologies for applications leveraging the GPU, either through existing libraries interfaces/CUDA code, or through an experiential port of Ada/OpenACC, which allows applications directly written in Ada or SPARK to offload to the GPU.

View More GTC 2020 Content