意外な発見: 自動推論がもたらすシステムの効率化と保守性向上

本ブログは 2024 年 10 月 17 日に公開された AWS Blog “An unexpected discovery: Automated reasoning often makes systems more efficient and easier to maintain” を翻訳したものです。

先日、米国防高等研究計画局 (DARPA) を訪問した際にある傾向について話したところ、強い関心を持たれました。Amazon Web Services (AWS) で過去 10 年にわたって自動推論を適用する中で、形式的検証されたコードは、置き換え前の未検証のコードよりもパフォーマンスが優れていることが多いことを確認しています。

これは、形式的検証の過程で行うバグ修正が、実行時パフォーマンスにもプラスの影響を与えることが多いためです。また、自動推論によってビルダーは自信を持ってさらなる最適化に取り組めるようになり、システムパフォーマンスがいっそう向上します。形式的検証されたコードは更新や変更、運用も容易であり、深夜のログ分析やデバッグの頻度も減ることがわかっています。この記事では、DARPA との議論で取り上げた 3 つの事例を紹介します。

自動推論: 基礎

AWS では、お客様にとってシンプルで直感的なサービスの構築に取り組んでいます。そのシンプルさの裏側には、毎秒数十億件のリクエストを処理する、広大で複雑な分散システムがあります。こうした複雑なシステムの正しさを検証することは大きな課題です。本番サービスは、新機能の追加、コンポーネントの再設計、セキュリティの強化、パフォーマンスの最適化に伴って常に進化し続けています。これらの変更の多くはそれ自体が複雑であり、AWS やお客様のセキュリティやレジリエンスに影響を与えることなく実施する必要があります。

設計レビュー、コード監査、ストレステスト、フォールトインジェクションは、いずれも日常的に使用しており、今後も使い続ける非常に重要なツールです。しかし、多くのケースで正しさの確認には、これらの手法だけでは不十分であることもわかっています。特に大規模でフォールトトレラントなアーキテクチャでは、巧妙なバグが検出をすり抜ける可能性があります。また、問題の中には実装上の欠陥ではなく、元のシステム設計自体に根本原因があるものもあります。サービスの規模と複雑さが増すにつれて、従来のテスト手法を数学とロジックに基づくより強力な手法で補完する必要が生じました。ここで人工知能 (AI) の一分野である自動推論が力を発揮します。

従来のテストが特定のシナリオにおけるシステムの動作検証に重点を置くのに対し、自動推論はあらゆるシナリオにおけるシステムの動作をロジックで検証することを目指します。中程度の複雑さのシステムでさえ、発生しうるすべての状態とパラメータの組み合わせを再現するには、途方もない時間がかかります。自動推論を使えば、システムの正しさの論理的な証明を導出することで、同じ効果をすばやく効率的に達成できます。

自動推論を活用するには、ビルダーに異なるマインドセットが求められます。考えうるすべての入力シナリオとその問題点を洗い出そうとするのではなく、システムがどう動作すべきかを定義し、正しく動作するために満たすべき条件を特定します。そして、数学的な証明を使ってその条件が真であることを検証します。つまり、このアプローチによってシステムの正しさを検証できるのです。

自動推論では、システムの仕様と実装を数学的に表現し、アルゴリズム的なアプローチで実装が仕様を満たすことを検証します。システムを数学的にエンコードし、形式的論理を用いて検証することで、システムの将来の動作に関する重要な問いに効率的かつ確実に答えることができます。システムは何ができるのか？何をするのか？何を絶対にしないのか？自動推論は、最も複雑で大規模な、さらには上限のないシステムについても、こうした問いに答えることができます。これは従来のテストだけでは網羅的に検証できないシナリオです。

自動推論によって完璧は達成できるのでしょうか？いいえ、できません。自動推論もまた、システムのコンポーネントが正しく動作することや、システムとその環境のモデルとの関係について、一定の仮定に依存しています。例えば、システムのモデルが、コンパイラやプロセッサなどの基盤コンポーネントにバグがないと誤って仮定している可能性があります (ただし、これらのコンポーネントも形式的検証することは可能です)。とはいえ、自動推論によって、従来のソフトウェア開発やテスト手法では得られない、より高い水準の正しさへの確信が得られるようになります。

