📝
Kubernetes オペレーターの形式検証

2025/07/29に公開
Kubernetes オペレーターは、ユーザーがコントローラーを独自に開発してアプリケーションやクラスターを制御するための拡張パターンです。カスタムリソースや外部アプリケーションのエンティティを非同期的に操作する必要があるため、オペレーターの開発は慎重に行う必要があります。
複雑なアプリケーションをバグなく開発するために、形式手法のアプローチがしばしば取り入れられます。Anvil は、Sun らが USENIX OSDI'24 で提案した、Kubernetes オペレーターに形式手法を取り入れたフレームワークです。論文や公開された GitHub リポジトリをもとに調査してみました。
元ネタ：Anvil: Verifying Liveness of Cluster Management Controllers. Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. In Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI'24), Santa Clara, CA, USA, Jul. 2024.

 AnvilAnvil は、Kubernetes コントローラーの実装および形式検証をサポートする Rust フレームワークです。開発者は、実装したコントローラーが以下のような性質（仕様）を満たすことを形式的に検証できます。

活性（liveness）。例：ある Kubernetes カスタムリソースのオブジェクトについて、対応する ConfigMap がいつか必ず生成されることを保証する。

安全性（safety）。例：レプリカの数が常に減少しないことを保証する。
Anvil は仕様の検証に Verus という形式検証フレームワークを利用します。開発者は verus! マクロ でラップされた Rust コードの中に仕様や証明を直接記述し、verus コマンドを実行することで、実行コードが仕様を満たすことを検証します。仕様や証明のためのコードはゴーストコード（ghost code）と呼ばれ、実行ファイルのコンパイル時に取り除かれます。

 コントローラーの実装Anvil において、Kubernetes コントローラーは Reconciler トレイトを実装するステートマシンです。コントローラーの初期状態と状態遷移はそれぞれ reconcile_init_state と reconcile_core によって定義されます[1]。
pub trait Reconciler {
    // S: type of the reconciler state of the reconciler.
    type S;
    // K: type of the custom resource.
    type K;
    // EReq: type of request the controller sends to the external systems (if any).
    type EReq;
    // EResp: type of response the controller receives from the external systems (if any).
    type EResp;

    // reconcile_init_state returns the initial local state that the reconciler starts
    // its reconcile function with.
    // It conforms to the model's reconcile_init_state.
    fn reconcile_init_state() -> Self::S;

    // reconcile_core describes the logic of reconcile function and is the key logic we want to verify.
    // Each reconcile_core should take the local state and a response of the previous request (if any) as input
    // and outputs the next local state and the request to send to API server (if any).
    // It conforms to the model's reconcile_core.
    fn reconcile_core(cr: &Self::K, resp_o: Option<Response<Self::EResp>>, state: Self::S) -> (Self::S, Option<Request<Self::EReq>>);

    // reconcile_done is used to tell the controller_runtime whether this reconcile round is done.
    // If it is true, controller_runtime will requeue the reconcile.
    // It conforms to the model's reconcile_done.
    fn reconcile_done(state: &Self::S) -> bool;

    // reconcile_error is used to tell the controller_runtime whether this reconcile round returns with error.
    // If it is true, controller_runtime will requeue the reconcile with a typically shorter waiting time.
    // It conforms to the model's reconciler_error.
    fn reconcile_error(state: &Self::S) -> bool;
}
reconcile_core は、入力として現在の Kubernetes カスタムリソースオブジェクト cr、直前の外部システムへのリクエストに対するレスポンス resp_o、および現在の状態 state を受け取ります。そして、遷移後の状態と、外部システム（Kubernetes API サーバーやコントローラー自身が制御するシステム）に送信するリクエストを計算します。reconcile_core による状態遷移とリクエストの送受信は、Reconciler のランナーである run_controller によって繰り返し実行されます。
例えばzookeeper_controllerの場合、reconcile_core によってコントローラーの状態は初期状態InitからAfterKRequestStepに遷移し、次に実行するリクエスト（HeadlessService の取得）を返します。
このようにコントローラーをステートマシンの形式で記述するのは、仕様を TLA (Temporal Logic of Actions) によって検証するためです。Verus 自体は TLA をサポートしていないため、Anvil は TLA のモデルや述語を TLA embedding として独自に実装しています。

 コントローラーの検証一般的な Kubernetes コントローラーは、Kubernetes オブジェクトに記述された spec をもとに、管理対象のオブジェクトが望ましい状態になるよう更新します。この更新が正しく行われること、すなわちコントローラーが管理対象のオブジェクトを望ましい状態にいつか必ず更新することを保証するのが、Kubernetes コントローラーの形式検証における主な目標です。
しかし、このような仕様を妥当な形で表現するのは容易ではありません。例えば、Kubernetes オブジェクトの spec 自体が頻繁に更新されている場合、管理対象のオブジェクトが変化し続ける望ましい状態にいつまでも到達しない可能性があります。仕様はこのようなケースも想定しなければなりません。さらに、活性の性質を検証するためには、コントローラーや環境に発生しうる故障（failure）のモデリングや、非同期システムの振る舞いの公平性（fairness）をうまく仮定することが重要です。
Anvil は Kubernetes コントローラーのための汎用的な形式検証フレームワークとして、この仕様を ESR (eventually stable reconciliation) として一般化し、検証をサポートするための API や補題を提供します。

 ESRESR の仕様は、TLA の論理式によって以下のように表現されます。


\forall d.\Box(\Box\mathrm{desire}(d) \implies \Diamond\Box\mathrm{match}(d)).

