Amazon Web Servicesのシステム正確性の実践事例

• AWSはセキュリティ・耐久性・完全性・可用性を守るため、システム正確性を中核的な基盤と位置づけ、TLA+から始めてモデル検査・ファジング・プロパティベースドテスト・ランタイム検証・形式証明まで適用範囲を広げてきた
• TLA+は従来のテストでは捉えにくいバグを早期に除去し、性能最適化への確信を与えたが、開発者のアクセス性を高めるためにPプログラミング言語やPObserveのようなツールも導入された
• S3 ShardStoreのプロパティベースドテスト、決定的シミュレーション、Aurora Limitless DatabaseのSQLファジングは、形式手法を日常的な開発・統合テストにより近づけた事例である
• Fault Injection ServiceはAPIエラー、I/O一時停止、インスタンス障害のような障害を注入してレジリエンス機構を検証し、Amazon.comはPrime Day 2024の準備過程でFISベースの実験を733件実行した
• Cedar、Firecracker、Graviton 2 RSA最適化のようにセキュリティ境界と性能最適化が重要な領域では形式証明が使われており、高い学習コストとツールの使いやすさは依然として採用の制約として残っている

---

AWSがシステム正確性に取り組む方法

• AWSは、顧客が信頼できるサービスを提供するにはセキュリティ、耐久性、完全性、可用性の高い基準を維持する必要があり、システム正確性がそれを支えているとしている
• 2015年のCACM論文「How Amazon Web Services Uses Formal Methods」は、AWSの中核サービスの正確性を保証するためのアプローチを紹介し、その後これらのサービスはAWSの顧客に広く使われるようになった
• 初期の中心的なツールはLeslie Lamportが開発した形式仕様言語**TLA+**だった
  • 従来のテストでは見落とされがちな微妙なバグを開発初期に発見し、除去するのに役立った
  • システム正確性を維持しながら大胆な性能最適化を実装できるという確信を与えた
• 15年前のAWSのテスト慣行は、主にビルド時の単体テストと限定的なデプロイ時の統合テストに依存していた
• その後AWSは、形式手法と準形式手法を開発プロセスに統合した
  • 定理証明、演繹検証、モデル検査
  • プロパティベースドテスト、ファジング、ランタイムモニタリング

Pプログラミング言語とPObserve

• AWSは2010年代初頭、形式手法を初期チームの外へ広げる過程で、多くのエンジニアがTLA+の学習と生産性の確保に苦労することを確認した
• TLA+は数学に近い高水準の抽象言語である点が強みだが、命令型言語に慣れた開発者には参入障壁になった
• 分散システムのモデリングと分析のための状態機械ベースの言語Pが、このギャップを埋める役割を担った
  • 開発者はシステム設計を通信する状態機械としてモデル化する
  • このメンタルモデルは、マイクロサービスやサービス指向アーキテクチャ（SOA）を多く扱うAmazonの開発者にとって馴染み深い
  • Pは2019年からAWSで開発され、戦略的なオープンソースプロジェクトとして維持されている
• 複数のAWS主要製品チームが、システム設計の正確性レビューにPを使用している
  • ストレージ: Amazon S3, EBS
  • データベース: Amazon DynamoDB, MemoryDB, Aurora
  • コンピュート: EC2, IoT
• S3はeventual consistencyからstrong read-after-write consistencyへ移行する過程でPを使用した
  • S3インデックスサブシステムは、高速なデータ参照を可能にするオブジェクトメタデータの保存場所である
  • 強い一貫性を達成するには、S3インデックスのプロトコルスタックに複数の非自明な変更が必要だった
  • Pによりプロトコル設計を形式的にモデリング・検証し、設計レベルのバグを早期に除去し、リスクの高い最適化をモデル検査で確認できるようになった
• 2023年、AWSのPチームはPObserveを構築した
  • 分散システム実行から得られる構造化ログを使用する
  • ログがシステムの形式的なP仕様で許容される動作と一致するかを事後検証する
  • RustやJavaなどの言語で書かれた本番実装と、設計時のP仕様とのギャップを埋める
  • 設計時の検証と実装のランタイムモニタリングをつなぎ、形式仕様への投資価値を高める

