# Zodiac [[Infrastructure as Code|IaC]] プログラムのセマンティックチェックを、公開リポジトリからの[[設定マイニング|マイニング]]とデプロイベースの検証で自動発掘するツール([[@2024__SOSP__Unearthing Semantic Checks for Cloud Infrastructure-as-Code Programs]], SOSP '24)。Python 約 11,000 行で実装され、KB 構築・マイニングは Rego/OPA クエリ、negative テスト生成は Z3 SMT ソルバ、補間は GPT-4 を用いる。([[@2024__SOSP__Unearthing Semantic Checks for Cloud Infrastructure-as-Code Programs]]) - **適用対象**: [[Terraform]] / [[Microsoft Azure]] の 52 リソース種別。26,000 リポジトリ・~3.8M 行から ~9,800 仮説チェックを生成し、510 の検証済みセマンティックチェックを得た。 - **成果**: 200+ のバグを含む Terraform リポジトリを発見し、Terraform Azure provider 公式ドキュメントの 4 つの誤った使用例を修正させた(GitHub issues #27065/#27078/#27194/#27222)。 - **OSS**: https://github.com/824728350/Zodiac(リポジトリ名も Zodiac)。Terraform core・Azure provider プラグイン・Rego/OPA・Z3 SMT ソルバに依存。 - **限界**: open-world assumption により健全性なし(偽陽性 5.4%)。Terraform/Azure 限定で、AWS CDK・Pulumi 等への一般化は未実証。 - **同一グループの兄弟研究**: [[Ang Chen]]([[University of Michigan]])グループの IaC ライフサイクル研究の 1 つで、デプロイ前検証を担う。逆生成は [[Lilac]]([[@2025__AIOps__Automated Lifting for Cloud Infrastructure-as-Code Programs]])、drift 修復は [[NSync]]([[@2025__arXiv__Automated Cloud Infrastructure-as-Code Reconciliation with AI Agents]])。Zodiac の [[Yiming Qiu]]・[[Patrick Tser Jern Kon]] は Lilac にも参加。3 者の住み分けは [[Infrastructure as Code]] を参照。 ## 関連 - ソース: [[@2024__SOSP__Unearthing Semantic Checks for Cloud Infrastructure-as-Code Programs]] - 開発者: [[Yiming Qiu]] / [[Patrick Tser Jern Kon]] / [[Ryan Beckett]] / [[Ang Chen]] - 所属: [[University of Michigan]] / [[Microsoft]] - 関連概念: [[Infrastructure as Code]] / [[設定マイニング]] / [[障害注入]] - 依存プロダクト: [[Terraform]] / [[Microsoft Azure]] - 兄弟プロダクト(同一グループ): [[Lilac]] / [[NSync]] - 関連 MOC: [[Software Engineering - MOC]] / [[Network - MOC]]