Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts
Graniteは、決定論的なISAリーク契約とのトレース等価性を確立することによって、RTLプロセッサの機能的正当性と非リーク性の両方を検証する、モジュール式の基礎的な手法を導入し、それによって中間仕様を信頼コンピューティング基盤から排除するためのハードウェアとソフトウェアの証明の合成を可能にする。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
超高速のレースカーを造りたいと考えているとしましょう。驚異的な速さを実現するために、ターボチャージャーや予測ステアリング、そして次にどのカーブを曲がるかを推測するシステムを追加します。しかし、一つ問題があります。もし車のエンジンが、左に曲がっている時だけ特定の「ガチャン」という音を立てるのだとしたら、傍らで聞き耳を立てている巧妙なスパイは、その音だけであなたのルートをすべて突き止めてしまうかもしれません。コンピュータチップの世界では、これを「タイミング・サイドチャネル」と呼びます。長年、プログラマーは、秘密のデータを扱っているときでも、どのようなデータであっても全く同じ時間を要するようにコードを書こうと試みてきました。それは、まるで廊下を音を立てずに歩こうとするスパイのようなものです。しかし、チップがより高速でスマートになるにつれ、チップは意図せず、鏡をチェックするための急な停止や、加速のバーストといった、小さな予測不可能な「ノイズ」を生み出すようになりました。これによって、秘密が漏洩してしまうのです。この論文は、たとえあなたのコードが完璧であったとしても、ハードウェアそのものが、その鼓動のリズムを通じて秘密を漏らしているかもしれないという恐ろしい概念に取り組んでいます。
Graniteとして知られる研究者たちは、コンピュータチップが秘密を確実に守っていることを数学的に証明する新しい方法を構築しました。彼らは単に推測したりテストを実行したりしたのではなく、コンピュータがどのように振る舞うべきかという高レベルのルール（「命令セット」）から、微細なワイヤやトランジスタ（「RTL」）に至るまでを繋ぐ、厳密でステップバイステップの数学的議論を作成しました。彼らの主な成果は、チップのタイミングが、パスワードや暗号鍵のような秘密のデータではなく、ボタンが押されたことのような「公開されてもよい事項」のみによって決定されることを証明する方法です。彼らは、チップが正しく見えるから、あるいは標準的なテストに合格したからといって、単に信頼してよいという考えを明確に否定しています。この特定の種類の証明がなければ、隠れた漏洩はほぼ確実に存在するのだということを彼らは示しています。彼らは単にこれが機能すると示唆しているのではなく、FPGA向けに合成することに成功したプロセッサ設計に対して、これを形式的に証明しました。ただし、ポスト合成テストのためのフルシステムオンチップへの統合はまだ行われていません。
偉大なるチップ探偵物語
コンピュータプロセッサを、高級レストランの賑やかで混沌とした厨房だと考えてみてください。シェフたち（ハードウェア）は、顧客のために料理（プログラム）を準備しています。「命令セットアーキテクチャ（ISA）」は、メニューとレシピ本です。それは厨房に対し、「ハンバーガーの注文が入ったら、最終的には必ずハンバーガーを提供しなければならない」と伝えます。しかし、メニューにはハンバーガーを作るのにどれくらいの時間がかかるのか、あるいはシェフがいつナイフを掴むのかまでは書かれていません。
昔は、シェフたちは「定時間（コンスタントタイム）」であるよう指示されていました。これは、顧客がサラダを注文しようがステーキを注文しようが、野菜を切る速度を全く同じにする必要があるという意味でした。そうすることで、窓の外から覗いているスパイが、包丁の刻むリズムから何を調理しているのかを察知できないようにするためです。しかし、その後、厨房はあまりに速くなりすぎました。シェフたちは「投機（スペキュレーション）」を使い始めました。つまり、注文が確定する前に、顧客が何を欲しがるかを予測して玉ねぎを切り始めるのです。もし予測が外れたら、玉ねぎを捨てて最初からやり直します。この推測ゲームは、新たな、偶発的なノイズを生み出しました。間違いに気づくまでの時間や、特定のスパイスを掴むまでの時間が情報を漏らし始めたのです。スパイは厨房の音を聞いて、「ああ、シェフが0.0001秒躊躇した。きっと秘密の玉ねぎを使った料理を作っているに違いない！」と推測できてしまうのです。
ここに、究極の厨房検査官であるGraniteが登場します。Graniteは単にシェフを見守るだけでなく、情報の漏洩を防ぐために厨房のルールを書き換えます。
「シャドウ・シェフ」のマジック
Graniteの天才的な点は、「シャドウ・シェフ（影のシェフ）」を用いた巧妙なトリックにあります。想像してみてください。秘密のレシピ（秘密のデータ）を知っている本物のシェフがいます。そして、目隠しをされ、注文の公開部分（公開データ）のみを知っているシャドウ・シェフがいます。
Graniteの手法はこう言います。「本物のシェフとシャドウ・シェフが、完璧に足並みを揃えて動いていることを証明する」。もし本物のシェフが、玉ねぎが大きかったために玉ねぎを切るのに5秒かかったとしても、シャドウ・シェフもまた、玉ねぎが大きいことを知らないにもかかわらず、正確に5秒かかる必要があります。シャドウ・シェフのタイミングは、公開された注文のみによって駆動されます。もし本物のシェフのタイミングが秘密（例えば玉ねぎの種類）に依存する場合、二人のシェフは同期が崩れ、証明は失敗します。
これを実現するために、Graniteは「ドライバー（Driver）」と「ウィットネス（Witness）」を導入します。
- ドライバーは、公開された注文のみを聞くメトロノームのようなものです。それは厨房がいつ前進すべきかを決定し、厨房の動作のタイミングが、顧客が知られることを望んでいる事項（公開データ）によってのみ決定され、秘密の材料には依存しないことを保証します。
- ウィットネスは、厨房の乱雑で予測不可能な部分（熱いフライパンのせいで発生するランダムな遅延など）のプレースホルダーです。ウィットネスはこう言います。「よし、ここでは具体的に何が起きても構わない。ただし、それが秘密に依存していない限りはね」。
実物の厨房が、ドライバーとウィットネスによって運営される厨房と全く同じように振る舞うことを証明することで、Graniteは、厨房のリズム（タイミング）が秘密の材料を漏らすことはあり得ないことを証明するのです。
モジュール式のパズル
厨房全体をチェックすることは非常に困難です。なぜなら、厨房は一度にすべてを見るには大きすぎるからです。Graniteは、厨房を小さく独立したステーション（切るステーション、焼くステーション、盛り付けステーション）に分割することで、この問題を解決します。
Graniteは、各ステーションが単独で安全であることを証明します。例えば、「乗算（マルチプライヤー）」ステーション（計算を行う場所）については、もし二つの数字を掛けるのに時間がかかる場合、それがゼロであること（これは既知であってもよい事項）によるものなのか、それとも秘密の値によるものなのかを確認し、安全であることを保証します。すべてのステーションが安全であると証明されたら、Graniteはそれらをレゴブロックのように組み立てます。この証明は「モジュール式」であるため、もし「焼くステーション」をより速いものに入れ替えたとしても、厨房全体を再チェックする必要はありません。新しいステーションだけをチェックすれば、システム全体が安全であり続けるのです。
最終判定
研究者たちは単に理論を述べただけではありません。彼らはプロセッサ設計を構築し、その上で証明を実行しました。彼らは、すでに「定時間」であることが知られているソフトウェア（Salsa20と呼ばれる暗号プログラム）を取り上げ、それが彼らのプロセッサ設計上で動作する際、タイミングを通じて一切の秘密を漏らさないことを証明しました。
これは、信頼すべき対象の定義を変える大きな出来事です。通常、ソフトウェアとハードウェアの間の複雑な契約を信頼する必要があります。しかし、Graniteは、彼らのハードウェアの証明を検証済みのソフトウェアの証明と結びつければ、ハードウェア・ソフトウェア間の契約自体を「信頼すべきリスト」から排除できることを示しています。ただし、この証明は依然として、命令セット・コントラクトの形式的な定義や、コードをハードウェア記述に翻訳するツールといった、いくつかのコアコンポーネントに依存しており、これらは引き続き「信頼できるコンピューティング基盤（TCB）」の中に残ります。彼らは自分たちの設計の中にさえバグを発見しました。特定の制御スイッチ（CSR）への書き込みが情報を漏らす可能性があることに気づき、証明が完了する前にそれを修正したのです。
要約すると、Graniteは、高速化し、予測を行い、ノイズを発している最中であっても、数学的に秘密を守ることが保証されたコンピュータチップを構築するための新しい方法です。それは、現代のコンピューティングにおける混沌とした騒々しい厨房を、静かで秘密を守る要塞へと変え、スピードとセキュリティを同時に実現できることを証明しています。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。