軽量形式手法を開発フローに組み込む方法

• AWSは軽量形式手法を導入し、形式手法をエンジニアリングチームの開発・テストフローにより近づけている

• プロパティベースドテスト

  • Amazon S3のShardStoreは、開発サイクル全体で正確性テストと開発速度の向上のためにプロパティベースドテストを使用している
  • 複数の手法を組み合わせ、人が期待動作を仕様化し、自動化テストがより多くの入力と障害条件を探索できるようにしている
    • 開発者が提供した正確性仕様
    • コードカバレッジ指標で入力分布を導くカバレッジガイド付きファジング
    • ハードウェアやその他のシステム障害をテスト中にシミュレートする障害注入
    • 反例を自動で縮小し、人がデバッグしやすくする最小化

• 決定的シミュレーション

  • 決定的シミュレーションテストは、分散システムを単一スレッドシミュレータ上で実行し、あらゆるランダム性の源を制御する
    • スレッドスケジューリング
    • タイミング
    • メッセージ配送順序
  • 開発者は、分散プロトコルの特定段階で参加者が失敗する状況のように、特定の障害・成功シナリオを書くことができる
  • テストフレームワークが非決定性を制御するため、過去のバグを引き起こした順序のような興味深い実行順序を指定できる
  • スケジューラは順序ファジングや、可能なすべての順序の探索へ拡張できる
  • 遅延や障害状況のシステムプロパティテストを統合テストよりもビルド時に近い位置へ移し、開発を加速し、動作カバレッジを広げる
  • AWSのスレッド順序およびシステム障害のビルド時テスト作業の一部は、shuttleおよびturmoilプロジェクトとしてオープンソース化されている

• 継続的ファジングとランダムテスト入力生成

  • 継続的ファジング、特にカバレッジガイド型のスケーラブルなテスト入力生成は、統合段階でのシステム正確性テストに効果的である
  • Amazon Auroraのデータシャーディング機能であるAurora Limitless Databaseの開発では、2つの重要なプロパティ検証にファジングを広範に使用した
  • SQLクエリとトランザクション全体をファジングし、シャードをまたぐSQL実行の論理分割が正しいことを検証する
  • 大量のランダムなSQLスキーマ、データセット、クエリを合成して対象エンジンで実行し、非シャーディングエンジンを基準とするオラクルと結果を比較する
  • SQLancerが切り開いたアプローチのような、別の検証方式も併用している
  • ファジングと障害注入テストの組み合わせは、データベースの原子性、一貫性、分離性といった正確性の側面にも有用である
    • トランザクションを自動生成する
    • 形式的に仕様化された正確性オラクルで正しい動作を定義する
    • トランザクションとトランザクション内文の可能なインターリービングを対象システム上で実行する
    • Elleのようなアプローチに従い、分離性のようなプロパティを事後検証する

Fault Injection Serviceと障害状況の検証

• AWSは2021年初頭にFault Injection Service(FIS) をリリースし、障害注入ベースのテストを幅広いAWS顧客が利用できるようにした
• FISはAWSインフラ上のテストまたは本番デプロイにシミュレーション障害を注入できる
  • APIエラー
  • I/O一時停止
  • 障害化したインスタンス
• 障害注入により、アーキテクチャに組み込まれたレジリエンス機構が実際に可用性を改善し、新たな正確性問題を生んでいないかを確認できる
  • フェイルオーバー
  • ヘルスチェック
