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/