When the RISC-V ISA is the Weakest Link
source link: https://blog.adacore.com/when-the-isa-is-the-weakest-link
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
When the RISC-V ISA is the Weakest Link
by Yannick Moy – Sep 02, 2021
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.
About 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 blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK