Spectre対策、設計段階でテストするツール「AMuLeT」──3時間で9件のバグを見つけた中身

CPUの投機的実行を悪用してメモリの中身を盗み見る「Spectre」攻撃への対策は、これまで複数のハードウェア設計が提案されてきたが、その多くが後になって「実は安全ではなかった」と判明する経緯を辿ってきた。トロント大学などの研究チーム(Bo Fu、Leo Tenenbaum、David Adler、Assaf Klein、Arpit Gogia、Alaa R. Alameldeen、Marco Guarnieri、Mark Silberstein、Oleksii Oleksenko、Gururaj Saileshwar)がarXivに公開した論文「AMuLeT」は、この「後になって破られる」問題を、対策がチップとして完成する前の設計段階、マイクロアーキテクチャシミュレータの中で検出できるようにするツールだ。

3行まとめ

1. AMuLeTは、投機的実行の情報漏洩を検出できる既存のモデルベース関係テストツールを、実チップではなくマイクロアーキテクチャシミュレータに応用した、この種として初めてのツール
2. 素朴な設計と比べてテストのスループットを10倍以上高速化し、限られたテスト予算の中で脆弱性を見つけやすくする工夫を導入している
3. 2018〜2024年の4つのSpectre対策(InvisiSpec・CleanupSpec・STT・SpecLFB)を対象に大規模テストを実施し、3時間以内に既知のバグ3件・未知のバグと脆弱性6件、計9件を発見した。SpecLFBについてはオープンソース実装が安全でないことも初めて示している

なぜ「設計段階」でのテストが必要なのか

論文の背景説明は、既存のSpectre対策が抱えてきた問題を次のように述べている。

In recent years, several hardware-based countermeasures proposed to mitigate Spectre attacks have been shown to be insecure. To enable the development of effective secure speculation countermeasures, we need easy-to-use tools that can automatically test their security guarantees early-on in the design phase to facilitate rapid prototyping.

(近年、Spectre攻撃を緩和するために提案された複数のハードウェアベースの対策が、安全でないことが示されてきた。効果的な安全な投機実行対策の開発を可能にするには、設計段階の早い時期に、その安全性の保証を自動的にテストできる、使いやすいツールが必要だ)

これまでのSpectre対策の検証は、多くの場合チップが実際に製造された後、あるいは少なくとも詳細なRTL実装が完成した後に行われてきた。この段階で脆弱性が見つかると、修正のコストは非常に高くつく。AMuLeTは、この検証をより早い設計段階に前倒しすることを目指している。

仕組み:実チップ向けのテスト手法をシミュレータに応用

論文が説明するAMuLeTの基本的なアイデアは、既存の検証技術の転用だ。

This paper develops AMuLeT, the first tool capable of testing secure speculation countermeasures for speculative leakage early in their design phase in simulators. Our key idea is to leverage model-based relational testing tools that can detect speculative leaks in commercial CPUs, and apply them to micro-architectural simulators to test secure speculation defenses.

(本論文はAMuLeTを開発する。これは、投機的な情報漏洩に対する安全な投機実行対策を、設計段階の早い時期にシミュレータの中でテストできる、この種として初めてのツールだ。私たちの鍵となるアイデアは、市販のCPUにおける投機的な情報漏洩を検出できるモデルベースの関係テストツールを活用し、それをマイクロアーキテクチャシミュレータに適用して安全な投機実行対策をテストすることだ)

実チップに対して使われてきた検証手法を、まだ物理的に存在しないシミュレータ上の設計に適用する際には、いくつかの技術的な壁があったと論文は述べている。

We identify and overcome several challenges, including designing an expressive yet realistic attacker observer model in a simulator, overcoming the slow simulation speed, and searching the vast micro-architectural state space for potential vulnerabilities.

(私たちは、シミュレータの中で表現力がありながら現実的な攻撃者の観測モデルを設計すること、シミュレーション速度の遅さを克服すること、潜在的な脆弱性を求めて広大なマイクロアーキテクチャの状態空間を探索すること、といった複数の課題を特定し克服した)

シミュレーション速度の遅さへの対策として、論文は「素朴な設計と比べて10倍以上のテストスループット向上」を達成したとしている。

4つの対策を3時間でテスト、9件のバグを発見

論文が報告する実験結果は次の通りだ。

Using AMuLeT, we launch for the first time, a systematic, large-scale testing campaign of four secure speculation countermeasures from 2018 to 2024--InvisiSpec, CleanupSpec, STT, and SpecLFB--and uncover 3 known and 6 unknown bugs and vulnerabilities, within 3 hours of testing. We also show for the first time that the open-source implementation of SpecLFB is insecure.