• FISベースの障害注入テストは、AWS顧客とAmazon内部の双方で広く利用されている
• Amazon.comはPrime Day 2024の準備過程で、FISベースの障害注入実験を733件実行した
• 2014年、Yuanらは、テスト対象の分散システムにおける致命的障害の92%が、非致命的エラーの誤った処理によって引き起こされたと分析した
• 正常経路で致命的障害がまれなのは、正常経路が頻繁に実行され、よりよくテストされ、エラー経路よりはるかに単純だからである
• 障害注入テストとFISは、障害や失敗状況でのシステム動作をより容易にテストできるようにし、正常経路とエラー経路のバグ密度の差を縮める
• 障害注入自体は形式手法とは見なされないが、形式仕様と組み合わせることができる
  • 期待動作を形式仕様として定義する
  • 障害注入中およびその後の結果を仕様化された動作と比較する
  • メトリクスやログエラーだけを確認したり、人が目視で判断したりする方法より多くのバグを捉えられる

メタスタビリティと創発的システム挙動

• この10年で、特定種のシステム障害であるメタスタブル障害(metastable failures) への関心が高まっている
• メタスタブル障害とは、過負荷やキャッシュのフラッシュのようなトリガーが、介入なしには回復できない状態へ分散システムを押し込む障害である
  • 介入の例として、負荷を通常より低い水準まで下げることがある
• この障害クラスは、クラウドシステムの非可用性における重要な寄与要因の1つである
• 典型的なメタスタブル挙動では、負荷増加に応じて最初はgoodputが増えるが、その後飽和し、輻輳を経てgoodputが0または0近くまで落ちる
• その後システムは、負荷を少し下げただけでは健全な状態に戻れず、大幅に下げて初めて回復できる
• この挙動は単純なシステムでも現れうえ、多くのシステムではタイムアウト後の再試行というクライアントロジックによっても引き起こされうる
• 従来の分散システムの形式モデリングは通常、安全性(safety)と活性(liveness)に焦点を当てるが、メタスタブル障害はこの分類にきれいには収まらない挙動があることを示している
• AWSは創発的システム挙動を理解するために、離散イベントシミュレーションをより多く活用している
  • カスタムシステムシミュレーションに投資している
  • TLA+やPのような言語で作成した既存のシステムモデルを、シミュレーションに利用できるツールへの投資も行っている
• TLA+のTLCのような全探索モデル検査器を確率的シミュレーションへ拡張すると、事後的な遅延分布のような統計的結果を生成できる
• こうした拡張により、レイテンシSLA達成可能性の理解のような作業にモデル検査を活用できる

形式証明が必要なセキュリティ境界

• 認可や仮想化のような重要なセキュリティ境界では、前述の形式手法だけでは十分でないことがあり、正確性証明への投資価値が大きい

• Cedar認可ポリシー言語

  • AWSは2023年、細粒度の権限を指定するポリシー作成のためのCedar認可ポリシー言語を導入した
  • Cedarは自動推論と形式証明を考慮して設計されている
  • 実装は検証に適したプログラミング言語Dafnyで構築されている
  • Dafnyにより、実装が複数のセキュリティ特性を満たすことを証明した
  • この証明はテストを超える数学的意味での証明である
  • チームは、Dafnyコードを正確性オラクルとして使う差分テストも適用し、本番利用可能なRust実装の正確性を検証した
  • Cedar実装とともに、Dafnyコードとテスト手順をオープンソースで公開し、利用者が正確性への取り組みを確認できるようにした

• Firecracker VMM

  • Firecracker仮想マシンモニタは、virtioという低水準プロトコルを使って、ネットワークカードやSSDのようなエミュレートされたハードウェアデバイスをVM内のゲストカーネルに公開する
  • これらのエミュレートデバイスは、信頼できないゲストと信頼されたホストの間で最も複雑な相互作用を担うため、重要なセキュリティ境界である
  • Firecrackerチームは、Rustコードを形式的に推論できるKaniを使って、このセキュリティ境界の中核特性を証明した
  • この証明は、ゲストが何を試みても境界の重要特性が維持されることを保証する
  • AWSはKani、Dafny、Lean、およびそれらを支えるSMT solverのような基盤ツールの開発を支援している
  • 形式モデルと仕様は複数の形で再利用される
    • 設計時のモデル検査
    • ランタイムモニタリングにおける正確性オラクルの役割
    • 創発的システム挙動のシミュレーション
    • 中核特性の証明構築

