> [!abstract] 概要(SOSP '24 abstract の日本語訳) > クラウドインフラはますます Infrastructure-as-Code(IaC)フレームワーク(例: Terraform)で管理されるようになっている。IaC フレームワークはクラウド利用者が、低レベルのクラウド API コールを直接扱うことなく、宣言的にリソースを構成できるようにする。しかし今日の IaC ツールでは、コンパイル段階を通過した IaC プログラムであってもデプロイ時にエラーを起こしうるため、重大な障害につながる。我々は、これが IaC レベルのプログラムとクラウドレベルの要求の間の根本的な semantic gap に由来すると観察する——構文的に正しい IaC プログラムであっても、クラウドレベルの期待に違反しうるのである。このギャップを橋渡しするため、我々はクラウドレベルの要求に関する IaC レベルのセマンティックチェックを発掘できるツール Zodiac を開発する。Zodiac はこれらのチェックをオンラインの IaC リポジトリからマイニングし、デプロイベースのテストで検証する自動パイプラインを提供する。我々は Zodiac を、主要な IaC フレームワークかつ主要なクラウドベンダである Microsoft Azure が提供する Terraform リソースに適用し、違反するとデプロイ失敗を生む 500 以上のセマンティックチェックを発見した。これらのチェックを用いて、200 以上のバグを含む Terraform プロジェクトを特定し、公式 Azure provider の使用例に含まれるエラーの修正を支援した。 ## 論文情報 - **タイトル**: Unearthing Semantic Checks for Cloud Infrastructure-as-Code Programs - **著者**: [[Yiming Qiu]]、[[Patrick Tser Jern Kon]]、[[Ryan Beckett]](† [[Microsoft]])、[[Ang Chen]]（いずれも [[University of Michigan]]、Beckett のみ Microsoft） - **媒体**: SOSP '24（ACM SIGOPS 30th Symposium on Operating Systems Principles）、2024 年 11 月 4–6 日、Austin, TX, USA、pp. 574–589 - **DOI**: 10.1145/3694715.3695974（ISBN 979-8-4007-1251-7/24/11） - **コード**: [[Zodiac]]（https://github.com/824728350/Zodiac） ## 概要 IaC プログラムがコンパイルを通過してもデプロイ時に失敗する問題を、IaC レベルとクラウドレベルの間の **semantic gap** として定式化した一次論文。Zodiac は公開 Terraform リポジトリからセマンティックチェックを[[設定マイニング|マイニング]]し、SMT ソルバと実際のクラウドデプロイによる positive/negative テストで検証する自動パイプラインで、[[Microsoft Azure]] の 52 リソース種別に対し 510 の検証済みチェックを発掘した。 ## 問題設定 - **入力**: GitHub からクロールした公開 Terraform リポジトリ群(オープンソースの IaC プログラム)。 - **出力**: 違反するとデプロイ失敗を生む、検証済みのセマンティックチェック集合。 - **前提・必要なデータ**: IaC provider のスキーマファイル(リソース属性の型・必須性等)、provider registry の使用例、クラウドへ実際にデプロイできる環境(課金口座)。 - **核心の問題**: テナント(利用者)とプロバイダ(Amazon・Microsoft 等)の分離により、テナントはクラウドレベルの挙動・規約に限られた可視性しか持たない。図 1 の Terraform スニペットはコンパイルに成功するが、(a) VM とその NIC が異なるリージョンにあってはならない、(b) サブネットの CIDR レンジは互いに重複してはならない、という Azure の規約に 2 箇所違反し、デプロイ時に初めて顕在化する。クラウドのプロビジョニングは遅く(最悪で 1 リソース数時間)、失敗の修正はリソースの破棄・再作成を伴いうるため高コスト。 ## 提案手法 ### アーキテクチャ(図 2) Zodiac は 2 フェーズのパイプライン。**マイニングフェーズ**(§3)が IaC リポジトリから仮説チェック(hypothesized checks)を生成し、**検証フェーズ**(§4)がデプロイベースのテストで各チェックを検証(validated)または棄却(falsified)する。中核は「セマンティック知識ベース(KB)」と「チェック仕様言語(DSL)」。 ### マイニングフェーズ(§3) - **セマンティック知識ベース(§3.1、表 1)**: チェック構築の「基本事実」を 3 クラスで保持。(1) **IaC native 制約**(provider スキーマ由来。required/optional、型、nested、computed 等)、(2) **provider 固有制約**(例: `subnet.name` は一般文字列だが "FWSubnet" のような予約 Enum 値を持つ。CIDR か port か等も符号化)、(3) **resource references**(例: `SUBNET.name = VPC.name` は同名制約、`SUBNET.vpc_name = VPC.name` はデプロイ順序の参照、という意味の違いを registry 例から構築)。 - **チェック仕様言語(§3.2、図 4)**: IaC プログラムは「設定の設定」(configuration of configurations)で階層的なので、属性レベルでなく**リソースグラフ上のアサーション**として表現。トポロジカル述語 `conn`(直接接続)・`path`(到達可能)・`coconn`(2 辺の共起)・`copath`(2 経路の共起)に加え、集約式 `indegree`/`outdegree`(特定型の入次数/出次数)。図 3 の 3 例: ①VM が NIC に接続なら同一リージョン、②同一 VM に繋がる 2 つの NIC は同一 VPC、③sku が "sb1ls" の VM はデータディスク ≤ 2。 - **チェックマイニング(§3.3)**: 文法から 84 のテンプレートを手作業 + 自動生成でキュレート(クラウドプロバイダごとに一度だけ)。**アソシエーションルールマイニング**でクロールしたリポジトリをテンプレートの観点で走査し、witnessed なチェックを具体化。 - **統計的フィルタリング**: 各チェックに **confidence**(条件付き確率 P(Y|X)、反例の少なさを選好)と **lift**(P(Y|X)/P(Y)、条件と結論の相関の強さ)を計算し、低いものを除去。 - **LLM 推論(interpolation)**: 量的範囲・Enum 等で観測が不完全なケースを、信頼できるオンライン文書(クラウドの sku 表等)を参照させた [[設定マイニング#LLM interpolation|LLM(GPT-4)の補間]]で埋める。few-shot のプロンプトエンジニアリングで fact-checking も行う。 ### 検証フェーズ(§4) - 各仮説チェック c に対し、c に適合し**デプロイに成功する** positive テスト $t_p$ と、c のみを違反させ**デプロイに失敗する** negative テスト $t_n$ を作る。両条件を満たせば validated、満たさなければ falsified。 - **ソルバ支援の mutation(§4.1)**: $t_p$ の属性・接続をシンボリック値(`??`)に置換し、Z3 SMT ソルバに「$t_n$ は c を違反するが、$R_v$(検証済み)・$R_c$(候補)の他チェックと KB の基本事実には適合する」制約を解かせる。これにより**ただ 1 つのチェック c のみが違反する**精密なテストを構成し、根本原因の取り違えを防ぐ。SMT の最適化目的で $t_n$ と $t_p$ の差分を最小化(値は近傍へ、接続は維持)。 - **MDC pruning**: c に無関係なリソースと、c の発効後にデプロイされる子リソースを刈り込み、c を witness する最小デプロイ可能構成(Minimal Deployable Configuration)を $t_p$ とする。テストサイズを 3〜9 倍削減(表 6)。 - **検証スケジューリング(§4.2、図 5)**: チェック間の相互干渉(あるチェックの違反を作ると別チェックも違反する)による行き詰まりを、**evaluation partial order**(例: VM は NIC の後にデプロイされるので、NIC のみの構成で VM 系チェックを無視できる)と、**false positive removal pass / true positive validation pass** の反復で解消。区別不能(indistinguishable)なチェック群はまとめて検証扱いにする。 ### 実装(§5 Prototype) Python 約 11,000 行(データ処理・KB 構築 ~3,100、マイニング ~4,100、検証 ~3,800)。KB 構築・マイニングは [[設定マイニング|Rego/OPA]] クエリで実装、テストケース生成は Z3、補間クエリは GPT-4。 ## 新規性 - 既存の設定マイニング研究(EnCore [70]、Santolucito ら [60, 61])は MySQL 等の「フラットな」設定の属性間相関を対象とし、検証は手作業(Stack Overflow・GitHub issue を辿る)。Zodiac は (1) IaC の**階層的・グラフ的**構造を扱う DSL、(2) **自動検証**(実デプロイによる positive/negative テスト)、(3) **inter-resource** 制約の発見、で差別化。クラウドバックエンドはブラックボックスで形式モデル化が困難なため、ネットワーク制御プレーン検証 [36] のようなホワイトボックス解析は適用しにくく、エンドツーエンドのデプロイ観測が必須という立場。 - 既存 IaC チェッカ(Terraform native validate、TFSec、Checkov、TFComp、Regula、TFLint)は per-attribute 検証やセキュリティ/ポリシー準拠が主で、inter-resource なセマンティクスを捕捉できない。 ## 実験設定 - **対象**: [[Microsoft Azure]] の人気 52 リソース種別。GitHub から 26,000 IaC リポジトリをクロール → 前処理後 ~6,000 プロジェクト・~3.8M 行の Terraform コード。 - **パイプライン**: IaC プログラムをデプロイプランへコンパイルし、マイニングと検証の双方の基盤に。SMT ソルバ非互換のプロジェクトを除外し、~4,200 プロジェクトを検証へ。 - **比較対象**: Native validate(JSON スキーマ)、TFSec/Checkov/TFComp/Regula(セキュリティ系)、TFLint(静的チェッカ)。 - **評価指標**: prevalence(問題報告された入力の割合)・precision(報告の中で実際にデプロイ問題だった割合)・blast radius(チェック違反で影響を受けるリソース種別数)。 ## 実験結果 - **発見数(§5.1)**: マイニングで ~9,800 仮説チェック → confidence/lift で ~5,600 除去 → 検証フェーズで **510 の検証済みチェック**(区別不能チェックは 1 と数える)。マイニング < 2 時間、検証 < 3 日。 - **既存ツールとの比較(§5.2、表 4)**: ~500 の negative テストを各チェッカへ入力。Native validate のコンパイル失敗は 11.74% にとどまり、うち実際のセマンティック違反は 36.66%(全体の 4.00%)。セキュリティ系チェッカはデプロイ失敗を狙っていないため Zodiac チェックを捕捉できない。TFLint は HCL のみ対応で直接比較不能。Zodiac のチェックは既存ツールに存在しない。 - **マイニングの有効性(§5.3、図 7)**: KB により intra-resource チェック数を桁違いに削減(KB なしで >70,000、Zodiac は ~2,000、約 35 倍)。confidence フィルタが 38.3%、lift が追加で 16.2% を除去。補間は初期に >800 チェックを生成し、40% を LLM が支持して採用。 - **検証の有効性(§5.4、表 5、図 8)**: 他チェックを考慮しないと negative テスト 1 件あたり真陽性違反 4.80・偽陽性違反 11.76 が混入し結論を出せない。全チェック考慮 + mutation 最小化で属性変更数を 11.05 → 2.87 に抑制。スケジューリングは 6 反復で $R_c$ が空に収束。区別不能チェックの扱いがないと未収束のまま残る。 - **デプロイ失敗の内訳(表 3)**: plugin checks 9.00%、pre-deploy sync 5.84%、**sending request 74.94%**(大半)、polling request 7.79%、post-deploy sync 2.43%。 - **blast radius(図 6)**: チェック 1 違反で最悪 ~7 リソース種別が rollback、~6 が halting の影響を受ける。VPC の CIDR は直接変更不可のため、52 種別中 36 種別が rollback 半径に入る。 - **実世界の誤設定(§5.5)**: 検証に使ったリポジトリの 85 件(2.0%)で誤設定を検出。違反最多の上位 3 チェックを GitHub API 検索に変換し、データセット外の 200+ リポジトリで違反を発見。さらに Terraform Azure provider 公式ドキュメントの **4 つの誤った使用例**を特定し、GitHub issue(#27065, #27078, #27194, #27222)で報告・修正提案、すべて修正された。例: APPGW に使う IP は Basic でなく Standard sku が必須(かつ Dynamic 割り当ては Basic 必須なので allocation も Static へ)、APPGW のサブネットは排他的、という 2 違反を同時に含む公式例。 ## 考察 - **false positives(§5.6)**: open-world assumption により健全性は保証されない。検証エンジン初期出力 539 チェックのうち 29(5.4%)が偽陽性——17(3.1%)は自動の反例テスト(他リポジトリでの違反が実際はデプロイ可能だった)、12(2.2%)は手作業の文書照合で発見。$t_n$ の失敗の真因が、Zodiac が知らない別チェックにある場合に偽陽性が生じる(例: `path(VM→VPC) ⇒ source_image_ref != null` は `create == 'Attach'` の場合に成り立たないが、データセットに Attach がほぼ無く誤って真と判定)。 - **限界(§6)**: 現プロトタイプは Terraform/Azure 限定。宣言的でない Pulumi 等の imperative フレームワークや、core compiler を自前で持つ AWS CDK へは追加の解析技術・手作業キュレーション(KB・テンプレート、約 400 行)が必要。region 固有・subscription 固有(クォータ)の制約は未対応。デプロイプランの JSON を共通項にする一般化が将来課題。 - **応用**: 発掘したセマンティックチェックを、LLM ベースの IaC プログラム合成(Pulumi AI 等)の RAG 知識ベースやドキュメント補強に転用できる。 ## 強み - デプロイ時にしか顕在化しない「semantic gap」を初めて体系化し、**マイニング(発見)と検証(デプロイ観測)を完全自動化**した。 - inter-resource・集約まで含むグラフ上のチェックを DSL で表現し、SMT で「単一チェックのみ違反」を保証する精密な negative テスト生成を実現。 - 実クラウドへのデプロイで裏取りした実用的成果(200+ バグ、公式ドキュメント 4 件の修正)。 ## 弱点・課題 - **健全性なし**(open-world assumption)。マイニングデータに現れない invariant やテンプレート外の制約は発見できず、5.4% の偽陽性が残る。 - データ希少性に依存——人気の低い「low-resource」クラウドや、データセットに稀な構成(前述の `create == 'Attach'`)では誤ったチェックを生む。 - 検証フェーズが実デプロイを要し 3 日かかる。テンプレート追加は手作業。region/subscription 固有制約は射程外。 - 評価は Azure/Terraform に限定。AWS・GCP・imperative フレームワークへの一般化は未実証(必要工数の見積もりにとどまる)。