AdaCore Blog

When the RISC-V ISA is the Weakest Link

by Yannick Moy

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.

Posted in #Security    #SPARK    #RISC-V   

About Yannick Moy

Yannick Moy

Yannick Moy is Static Analysis Lead at AdaCore and co-director of the ProofInUse joint laboratory with Inria. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a product he presents in articles, conferences, classes and blogs (in particular Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.