Amazon Web Servicesにおけるシステム正確性の実践事例
(cacm.acm.org)- Amazon Web Services(AWS) は、サービスの正確性を中核的な価値と位置づけ、さまざまな形式手法を開発プロセスに統合している
- TLA+やP言語などの形式仕様ツールにより、微妙なバグを早期に発見し、大胆な最適化においても信頼性を確保できる
- AWSは軽量な形式手法として、プロパティベーステスト・決定論的シミュレーション・継続的ファジングなども幅広く運用している
- Fault Injection Serviceのような障害注入ツールを通じて、障害発生時を含む信頼性検証を自動化している
- 教育面の障壁やツールの複雑さは依然として残るが、AIと自動化ツールの普及が導入拡大に寄与すると見込まれる
AWSのシステム正確性保証戦略
Amazon Web Services(AWS)は、顧客が完全に信頼できる高信頼なサービスの提供を目標としている
そのために、セキュリティ、耐久性、完全性、可用性の基準維持を追求し、その中心にシステム正確性の概念を据えている
2015年にCommunications of the ACMで紹介されたAWSの形式手法適用事例以降、このアプローチは中核サービスの成功裏の運用に重要な役割を果たしてきた
中心には、Leslie Lamportが開発したTLA+という形式仕様言語がある
AWSにおけるTLA+導入の経験は、開発初期段階で従来のテストでは捉えられない微細なバグを把握できるようにした
また、大胆な性能最適化を進める際にも、形式的検証によって安定性と信頼性を確保できた
15年前のAWSは、ビルド時の単体テストや限定的な統合テストなど基本水準にとどまっていたが、その後は形式的アプローチと準形式的手法を包括的に導入した
こうした変化は、正確性だけでなく、高水準および低水準の最適化検証、開発速度の向上、コスト削減にも寄与している
AWSでは、従来の定理証明、モデル検査に加え、プロパティベーステスト、ファジング、ランタイムモニタリングなども形式手法の範疇として受け入れている
Pプログラミング言語の登場
当初、TLA+には強力な抽象的記述という利点があった一方で、多くの開発者にとって数理記法の使用は参入障壁が高かった
そこでAWSは、開発者に馴染みのある状態機械ベースのアプローチを提供するP言語を導入した
P言語は、分散システムの設計と分析のために状態機械モデリング方式を提供する
マイクロサービスベースのSOAアーキテクチャを用いるAmazonの開発者にとって親しみやすい概念である
2019年からAWSで開発され、戦略的オープンソースプロジェクトとして管理されている
Amazon S3、EBS、DynamoDB、Aurora、EC2、IoTなどの主要サービスチームがPを活用し、システム設計の正確性検証を行っている
S3を強力なread-after-write整合性へ移行する際、Pでプロトコルをモデリング・検証することで、設計初期段階でバグを除去し、最適化事項も安定して反映した
2023年、AWSのPチームはPObserveツールを開発し、テスト環境と実運用環境の両方で分散システムの正確性を検証できるようにした
PObserveは実行ログを抽出し、仕様に従って正しい動作が行われたかを事後検証でき、設計段階の仕様と実際のコード実装を効果的に結び付ける
軽量形式手法の拡大
プロパティベーステスト
代表的な軽量形式技法としてプロパティベーステストがある
たとえばS3のShardStore開発チームは、開発サイクル全体を通して、プロパティベーステスト、コードカバレッジベースのファジング、障害注入、反例最小化などを組み合わせて使用している
この方式は、開発者が直接記述する正確性仕様と連動し、問題のデバッグ効率も大きく向上させる
決定論的シミュレーション
決定論的シミュレーションテストでは、単一スレッドのシミュレータ上で分散システムを実行し、あらゆる乱数要素（スケジューリング、タイミング、メッセージ順序など）を制御できる
特定のエラーおよび成功シナリオに対するテスト、バグを誘発する順序の調整、ファジングの拡張など、さまざまな形で適用される
これにより、システムの遅延や障害などの動作検証をビルド段階で早期に実施でき、テスト範囲も拡大する
AWSはこのようなビルドタイムテストコードを、shuttle、turmoilのオープンソースプロジェクトとして公開している
継続的ファジング
継続的ファジング、特にコードカバレッジベースの大規模入力生成は、統合テスト段階でのシステム正確性検証に有効である
たとえばAurora Limitless Databaseの開発では、SQLクエリとトランザクションをファジングし、パーティショニングロジックの正確性を、大量のランダムなスキーマ、データセット、クエリを生成して検証している
結果は、non-shardedエンジンの動作、またはSQLancerなどの方式と比較する
ファジングと障害注入を組み合わせることで、原子性、一貫性、分離性などデータベースの中核的性質を検証する
自動生成トランザクションや分離性など一部の性質は、実行履歴ベースの事後検証によって保証する
Fault Injection Serviceによる障害注入
2021年、AWSはFault Injection Service(FIS) を公開し、顧客もAPIエラー、I/O中断、インスタンス障害など多様な欠陥シナリオを実環境またはテスト環境で迅速に試せるようにした
これにより、アーキテクチャの可用性確保と障害復元力の点検、エラーケースにおける高いバグ密度差の解消、発生可能性の高い重大問題の事前発見といった効果がある
FISはAWSの顧客だけでなくAmazon社内でも広範に利用されており、たとえばPrime Dayの準備過程だけでも733件の実験が行われた
エラー注入は形式仕様と組み合わせるとさらに効果的である
期待される動作を形式仕様として記述したうえで、実際に欠陥を発生させた結果と照合することで、従来の単純なログや指標の点検よりも多くの誤りを検出できる
メタ安定性とシステムの創発的動作
分散システムでは、過度な負荷やキャッシュ枯渇などをきっかけに、「自力では回復不能」な異常状態（メタ安定状態）に陥る事例が増えている
この状態では、単に負荷を下げるだけでは正常復旧せず、通常のエラーケースより対応が難しい
再試行とタイムアウトのロジックの多くも、この現象の原因となる
従来の形式仕様は安全性と進行性に焦点を当てるが、メタ安定性ではそれ以外の多様な創発的動作まで考慮する必要がある
AWSはTLA+やPなどの仕様モデルを基に離散イベントシミュレーションを実行し、性能SLA達成可能性や遅延分布の算出など、確率的特性まで体系的に分析している
形式証明の必要性
一部の**セキュリティ境界（権限、仮想化など）**では、単なるテストを超えた数学的水準の証明が不可欠である
たとえば2023年にAWSが導入したCedar権限ポリシー言語は、Dafnyベースで自動証明と形式的検証に最適化されており、公開コードと修正手順を通じて一般ユーザーも直接検証できる
また、Firecracker VMMのセキュリティ境界に関する主要な性質は、KaniなどのRustコード解析ツールで証明作業が進められている
このように、形式モデルと仕様をさまざまな段階（設計、実装、実行、証明）で幅広く活用することで、ソフトウェアの正確性確保と企業・顧客価値の拡大に役立てている
正確性を超えた追加効果
形式手法は信頼性と性能改善の両方において重要な役割を果たす
たとえばAuroraのcommitプロトコルをPとTLA+で検証し、ネットワークに要するラウンドトリップを減らすと同時に安全性も保証した
RSA暗号アルゴリズムのARM Graviton 2最適化では、HOL Lightで変換の数学的正確性を証明し、性能とインフラコストの同時改善という実質的な効果を得た
未来の課題と機会
15年間でAWSは形式的・準形式的手法の産業適用を大きく拡大してきたが、学習曲線、専門家の必要性、ツールの学術的性格など、実際の導入障壁は依然として存在する
プロパティベーステストや決定論的シミュレーションも、多くの開発者にとってはなお馴染みが薄い
教育上の参入障壁は学部課程の段階から存在するため、ツールや手法の普及と実務適用は緩やかに進んでいる
メタ安定性のような大規模システムの創発的特性も、まだ研究初期段階にある
今後はAI/大規模言語モデルが形式モデルや仕様の作成を支援し、実務者のアクセス性を短期間で飛躍的に高めることが期待される
結論
堅牢で安全なソフトウェアを構築するには、システム正確性を確保するための多様な手段が必要である
AWSは標準的なテスト手法に加え、モデル検査、ファジング、プロパティベーステスト、障害注入テスト、決定論的／イベントベースシミュレーション、実行履歴検証などを包括的に導入している
形式仕様と形式手法はAWSの開発プロセスにおいて重要なテストオラクルの役割を果たしており、すでに実質的・経済的効果の検証を通じて、投資対象領域の一つとして位置付けられている
1件のコメント
Hacker Newsのコメント
決定論的シミュレーションテスト方式について話したい。AWSでは分散システムを単一スレッドのシミュレータ上で実行し、スレッドスケジューリング、タイミング、メッセージ配信順序など、あらゆる非決定的要素を制御している。そのうえで、特定の失敗または成功シナリオに合わせたテストを書き、システム内の非決定性はテストフレームワークが制御する。開発者は過去にバグを引き起こした特定の順序を指定できる。スケジューラは順序に対するファジングや、あり得るすべての順序の探索にまで拡張可能だ。こうしたものを言語非依存でオープンソース実装したライブラリがあるのか気になる。コンテナ内でネットワーキング、ストレージなどもテスト時点で「決定的」にするミドルウェアツールが必要だ、という発想だ。antithesisはほぼこれに近い役割を果たしているが、まだオープンソースでは見ていない。テストをうまく書けばI/Oなどをスタブ化してある程度は解決できるが、誰もがテストをうまく書くとは限らない。アプリケーションの上に、より高いレイヤーで決定性を提供できるとよいと思う。一方で、AIがテストで本領を発揮できるのではないかと期待している。プロンプト（要件）-テスト実装-AI-実行コードという3つの軸が理想的に噛み合う可能性がある。AIが形式検証をもっと容易にして、ソフトウェアの世界を一段と厳密なものにしてくれることを期待している
決定論的シミュレーションテスト（DST）技術の普及には2つの難しさがある。第一に、従来はすべてのシステムを特定のシミュレーションフレームワーク上に直接載せ、ほかの依存関係がないようにする必要があった。第二に、入力生成と探索が弱いと、テストがすべて成功したように見えても実質的な検証にならない。antithesisはこの2つの両方を解決しようとしているが、まだ難題は多い。決定性を任意のソフトウェアに適用する確実な方法を持っているところはほとんどない。FacebookのHermitプロジェクトも決定論的なLinuxユーザースペースとして試みられたが、最終的には中止された。決定論的コンピュータはテスト以外にも非常に有用な技術基盤であり、いつか誰かがオープンソースとして公開するだろうと思う
QEMUを100%エミュレーションモードで単一スレッド実行して決定論的マシンを得るのは、比較的容易だと思う。ただ、本当に欲しいのは「制御された」決定論的実行で、これははるかに難しい。複数のプロセスを指定したシナリオどおりに動かすには、特にCPUやOSスケジューラのレベルで難易度が非常に高い。言語に依存しない環境そのものを作るのも難しく、細部に振り回されやすい。私もJVMスレッドを複数、特定の動作時点でロックステップで動かす簡単なシステムを作ったことがあり、I/Oとシステム時刻はスタブ化と制御で処理した。おかげで、非同期コンポーネント間の多様な相互作用、I/O障害、リトライなどもテストでき、本番投入前に厄介なバグを捕まえられた。ただし、システム全体を制御するのではなく、特定の同期ポイントだけを単純化したことで可能になっていた。同期ミスによる一般的なデータレースは、この方法では捉えにくい
FoundationDBのテスト手法の公式ドキュメント および YouTubeの発表動画 を共有
gdbでデバッグ可能な言語なら https://rr-project.org/ プロジェクトがおすすめ
Joe Armstrongがproperty testingを使ってDropboxをテストした発表を以前見た記憶がある
S3は、これまで見てきたソフトウェアの中でもっともすごいものの一つだと思う。数年前にS3全体に強力な読み取り後書き込み一貫性を追加したのも、まさにソフトウェアエンジニアリングの極致だと思う ブログ記事リンク
S3のライフサイクル担当として実際に働いたことがあるが、その頃はインデックスチームがこの一貫性を提供するための構造を新たに設計していた時期と重なっていた。外から見てもS3はすごいが、内部では実装も組織構造も想像を超えるほど印象的だ
Google Cloud Storageは、むしろS3よりずっと前からこの機能（強い一貫性）を備えていた。全体としてGCSのほうが、より体系的でしっかり作られた製品という印象がある
92%という数字（クラスタ障害の大半が些細な失敗から始まる）には共感する。派手な大事故ではなく、「大したことのない」リトライが状態の蓄積につながり、最終的に深夜2時に大規模障害として爆発することが大半だ。目立たない失敗にもっと多くのエンジニアリング時間を割くことが重要だ
本当に興味深い記事だと思う。インフラのコントロールプレーン構築に状態機械を使うのは必須だ。Pが本当に必要だったかは分からない。私たちも13年以上Rubyでインフラのコントロールプレーンを作ってきたが、とてもうまく動いている 関連経験を共有するブログ
P言語について気になっていたことがある。以前はMicrosoftでWindows USBスタックのランタイム用途にPからCコードを生成して実際に使っていたようだが、今はもう運用コード生成には使っていないように見える。この件についてHacker Newsにも質問を残したことがある 質問リンク。カーネルにまで生成コードを入れられるなら、ずっと制約の緩いクラウド環境でも当然使えるはずだ
AWS出身ではなく、TLA+やPにも詳しくない立場からすると、「Hello World」程度の例でもあれば、まだ理解しやすかったと思う。記事だけ読むと、ただ苦しいプロセスのようにも感じられるし、良い設計とテストだけで十分に捉えられる問題なのでは、という気もする。簡単な例があれば、実際に何をしているのか判断する助けになっただろう
私の好きなTLA+の手早いデモ例がある gistリンク。複数スレッドが共有カウンタを互いに非アトミックにインクリメントするモデルで、性質検証を行うとrace conditionが見つかる。実際、こういうバグをテストだけで発見するのは非常に難しい。ほとんどのTLA+仕様はもっと複雑だが、単純な誤りを捉えるにはこの例がよい
実際にTLAを使ってみたことがあるが、グラフィカルツールがチュートリアルとうまく噛み合っておらず、がっかりした経験がある。TLA自体は使いたかったし、Lamportの仕事（LaTeXから論文まで）は以前から好きだった
形式手法を使う前提は、結局のところテストだけであらゆる問題を絶対に捉え切ることはできない、という点にある
公式の TLA+ Examples GitHubリポジトリ がおすすめ。DieHard問題のような単純なものから始めるのを勧める
テストは、問題の特定のインスタンスに対して実装の正しさを証明するが、形式検証は問題のクラス全体に対して証明する。たとえばアナグラムを返す関数なら、テストでは一部の単語ペアでしか確認しないが、すべての単語ペアに対する正しさを証明するにはformal verificationが必要だ。undefined behaviorやライブラリバグのようなケースも、formal verificationの過程でしか見つからないことが多い
「プロパティベーステスト、ファジング、ランタイムモニタリングのような軽量な準形式手法」という言及について、property-based testingとfuzzingは形式手法の下位集合だとしても、runtime monitoringまで準形式手法に含めるのはやや広げすぎだと感じる
以前、Leslie LamportとBuridan's Principle関連の論文などを通じて接点があった。今日、彼のホームページでTLA+とPlusCalについて多くを知った Petersonの例のページ。数学をプログラミングに持ち込み、並行システム分野の草分けのような人物がシステム設計言語（TLA+）を作り、それがAWSなどで使われているというのは実に自然だ。分散システムを構築する人たちがLamportの作ったものをもっと使ってほしいと思う。大規模システムでは正しさの証明が非常に重要だ
既存コードからTLA+仕様への変換には、Claude Opus（Extended Thinking）がかなり使える。RustプロジェクトやC++の中核コンポーネントの検証でも、いくつもバグを見つけた経験がある。ほかのモデルは構文や仕様ロジックでよく詰まる一方、Opusはずっと滑らかに動作する
大規模システムだけでなく、SSHやターミナルのような小さいが重要な（世界中で広く使われる）ユーティリティでも、正しさの証明は非常に有益だ
「システムの正しさの証明」という発言について、実際にはすべてを証明することは不可能だ。モデルチェッカーは、限られた状態空間の中で記述した仕様が性質を満たすことを示せるだけだ
個人的には、FISを分散サービス実験に使った経験がある人がいるのか気になる。導入を検討しているが、実際に大規模な実験を行った経験はない
PromelaとSPINは、記事で扱われているものよりさらに高水準の言語なのか気になる