開発の高速化

自動推論は、数学者や科学者だけのものではありません。Amazon Simple Storage Service (Amazon S3) のエンジニアは、バグを防ぐために日々自動推論を活用しています。S3 のシンプルなインターフェイスの裏側には、400 兆個のオブジェクトとエクサバイト規模のデータを保持し、毎秒 1 億 5,000 万件を超えるリクエストを定常的に処理する、世界最大級かつ最も複雑な分散システムの 1 つがあります。S3 は多数のサブシステムで構成されており、それぞれが独立した分散システムであり、その多くは数万台のマシンで動作しています。お客様に大規模にご利用いただいている中でも、新機能は常に追加され続けています。

S3 の主要コンポーネントの 1 つが S3 インデックスサブシステムです。これは、高速なデータ検索を可能にするオブジェクトメタデータストアです。このコンポーネントには、非常に大規模で複雑なデータ構造と、精巧に最適化されたアルゴリズムが含まれています。S3 の規模ではアルゴリズムを人間が正確に実装するのは難しく、検索でエラーは許されません。変更を確信を持って行うには極めて慎重な対応と広範なテストが必要なため、新たな改善はおよそ四半期に 1 回のペースにとどまっていました。

S3 は 15 年にわたる経験の上に堅牢に構築され、十分にテストされたシステムです。しかし、S3 インデックスサブシステムには、長い間根本原因を特定できないバグが存在していました。システムはその例外から自動的に回復できたため、バグがシステムの動作に影響を与えることはありませんでした。それでも、この状態に満足してはいませんでした。

なぜこのバグは長期間残り続けたのでしょうか？S3 のような分散システムには多数のコンポーネントがあり、それぞれに固有のコーナーケースがあります。そして、複数のコーナーケースが同時に発生することもあります。300 を超えるマイクロサービスを持つ S3 では、これらのコーナーケースの組み合わせは膨大な数になります。バグが存在する証拠やその根本原因の推測があったとしても、開発者がコーナーケースを 1 つ 1 つ検討し尽くすことは不可能です。ましてや、コーナーケースのあらゆる組み合わせを検討することなど到底できません。

この複雑さがきっかけとなり、自動推論を使って潜在的な状態やそこに潜むエラーを探索する方法を検討しました。システムの形式的仕様を構築することで、バグを発見し、同種のバグがこれ以上存在しないことを証明できました。自動推論の活用により、年に 3～4 回だったアップデートと改善のリリースを、1～2 か月ごとに行えるようになりました。

コードの高速化

AWS Identity and Access Management (IAM) サービスの正しさは、お客様のワークロードのセキュリティの基盤です。数百万のお客様、数千のリソースタイプ、数百の AWS サービスにわたり、すべての API コール (つまり、AWS へのすべてのリクエスト) は IAM の認可エンジンによって処理されます。毎秒 12 億件を超えるリクエストです。これは AWS の中でも最もセキュリティ上重要で、最大規模にスケールされたソフトウェアの 1 つです。

AWS では、いかなる変更も本番環境に反映する前に、システムがセキュアかつ正しい状態を維持していることについて、極めて高い確信が求められます。自動推論を使うことで、あらゆる状況においてシステムが特定のセキュリティプロパティに準拠していることを証明できます。これを証明可能なセキュリティと呼んでいます。自動推論により、お客様に証明可能なセキュリティの保証を提供できるだけでなく、機能、セキュリティ、最適化を大規模に提供できるようになっています。

S3 と同様に、IAM も 15 年をかけて進化してきた、時間の試練を経た信頼性の高いシステムです。しかし、さらに水準を引き上げたいと考えました。既存の IAM 認可エンジンの動作を捉える形式的仕様を構築し、ポリシー評価の原則を証明可能な定理として定式化し、自動推論を使ってより効率的な新しい実装を構築しました。2024 年初めに、正しさが証明された新しい認可エンジンをデプロイしましたが、誰も気づきませんでした。自動推論により、AWS インフラストラクチャの中で最も重要なコンポーネントの 1 つである認可エンジンを、正しさが証明された同等の実装にシームレスに置き換えることができたのです。

