大規模システム開発の問題 ３ -- CPUの設計

9/24のマルレクでは、ソフトウェアの開発の世界の話題を取り上げます。https://deep-spec.peatix.com/　

ソフトウェアの開発だけでなくハードウェアの開発も、大規模化・複雑化が進んでいます。ここではCPUの開発での話題を取り上げます。

CPUの設計では、動作の徹底的なシミレーションは可能ですが、最終成果物であるCPUチップに対して、アジャイルのような開発手法はとれません。

今回のマルレクのテーマである「形式手法」は、ハードウェアの正しい動作を保証する手段として、ハードウェアの開発では重要な役割を果たしていて、すでに広く用いられていると語られてきました。

ただ、実態は、必ずしもそうでなかったようです。

RISCVチップの検証を、初めて完全に形式的手法で行うことに成功したチッパラは、次のように語っています。http://bit.ly/2MbSdin

「ソフトウェアに関する経験しかない研究者にとっては、この業界がハードウェアに対して行なっている形式的方法というものが、いたるところで制限されたものだということに驚くことになるだろう。

そこでの形式方法というのは、典型的には、モデルのチェックと充足性の解決に基づいたもので、結局分析は明示的な状態空間の探索に還元される。

検証作業は、フルシステムの（比較的）小さなコンポーネント、例えば、プロセッサの浮動小数点ユニットに集中している。確かに、浮動小数点演算の実装アルゴリズムの完全な検証は、それ自体、英雄的な努力を必要とするのだが、これらの個々の結果は、システム全体の定理には組み込まれない。」

彼の指摘は、昨年来話題になっている、SpectreやMeltdownといった CPUアーキテクチャー設計自体の不備をつく攻撃に対する、CPUの深刻な脆弱性を考えると重要な意味を持っています。

現在のほとんど全てのCPUは「投機的実行 Speculative execution」をサポートしています。投機的実行は、条件付き分岐命令に出会うと、条件の計算が終わるのを待たずに、二つの可能な分岐をキャッシュ上で先読みして実行します。条件の計算が終わって、どちらの分岐が選択されるのか確定した時点で、一方の「当たり」のキャッシュの計算結果が採用され、一方の「はずれ」のキャッシュの中身は無視されます。

Spectreは、キャッシュ上に一定期間、トラップを仕掛けた命令がチェックされずに残存することを利用します。これまでのCPUの「検証」では、こうしたセキュリティ上の「大穴」が存在することが見逃されてきたのです。

写真は、Spectreに対するインテルのパッチを、激しい言葉で非難するライナス。http://bit.ly/2lRIwKI

彼の怒りを理解するには、日本のIT業界のジョーク、「それはバグではありません。仕様です。」を思い出せばいいと思います。

事実、インテルが提供したパッチは、この投機的実行の不都合を「バグ」ではなく、「セキュリティーの特徴 Security feature」と呼び、オプションでこの「特徴」を使うことも（おいおい！）、使わないこともできるとしたものでしたから。

結局、CPUの性能を最大化するための実装が先行していて、それがどういう副作用を持つかの検証が不十分だったということです。

ただ、それは、CPUを設計する「仕様」が実際には完全なものではなく、その正当性・妥当性のチェックがキチンと行われていないことを意味します。それでは、CPUアーキテクチャー自体の持つ脆弱性への攻撃（これからもありうることです）には、個別にモグラ叩きのように対応するしかなくなります。

僕は、RISCVチップの開発で成功した、CPU開発での「形式的手法」の導入に注目しています。