RISC-V ISAの脆弱性

NVIDIA社は、SPARKを使用して、安全性やセキュリティが重要なファームウェア(develop safety- and security-critical firmware applications.)を開発しています。DEF CON 29会議では、ハッカーZabrocki氏とMatrosov氏(Zabrocki and Matrosov)が、SPARKで記述されたファームウェアに対する攻撃方法(attacking NVIDIA firmware written in SPARK)を発表しました。結論として、ファームウェアではなくRISC-V ISAを攻撃することになりました。

Zabrocki氏は、まずNVIDIAでのレッドチーム活動(the context for their red teaming exercise at NVIDIA)について解説し、続いてSPARKの概説とセキュリティ攻撃の観点から言語の評価(their evaluation of the language from a security attack perspective)を行っています。Zabrocki氏は、Ghidraの拡張機能を使ってGNATが生成したバイナリコードを逆コンパイルする方法(extension of Ghidra to decompile the binary code generated by GNAT)を紹介し、その逆コンパイルによってRISC-V ISAに発見された脆弱性(how they glitched the NVIDIA chip to exploit this vulnerability)について述べています。さらにMatrosov氏は、この脆弱性を利用してNVIDIAチップにどのような細工を施したか(how they glitched the NVIDIA chip to exploit this vulnerability)を説明しています。最後に、Zabrocki氏は、RISC-Vプラットフォームを強化するためのプロジェクト(projects used to harden RISC-V platforms)について語っています。

この発表で驚かされることは、NVIDIAチームがSPARKを使用して、ソフトウェアにランタイムエラーが無いことを証明しています。 結果、ファームウェアは保護されています。そのため、ハッカーたちはソフトウェアの脆弱性を検出できず、RISC-V ISA自体の問題点の発見に至りました。

Zabrocki氏は、メモリの枯渇はSPARK/GNATprove検証ツール(memory exhaustion issues are not detected by the SPARK tool, GNATprove.)では検出できないことを指摘しています。代わりに、GNATstackを使用して問題点を検出する必要があります。これは、SPARKで検出できない機能要件と言えます。また、リアルタイムソフトウェアのタイミング制約や、衛星ソフトウェアの宇宙線に対する堅牢性などは検出できません。最後に、SPARK Pro 2020で追加された機能としてのポインタをサポート(an enhancement added in SPARK Pro 2020)、ならびに、ツールで検出される問題のクラスがツール内で明確に定義(the classes of problems detected by the tool are clearly defined in the tool)されています。

本資料は、AdaCore のブログを意訳したものです。正確な内容については、原文をご参照下さい。
原稿タイトル When the RISC-V ISA is the Weakest Link
https://blog.adacore.com/