ここで、d はオブジェクトの状態の記述（state description）です。\mathrm{desire}(d)はdが現在 Kubernetes オブジェクトに記述された望ましい状態と合致するときに真となり、\mathrm{match}(d)はdが管理対象のオブジェクトの状態と合致するときに真となります。\Diamond（eventually; いつか必ず）と\Box（always; 常に）は時相論理の演算子です。
ESR は、ある時点においてKubernetesオブジェクトに記述された望ましい状態が定まったとき（\Box\mathrm{desire}(d)）、それ以降のある時点から管理対象のオブジェクトがその望ましい状態dに一致する（\Diamond\Box\mathrm{match}(d)）ことを表します。外側の\Box演算子によって、Kubernetes オブジェクトの spec が変わって調停が複数回行われるケースもサポートしています。

 故障モデルAnvil は、コントローラー自身のクラッシュとリクエストの失敗という2種類の故障をモデル化しています。ただし、常に故障するモデルや一度しか故障しないモデルでは仕様を十分に評価できません。そのため、Anvil は故障は任意の回数発生しうるが、ある時点をもって発生しなくなるという仮定を採用しています。

 検証プロセス開発者は、Kubernetes コントローラーの実装が仕様を満たすことを以下のステップで検証します。
コントローラーの実装をもとに、コントローラーのモデルを作る。
コントローラーのモデルが実装に沿うことを検証する。
コントローラーのモデルが仕様を満たすことを検証する。
最初のステップでは、開発者はコントローラーの実装（reconciler::exec::Reconcilerトレイトの実装）をもとに、コントローラーのモデル（reconciler::spec::Reconcilerトレイトの実装）を作成します。コントローラーのモデルにおいて、Vec や HashMapといった要素は Verus が提供する証明に適した型（SeqやMap）に置き換えられます[2]。
2つ目のステップでは、コントローラーのモデルがコントローラーの実装を正しく模倣していることを検証します。これは、コントローラーの各メソッドにおいて、実装とモデルの返り値が同値であることを事後条件（ensure 節）として表明することで検証します（例：zookeeper_controller）。
最後に、作成したコントローラーのモデルが ESR などの仕様を満たすことを検証します。検証には Anvil が提供する環境のモデル（Kubernetels API サーバーや非同期ネットワーク）を使用します。また、開発者による証明の記述をサポートするため、Anvil は時相論理や環境の振る舞いの性質を示す約60個の補題（lemma）をライブラリとして提供しています。

 ケーススタディ著者らは広く利用されている Kubernetes オペレーターを Anvil で再実装し、ESR 等の仕様を満たすことを検証しました。検証の過程でコントローラーの実装にバグを発見し、さらにそのいくつかはオリジナルの Kubernetes オペレーターにも存在することを確認しました。

pravega/zookeeper-operatorは、Pravega が提供している ZooKeeper のための Kubernetes オペレーターです。Anvil を用いてこのオペレーターを再実装し検証する過程で、コントローラーが znode を作成する直前でクラッシュしたときにStatefulSetが更新されなくなるバグを発見しました。この活性に関するバグは本家のオペレーターにも存在する（pravega/zookeeper-operator#569）ことが確認されました。

rabbitmq/cluster-operatorは、RabbitMQ クラスターを管理する公式の Kubernetes オペレーターです。RabbitMQ クラスターのダウンサイジングにはデータロスの可能性があるので、 replicas カウントが減少しないように CRD のバリデーションルールを設定しました。しかし、Kubernetes の GC による StatefulSet の削除が遅れた場合、レプリカの数が減少してしまうバグを発見しました。

 所感Kubernetes コントローラーのような状態を扱うシステムについて、活性や安全性といった時相的な性質を検証する場合、モデルと実装を分離し、モデルのみを検証してデザインの妥当性を確認するのが主流でした。TLA+ を用いたモデル検査がその代表的な例で、TiDB の分散トランザクションの検証や、AWS DynamoDB や S3 のデザインの検証などが挙げられます。一方で、時相的な性質を検証する必要がない場合には、Dafny や F* のような、実装そのものの形式検証をサポートするツールや言語がしばしば用いられます。AWS の内部で利用されている IAM SDK 認可エンジンの検証や、暗号ライブラリのメモリ安全性の検証などがその例です。
Anvil は、Kubernetes コントローラーという実用的なシステムについて、その実装そのものが時相的な性質を満たすことを検証できるという点で先進的なプロジェクトだと思います。また、実行パスの全数検査が必要なモデル検査ではなく、Verus を利用した証明ベースのアプローチを採用している点も特筆すべきでしょう。ただ、検証のために TLA embedding を導入したり、開発者が実装とモデルを両方記述する必要がある[3]など、まだまだ導入のハードルは高いかもしれません。これらについては、Verus や Dafny のような検証フレームワーク側にブレイクスルーを期待したいところです。

脚注
論文における名前はそれぞれinitial_state、stepですが、GitHubで公開されている実装に合わせています。 ↩︎
二分探索木を検証する Verus のチュートリアルが参考になります。 ↩︎
Dafny では実装とモデルを分けて記述する代わりに、実装コードのみを記述して検証し、Java などの言語にコンパイルすることができます。しかし、Dafny が提供している seqやmapといったコレクション型が証明に特化している都合上、実行コードへのコンパイル後にパフォーマンスのボトルネックになり得ることがIAM SDK 認可エンジンの検証論文で指摘されています。 ↩︎
Anvil

コントローラーの実装

コントローラーの検証

ESR

故障モデル

検証プロセス

ケーススタディ

所感

Discussion
