NVIDIA has been using SPARK for some time now to develop safety- and security-critical firmware applications. At the recent DEF CON 29, hackers Zabrocki and Matrosov presented how they went about attacking NVIDIA firmware written in SPARK but ended up attacking the RISC-V ISA instead!

Zabrocki starts by explaining the context for their red teaming exercise at NVIDIA, followed by a description of SPARK and their evaluation of the language from a security attack perspective. He shows how they used an extension of Ghidra to decompile the binary code generated by GNAT and describes the vulnerability they identified in the RISC-V ISA thanks to that decompilation. Matrosov goes on to explain how they glitched the NVIDIA chip to exploit this vulnerability. Finally, Zabrocki talks about projects used to harden RISC-V platforms.

What I found amazing about this presentation is that because of the protection provided by the NVIDIA team’s developing the software in SPARK and proving it free of runtime errors, the hackers had to turn to something other than the software to find vulnerabilities - which led them to find one in the RISC-V ISA itself!

Zabrocki correctly pointed out that memory exhaustion issues are not detected by the SPARK tool, GNATprove. Instead, you should use, for example, GNATstack to detect (some of) them. This is a perfect example of non-functional requirements that are not checked by the SPARK tool. Other similar requirements include timing constraints for real-time software and robustness against cosmic rays for satellite software. Finally, note that SPARK supports safe pointers (an enhancement added in SPARK Pro 2020), and that the classes of problems detected by the tool are clearly defined in the tool documentation.