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

GTC 2020 S21122
Presenters: Quentin Ochem,AdaCore
Abstract
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.

Watch this session
Join in the conversation below.