Common Expression Language（CEL）

Common Expression Language（CEL）は、高速、ポータブル、安全に実行できるように設計された汎用式言語です。CEL は単独で使用することも、大規模なプロダクトに埋め込むこともできます。CEL は、リモート プロシージャ コール（RPC）のルーティングからセキュリティ ポリシーの定義まで、さまざまなアプリケーションに適しています。CEL は拡張可能で、プラットフォームに依存せず、正式に検証可能で、コンパイル 1 回/評価複数回のワークフローに最適化されています。

CEL は、ユーザーコードを安全に実行できるように特別に設計されています。ユーザーの Python コードで eval() を盲目的に呼び出すのは危険ですが、ユーザーの CEL コードは安全に実行できます。また、CEL はパフォーマンスを低下させる動作を防ぐため、ナノ秒またはマイクロ秒単位で安全に評価されます。CEL の速度と安全性は、パフォーマンスが重要なアプリケーションに最適です。

CEL は、1 行の関数やラムダ式に似た式を評価します。CEL は通常、ブール値の決定に使用されますが、JSON やプロトコル バッファ メッセージなどの複雑なオブジェクトを構築するために使用することもできます。

CEL を使用する理由

多くのサービスとアプリケーションは宣言型構成を評価します。たとえば、ロールベース アクセス制御（RBAC）は、ユーザーロールとユーザーのセットに基づいてアクセス決定を行う宣言型構成です。宣言型構成はほとんどの場合に十分ですが、より表現力が必要になることもあります。そこで CEL の出番です。

CEL で宣言型構成を拡張する例として、Google Cloud Identity and Access Management（IAM）の 機能について考えてみましょう。 RBAC は一般的なケースですが、IAM は CEL 式を提供し、ユーザーはリクエストまたはアクセスされるリソースの proto メッセージ プロパティに従って、ロールベースの付与のスコープをさらに制限できます。データモデルでこのような条件を記述すると、操作が難しい複雑な API サーフェスになります。代わりに、CEL を属性ベースのアクセス制御（ABAC）で使用すると、RBAC の表現力豊かで強力な拡張機能になります。

CEL の基本コンセプト

CEL では、式は環境に対してコンパイルされます。コンパイル ステップ では、プロトコル バッファ形式の抽象構文木（AST）が生成されます。 コンパイルされた式は、評価をできるだけ高速に保つために、後で使用できるように保存されます。1 つのコンパイル済み式を、さまざまな入力で評価できます。

これらのコンセプトについて詳しく見ていきましょう。

式

式はユーザーが記述します。式は、1 行の関数本体やラムダ式に似ています。入力を宣言する関数シグネチャは CEL 式の外側に記述され、CEL で使用できる関数のライブラリは自動的にインポートされます。

たとえば、次の CEL 式はリクエスト オブジェクトを受け取り、リクエストには claims トークンが含まれています。この式は、claims トークンがまだ有効かどうかを示すブール値を返します。

クレーム トークンを認証する CEL 式の例

// Check whether a JSON Web Token has expired by inspecting the 'exp' claim.
//
// Args:
//   claims - authentication claims.
//   now    - timestamp indicating the current system time.
// Returns: true if the token has expired.
//
timestamp(claims["exp"]) < now

ユーザーは CEL 式を定義しますが、サービスとアプリケーションは CEL 式が実行される環境を定義します。

環境

環境はサービスによって定義されます 。CEL を埋め込むサービスとアプリケーションは、式環境を宣言します。環境は、CEL 式で使用できる変数と関数のコレクションです。

たとえば、次の textproto コードは、CEL サービスの CompileRequest メッセージを使用して、request 変数と now 変数を含む環境を宣言します。

CEL 環境宣言の例

# Format: $SOURCE_PATH/service.proto#CompileRequest
declarations {
  name: "request"
  ident {
    type { message_type: "google.rpc.context.AttributeContext.Request" }
  }
}
declarations {
  name: "now"
  ident {
    type { well_known: "TIMESTAMP" }
  }
}

proto ベースの宣言は、CEL 型チェッカーによって使用され、式内のすべての識別子と関数参照が宣言され、正しく使用されていることを確認します。

式の処理フェーズ

CEL 式は次の 3 つのフェーズで処理されます。

1. 解析
2. チェック
3. 評価

CEL の最も一般的な使用パターンは、構成時に式を解析してチェックし、AST を保存して、実行時に AST を繰り返し取得して評価することです。

CEL 処理フェーズの図

CEL は、 ANTLR レキサーとパーサーの文法を使用して、人間が読める式から AST に解析されます。解析フェーズでは、proto ベースの AST が出力されます。AST 内の各 Expr ノードには、解析とチェック中に生成されたメタデータの インデックスに使用される整数 ID が含まれています。解析中に生成される syntax.protoファイルは、式の 文字列形式で入力された内容の抽象表現 を表します。

式が解析されたら、環境に対して型チェックを行い、式内のすべての変数と関数識別子が宣言され、正しく使用されていることを確認します。型チェッカーは、評価効率を大幅に向上させることができる型、変数、関数の 解決メタデータを含む checked.proto ファイルを生成します。

最後に、式が解析されてチェックされたら、保存された AST が評価されます。

CEL 評価ツールには次の 3 つが必要です。

• カスタム拡張機能の関数バインディング
• 変数バインディング
• 評価する AST

関数と変数のバインディングは、AST のコンパイルに使用されたものと一致する必要があります。これらの入力は、複数の評価で再利用できます。たとえば、多くの変数バインディングのセットで評価される AST、多くの AST に対して使用される同じ変数、プロセスのライフサイクル全体で使用される関数バインディングなどです（一般的なケース）。

正式な検証

実行時の評価に加えて、CEL 式とポリシーを正式に検証 して、考えられるすべての入力で正しさを数学的に証明できます。

Z3 定理証明ツールを搭載した CEL-Java の CEL Formal Verification Framework は、式と CEL ポリシーを Satisfiability Modulo Theories（SMT）の数式に変換して、次のことを行います。

• セキュリティ不変条件を証明する: assume 仕様と assert 仕様を使用して、入力の組み合わせに関係なく、重要なポリシーをバイパスできないことを確認します。
• 論理的な同等性を検証する: リファクタリングされた式または AI によって生成された式が、元のルールと同じように動作することを数学的に証明します。
• 包括的な有効性を適用する: ガードレール（Kubernetes Validating Admission Policies など）がすべての入力で保持されるようにするか、違反した場合は具体的な反例を生成します。
• 偽陽性を排除する: 3 パスの汚染追跡を使用して、マッピングされていないカスタム関数を分離し、報告された違反が常に再現可能なバグであることを保証します。

概要と実際の例については、Google Open Source ブログ 投稿「Securing the agentic era: Introducing formal verification for CEL」をご覧ください。

関連資料

• CEL チュートリアル
• 言語定義
• 関数リファレンス ガイド
• 正式な検証の発表
• CEL Java Verifier リポジトリ