(AMuLeTを使い、私たちは2018年から2024年までの4つの安全な投機実行対策──InvisiSpec、CleanupSpec、STT、SpecLFB──に対する、体系的かつ大規模なテストキャンペーンを初めて実施し、3時間のテストで既知のバグ3件・未知のバグと脆弱性6件を発見した。また、SpecLFBのオープンソース実装が安全でないことも初めて示した)

対象になった4つの対策は、2018年(InvisiSpec)から2024年(SpecLFBとみられる)までの間に提案されたもので、いずれも学術的に発表された正式なSpectre対策案だ。それらに対して、わずか3時間のテストで合計9件の問題を検出できたという結果は、既存の検証プロセスがどれだけの見落としを残してきたかを示す数字とも読める。ただし、この「3時間」がどのような計算資源(CPU数・並列度)を前提にした時間なのかは、抄録には明記されていない。

ASPLOS 2025に採択、5機関の共同研究

arXivの抄録ページには「Comments」欄があり、"To be published in Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'25)" と記載されている。この記載に加えて、ASPLOS 2025の公式プログラムページ(asplos-conference.org)にも「AMuLeT: Automated Design-Time Testing of Secure Speculation Countermeasures」の論文タイトルと著者一覧が掲載されているのを確認した。つまりASPLOS 2025(コンピュータアーキテクチャ分野のトップカンファレンスの一つ)に採択された論文であることは、arXiv側のメタデータと学会の公式プログラムの両方で裏が取れる。

ASPLOS公式プログラムには著者の所属機関も記載されており、5つの機関にまたがる共同研究であることがわかる。

Oleksii OleksenkoがMicrosoftのAzure Researchに所属している点は、この研究がアカデミアだけでなくクラウドベンダーの投機的実行対策の実務にも接点を持つ可能性を示している。なお、arXivのSubmission historyによれば、この論文は2025年2月28日に初版(v1)が投稿されている。

GitHubに実装コードが公開されている

著者の一人Gururaj SaileshwarのWebサイト(gururaj-s.github.io)には、AMuLeTの発表資料一式へのリンクが掲載されており、その中に実装コードを公開しているGitHubリポジトリ「sith-lab/amulet」へのリンクがある。GitHub APIで取得したリポジトリのメタデータは次の通り。

主要言語がAssemblyになっている点は、AMuLeTがシミュレータに対して投機的実行のテストケースを直接アセンブリレベルで生成・投入する実装であることを示唆している。ただしこれはGitHub側の言語判定(バイト数ベースの自動集計)に基づく推測であり、リポジトリ内のコード自体を読んで確認したわけではない。スター数10・フォーク数3は、2025年1月の作成から2026年8月時点でまだ広く使われるツールとしては認知が広がっていない規模感であることも付け加えておく。

著者の重なりが示す研究の連続性

この論文の著者の一人であるGururaj Saileshwar(トロント大学)は、当サイトで先に扱ったNVIDIA GPUのECC保護を破る「GPUThor」や、DDR5のRowhammer対策PRACの欠陥を指摘したQPRACにも名を連ねている。AMuLeTはRowhammer(DRAMの物理的欠陥)ではなくSpectre(CPUの投機的実行を悪用した情報漏洩)を扱っており、攻撃対象の物理層は異なるが、「ハードウェアレベルのセキュリティ対策の欠陥を、体系的なテストで暴く」という研究のアプローチは共通している。

論文本文とコードの中身は読んでいない

ASPLOS 2025への採択と著者所属は、arXivのComments欄・ASPLOS公式プログラム・著者本人のWebサイトという3つの独立したソースで確認できた。しかし、この記事が一次ソースにしているのはarXivの抄録・メタデータと、GitHub APIが返すリポジトリの統計情報(スター数・言語・日付など)までで、論文本文のPDFとGitHub上の実装コードそのものは読んでいない。そのため、AMuLeTの攻撃者観測モデルの具体的な設計、4つの対策それぞれで見つかった9件のバグの技術的な中身、SpecLFBのオープンソース実装が安全でない理由の詳細は確認できていない。発表スライド(gururaj-s.github.ioからリンクされているPowerPointファイル)も、本記事では開いていない。

自分自身はCPUのマイクロアーキテクチャ設計やSpectre対策の実装に関わったことがなく、この記事は論文抄録・カンファレンスの公開情報・GitHubのメタデータの読み込みのみに基づいている。

感想・指摘はコメント欄へ。