仕様と証明が整ったことで、高い確信を持って安全かつ大胆にコードを最適化できるようになりました。IAM の膨大な規模では、わずか 1 マイクロ秒のパフォーマンス向上でさえ、お客様のエクスペリエンスの改善と AWS のコスト最適化に直結します。文字列マッチングの最適化、不要なメモリ割り当てや冗長な計算の削除、セキュリティの強化、スケーラビリティの向上を実現しました。変更のたびに証明を再実行し、システムが正しく動作し続けていることを確認しました。

最適化後の IAM 認可エンジンは、以前のバージョンと比較して 50% 高速になりました。自動推論がなければ、これほどインパクトのある最適化をこれほどの確信を持って実現することは到底できなかったでしょう。この取り組みの詳細については、こちらの AWS re:Inforce セッションをご覧ください。

デプロイの高速化 (とコードの高速化)

オンラインで行われるトランザクションの大半は、暗号によって保護されています。例えば、RSA 暗号化アルゴリズムは 2 つの鍵を生成してデータを保護します。1 つはデータの暗号化用、もう 1 つは復号用です。これらの鍵により、安全なデータ伝送とデジタル署名が実現します。暗号においては、正しさとパフォーマンスの両方が不可欠です。暗号化アルゴリズムのバグは壊滅的な結果を招きかねません。

お客様がワークロードを AWS Graviton に移行するにつれて、ARM 命令セット向けに暗号を最適化するメリットは増しています。しかし、パフォーマンス向上のための暗号の最適化は複雑であり、変更した暗号化アルゴリズムが正しく動作しているかの検証は困難です。自動推論を導入する以前は、暗号ライブラリの最適化を本番環境にリリースするまでに、数か月にわたるレビューが必要になることも珍しくありませんでした。

ここで自動推論が威力を発揮しました。Graviton で RSA を高速化し、形式的検証で正当性を証明し開発も加速しました。楕円曲線暗号に自動推論を適用した場合にも、同様の成果が得られています。

好循環の形成

過去 10 年にわたり、AWS ではクラウドインフラストラクチャとサービスの正しさを証明するために、自動推論技術の適用を拡大してきました。正しさの検証だけでなく、セキュリティと信頼性の向上、設計上の欠陥の最小化にも、日常的にこれらの手法を活用しています。自動推論を使うことで、システムの精密でテスト可能なモデルを作成し、変更が安全であることをすばやく検証できます。また、本番環境に影響を与えることなく、変更が安全でないことを事前に把握することもできます。

インフラストラクチャに関する重要な問いに答え、データを露出させる可能性のある設定不備を検出できます。他の手法では発見できなかったであろう、目立たないが深刻なバグが本番環境に到達するのを防ぐことができます。モデル検査なしでは到底挑戦できなかったような、大胆なパフォーマンス最適化を実現できます。自動推論は、重要なシステムが期待どおりに動作することについて、厳密な数学的保証を提供します。

AWS は、この規模で自動推論を活用する初めてかつ唯一のクラウドプロバイダーです。自動推論ツールの導入が広がるにつれ、ユーザビリティとスケーラビリティの向上に対するより大きな投資が正当化しやすくなります。ツールが使いやすく、強力になるほど、導入はさらに進みます。クラウドインフラストラクチャの正しさをより多く証明できるほど、セキュリティを最重視するお客様にとってクラウドの魅力は高まります。そして、この記事の事例が示すように、セキュリティの保証を高めるだけでなく、よりパフォーマンスの高いコードをお客様に迅速に提供し、最終的にはお客様に還元できるコスト削減も実現しています。

セキュリティ、コンプライアンス、可用性、耐久性、安全性といった重要な特性を、大規模なクラウドアーキテクチャに対して自動的に証明できる時代が始まりつつあると考えています。AI ハルシネーションの潜在的な問題の防止から、ハイパーバイザー、暗号、分散システムの分析に至るまで、確かな数学的推論を基盤に据え、構築するものを継続的に分析し続けていることが、Amazon ならではの強みです。

関連情報

• Amazon Science ブログで自動推論の詳細をご覧ください
• AWS が自動推論により証明可能なセキュリティを提供する方法をご覧ください
• AWS Automated Reasoning Group でのインターンシップにご興味がある方は、お問い合わせください

 

この記事についてご質問がある場合は、AWS サポートにお問い合わせください。