一般運算語言 (CEL) 是一種一般用途運算式語言,可快速、安全地執行,且具備可攜性。您可以單獨使用 CEL,也可以將其嵌入較大的產品。CEL 適用於各種應用程式,從遠端程序呼叫 (RPC) 的路徑到定義安全政策,都能派上用場。CEL 可擴充、不限平台、可正式驗證,且已針對編譯一次/評估多次的工作流程進行最佳化。
CEL 的設計宗旨是安全地執行使用者程式碼。盲目呼叫使用者 Python 程式碼中的 eval() 相當危險,但您可以安全地執行使用者的 CEL 程式碼。此外,CEL 會避免導致效能降低的行為,因此評估作業可在奈秒或微秒內安全完成。CEL 的速度和安全性非常適合用於效能至關重要的應用程式。
CEL 會評估類似單行函式或 lambda 運算式的運算式。雖然 CEL 通常用於布林決策,但您也可以使用 CEL 建構更複雜的物件,例如 JSON 或通訊協定緩衝區訊息。
為什麼要使用 CEL?
許多服務和應用程式都會評估宣告式設定。舉例來說,角色式存取控管 (RBAC) 是一種宣告式設定,可根據使用者角色和一組使用者產生存取決策。雖然宣告式設定檔在大多數情況下都足夠使用,但有時您需要更強大的表達能力。這時 CEL 就能派上用場。
以使用 CEL 擴充宣告式設定為例,請考慮 Google Cloud Identity and Access Management (IAM) 的功能。雖然 RBAC 是常見情況,但 IAM 提供 CEL 運算式,可讓使用者根據要求或存取資源的 Proto 訊息屬性,進一步限制角色型授權的範圍。透過資料模型描述這類條件,會導致 API 介面複雜難用。相較之下,搭配屬性式存取控管 (ABAC) 使用 CEL,是 RBAC 的強大擴充功能,可提供更豐富的控制選項。
CEL 的核心概念
在 CEL 中,運算式會根據環境編譯。編譯步驟會產生 通訊協定緩衝區 格式的抽象語法樹 (AST)。編譯後的運算式會儲存起來,供日後使用,盡可能加快評估速度。單一編譯運算式可使用多種不同的輸入內容進行評估。
以下將進一步說明這些概念。
運算式
運算式是由使用者撰寫。運算式類似於單行函式主體或 lambda 運算式。宣告輸入內容的函式簽章會寫在 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 運算式。
舉例來說,下列 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" }
}
}
CEL 型別檢查程式會使用以 Proto 為基礎的宣告,確保運算式中的所有 ID 和函式參照都已宣告,且使用方式正確。
運算式處理階段
系統會分三個階段處理 CEL 運算式:
- 剖析
- 檢查
- 評估
最常見的 CEL 用法是在設定時剖析及檢查運算式、儲存 AST,然後在執行階段重複擷取及評估 AST。
CEL 處理階段的插圖

CEL 會使用 ANTLR 詞法分析器和剖析器文法,從人類可解讀的運算式剖析為 AST。剖析階段會發出以 Proto 為基礎的 AST,其中 AST 中的每個 Expr 節點都包含整數 ID,用於編入剖析和檢查期間產生的中繼資料。剖析期間產生的 syntax.proto 檔案,代表以字串形式輸入的運算式抽象表示法。
剖析運算式後,系統會根據環境進行型別檢查,確保運算式中的所有變數和函式 ID 都已宣告,且使用方式正確。型別檢查器會產生 checked.proto 檔案,其中包含型別、變數和函式解析中繼資料,可大幅提升評估效率。
最後,在剖析及檢查運算式後,系統會評估儲存的 AST。
CEL 評估工具需要三項資訊:
- 任何自訂擴充功能的函式繫結
- 變數繫結
- 要評估的 AST
函式和變數繫結應與用於編譯 AST 的繫結相符。這些輸入內容都可以在多項評估中重複使用,例如在多組變數繫結中評估的 AST、用於多個 AST 的相同變數,或是在程序生命週期中使用的函式繫結 (常見情況)。
正式驗證
除了執行階段評估外,CEL 運算式和政策也可以正式驗證,以數學方式證明所有可能輸入內容的正確性。
Z3 定理驗證器支援的 CEL 正式驗證框架會將 CEL-Java 中的運算式和 CEL 政策轉換為可滿足模數理論 (SMT) 公式,以執行下列操作:
- 證明安全不變量:使用
assume和assert規格,驗證在任何輸入組合下,重要政策都不會遭到規避。 - 驗證邏輯等價:以數學方式證明重構或 AI 生成的運算式,行為與原始規則完全相同。
- 強制執行詳盡的有效性:確保所有輸入內容都符合安全防護措施 (例如 Kubernetes 驗證許可政策),或在違規時產生具體的反例。
- 排除誤判:採用三階段汙染追蹤功能,隔離未對應的自訂函式,確保回報的違規事項一律是可重現的錯誤。
如需簡介和實際範例,請參閱 Google 開放原始碼網誌文章:Securing the agentic era: Introducing formal verification for CEL (確保 AI 代理時代安全:推出 CEL 的正式驗證)。