正確性を超えた性能とコスト効果

• 形式手法は、クラウドシステムの性能を安全に改善するうえでも重要である
• Auroraリレーショナルデータベースエンジンの中核コミットプロトコルを**PとTLA+**でモデル化した結果、安全性特性を犠牲にせず、分散コミットのコストを2ネットワーク往復から1.5ネットワーク往復へ削減できる機会が見つかった
• こうした成果は、形式手法を導入したチームでは珍しくない
  • 分散プロトコルを深く考え、形式的に記述する過程が構造化された思考を強制する
  • プロトコル構造と解くべき問題に対する、より深い洞察を与える
  • 提案された設計最適化が正しいことを形式的に確認または証明できれば、分散システムエンジニアはリスクを増やさずにより大胆な設計を選べる
• 生産性とコスト効果は、高水準の設計最適化だけに限られない
• AWSチームは、ARMベースのGraviton 2プロセッサにおいてRSA公開鍵暗号化実装の最適化を見つけ、スループットを最大94%改善できた
• HOL Light対話型定理証明器を使って、この最適化の正しさを証明した
• クラウドCPUサイクルの高い割合が暗号化に使われるため、この種の最適化はインフラコスト削減、持続可能性の支援、顧客が体感する性能改善に貢献しうる

残された課題と今後の機会

• AWSは過去15年間で、形式・準形式のテスト手法を拡張することに成功したが、産業的な採用には依然として課題が残る
• 形式手法ツールの主要な障壁は、急な学習曲線と専門的なドメイン知識の要求である
• 多くのツールはいまだに学術色が強く、ユーザーフレンドリーなインターフェースが不足している
• すでに定着した準形式アプローチでも採用障壁は残っている
  • 決定的シミュレーションはAWSやFoundationDBのようなプロジェクトで成功裏に使われてきた中核的な分散システムテスト手法だが、AWSに加わる熟練の分散システム開発者にとっても馴染みがない場合がある
  • 障害注入テスト、プロパティベースドテスト、ファジングのような実証済み手法でも同様のギャップが存在する
• 分散システム開発者に、こうしたテスト手法とツールを教育し、厳密な思考様式を教える必要がある
• 教育ギャップは学術レベルから始まっている
  • 基本的な形式推論アプローチでさえ、教えられる機会はまれである
  • 上位機関の卒業生でも、こうしたツールの採用に苦労する
  • 形式手法と自動推論は産業応用に重要だが、依然としてニッチ分野と見なされている
• メタスタビリティや、大規模システムの他の創発的特性も、同様の認識課題を抱える重要な研究領域である
  • 「タイムアウト時にN回再試行」のように、メタスタブルなシステム挙動を引き起こしうる慣行は、既知の問題であっても今なお広く推奨されている
  • 創発的システム挙動を理解するための現在のツールと手法は初期段階にある
  • システム安定性のモデリングは高コストで複雑である
• AWSは大規模言語モデルとAIアシスタントが、形式手法の実務採用上の問題を大きく緩和すると見ている
  • AI支援の単体テストが人気を集めているのと同様に、開発者が形式モデルや仕様を作成するのを支援できる
  • 高度な手法がより広い開発者コミュニティにアクセス可能になる可能性がある

AWSが継続投資する正確性の枠組み

• 信頼でき、安全なソフトウェアを作るには、システム正確性を推論するための多様なアプローチが必要である
• AWSは、単体テストや統合テストのような業界標準のテストとあわせて複数の手法を採用している
  • モデル検査
  • ファジング
  • プロパティベースドテスト
  • 障害注入テスト
  • 決定的シミュレーション
  • イベントベースシミュレーション
  • 実行トレースのランタイム検証
• 形式仕様は、AWSの複数のテスト実践において正しい答えを与えるテストオラクルとして重要な役割を果たしている
• 正確性テストと形式手法は、すでに得られている投資対効果を踏まえ、AWSの中核投資領域であり続けている