Open source the CEL formal verification framework

.github/workflows/cross_artifact_dependencies_check.sh

@@ -22,6 +22,7 @@ TARGETS=(
   "//publish:cel_runtime"
   "//publish:cel_protobuf"
   "//publish:cel_v1alpha1"
+  "//publish:cel_verifier"
 )
 
 echo "------------------------------------------------"

MODULE.bazel

@@ -98,6 +98,7 @@ maven.install(
         "org.jspecify:jspecify:1.0.0",
         "org.threeten:threeten-extra:1.8.0",
         "org.yaml:snakeyaml:2.5",
+        "tools.aqua:z3-turnkey:4.14.1",
     ],
     repositories = [
         "https://maven.google.com",

publish/BUILD.bazel

@@ -130,6 +130,18 @@ BUNDLE_TARGETS = [
 
 CEL_MISC_TARGETS = BUNDLE_TARGETS + EXTENSION_TARGETS + OPTIMIZER_TARGETS + VALIDATOR_TARGETS + POLICY_COMPILER_TARGETS
 
+# keep sorted
+VERIFIER_TARGETS = [
+    "//verifier/src/main/java/dev/cel/verifier",
+    "//verifier/src/main/java/dev/cel/verifier:policy_verifier",
+    "//verifier/src/main/java/dev/cel/verifier:policy_verifier_factory",
+    "//verifier/src/main/java/dev/cel/verifier:policy_verifier_impl",
+    "//verifier/src/main/java/dev/cel/verifier:type_system",
+    "//verifier/src/main/java/dev/cel/verifier:verifier_factory",
+    "//verifier/src/main/java/dev/cel/verifier:z3_impl",
+    "//verifier/src/main/java/dev/cel/verifier/axioms",
+]
+
 # Excluded from the JAR as their source of truth is elsewhere
 EXCLUDED_TARGETS = [
     "@com_google_googleapis//google/api/expr/v1alpha1:expr_java_proto",
@@ -316,3 +328,24 @@ java_export(
     pom_template = ":cel_runtime_android_pom",
     exports = LITE_RUNTIME_TARGETS,
 )
+
+pom_file(
+    name = "cel_verifier_pom",
+    substitutions = {
+        "CEL_VERSION": CEL_VERSION,
+        "CEL_ARTIFACT_ID": "verifier",
+        "PACKAGE_NAME": "CEL Java Verifier",
+        "PACKAGE_DESC": "Formal verification tools for Common Expression Language for Java.",
+    },
+    targets = VERIFIER_TARGETS,
+    template_file = "pom_template.xml",
+)
+
+java_export(
+    name = "cel_verifier",
+    deploy_env = EXCLUDED_TARGETS,
+    javadocopts = JAVA_DOC_OPTIONS,
+    maven_coordinates = "dev.cel:verifier:%s" % CEL_VERSION,
+    pom_template = ":cel_verifier_pom",
+    exports = VERIFIER_TARGETS + [":cel"],
+)

verifier/README.md

@@ -0,0 +1,304 @@
+# CEL Java Verifier
+
+The **CEL Java Verifier** is a formal verification framework for CEL Java,
+designed to statically prove semantic properties of CEL expressions and
+policies.
+
+Powered by the [Z3 SMT solver](https://github.com/Z3Prover/z3), the verifier
+translates CEL Abstract Syntax Trees (ASTs) into mathematical formulas to prove
+equivalence, satisfiability, and validity without executing the expressions.
+
+---
+
+## Overview
+
+CEL is side-effect free with guaranteed termination, but as expressions grow in
+complexity, ensuring correctness under all possible inputs becomes challenging.
+The CEL Verifier addresses this by allowing you to mathematically prove
+properties about your expressions.
+
+### Common Use Cases
+
+*   **Compliance Auditing:** Statically prove that a critical resource is
+    mathematically protected (e.g., "prove that access is never allowed unless
+    `request.auth.claims.role == 'admin'`").
+*   **Optimization & Safe Refactoring:** Verify that a simplified or optimized
+    version of an expression behaves identically to the original version for
+    all possible inputs.
+*   **Dead Code Detection:** Identify branches in an expression that can never
+    be reached (are unsatisfiable).
+
+---
+
+## Key Features
+
+*   **Satisfiability & Validity Proving:** Check if an expression can ever
+    evaluate to `true` (satisfiability) or if it is guaranteed to always be
+    `true` (validity).
+*   **Logical Equivalence:** Prove that two different ASTs or Policies are
+    semantically identical.
+*   **Bounded Model Checking (BMC):** Safely verify list and map comprehensions
+    (`all`, `exists`, `map`, `filter`) by statically unrolling them up to a
+    configurable limit.
+*   **Counterexample Generation:** When verification fails (e.g., two
+    expressions are not equivalent), the verifier generates a human-readable
+    counterexample showing the inputs that caused the mismatch.
+*   **Partial Evaluation (Unknowns) Support:** Define variables that are
+    permitted to evaluate to `Unknown` during verification, mirroring CEL's
+    runtime partial evaluation.
+
+```java
+CelVerifier verifier = CelVerifierFactory.newVerifier()
+    .addUnknownIdentifier("request.headers") // Exclude dynamic fields from failure paths
+    .build();
+```
+
+---
+
+## Upcoming Capabilities
+
+The following features are planned for future releases:
+
+*   **Custom Invariants Verification:** Allows policy authors to define safety
+    invariants (e.g., "port must always be secure if external access is
+    allowed") and mathematically prove that the policy never violates them.
+*   **Deep Reachability Analysis:** Statically analyzes nested policy rules
+    to detect unreachable execution paths (dead code) that can never be
+    executed under any input.
+*   **Rule Shadowing & Independence Detection:** Detects when sibling rules
+    in a policy conflict or shadow each other (i.e., a rule is partially or
+    fully shadowed by a preceding rule with overlapping conditions), ensuring
+    deterministic and intended policy routing.
+
+---
+
+## Usage
+
+### 1. AST Equivalence Verification
+
+The following example demonstrates how to verify if two CEL expressions
+are logically equivalent.
+
+```java
+import dev.cel.common.CelAbstractSyntaxTree;
+import dev.cel.common.types.SimpleType;
+import dev.cel.compiler.CelCompiler;
+import dev.cel.compiler.CelCompilerFactory;
+import dev.cel.verifier.CelVerificationException;
+import dev.cel.verifier.CelVerificationResult;
+import dev.cel.verifier.CelVerificationResult.VerificationStatus;
+import dev.cel.verifier.CelVerifier;
+import dev.cel.verifier.CelVerifierFactory;
+import java.time.Duration;
+
+public class VerifierExample {
+  public static void main(String[] args) throws Exception {
+    CelCompiler compiler = CelCompilerFactory.standardCelCompilerBuilder()
+        .addVar("x", SimpleType.INT)
+        .build();
+
+    // Compile two logically equivalent expressions
+    CelAbstractSyntaxTree astA = compiler.compile("x > 10").getAst();
+    CelAbstractSyntaxTree astB = compiler.compile("10 < x").getAst();
+
+    // Create and configure the verifier
+    CelVerifier verifier = CelVerifierFactory.newVerifier()
+        .setTimeout(Duration.ofSeconds(2))
+        .build();
+
+    CelVerificationResult result;
+    try {
+      // Verify equivalence
+      result = verifier.verifyEquivalence(astA, astB);
+    } catch (CelVerificationException e) {
+      System.out.println("Verification failed or timed out: " + e.getMessage());
+      return;
+    }
+
+    if (result.status() == VerificationStatus.VERIFIED) {
+      System.out.println("Expressions are logically equivalent!");
+    } else if (result.status() == VerificationStatus.VIOLATED) {
+      System.out.println(result.message());
+      // Example output if expressions were NOT equivalent:
+      // Equivalence violation detected. Counterexample input:
+      //   x = ...
+    } else {
+      // INCONCLUSIVE means the solver could not positively confirm VERIFIED or VIOLATED
+      // due to things like loop truncation (BMC) or uninterpreted functions.
+      System.out.println("Verification was inconclusive: " + result.message());
+    }
+  }
+}
+```
+
+### 2. Policy Equivalence Verification
+
+You can also verify the equivalence of two structured CEL Policies.
+
+```java
+import dev.cel.bundle.Cel;
+import dev.cel.bundle.CelFactory;
+import dev.cel.common.types.SimpleType;
+import dev.cel.policy.CelPolicy;
+import dev.cel.policy.CelPolicyCompiler;
+import dev.cel.policy.CelPolicyCompilerFactory;
+import dev.cel.policy.CelPolicyParser;
+import dev.cel.policy.CelPolicyParserFactory;
+import dev.cel.verifier.CelPolicyVerifier;
+import dev.cel.verifier.CelPolicyVerifierFactory;
+import dev.cel.verifier.CelVerificationException;
+import dev.cel.verifier.CelVerificationResult;
+import dev.cel.verifier.CelVerificationResult.VerificationStatus;
+import dev.cel.verifier.CelVerifier;
+import dev.cel.verifier.CelVerifierFactory;
+
+public class PolicyVerifierExample {
+  private static final Cel CEL = CelFactory.standardCelBuilder()
+      .addVar("role", SimpleType.STRING)
+      .addVar("country", SimpleType.STRING)
+      .addVar("port", SimpleType.INT)
+      .build();
+
+  private static final CelPolicyParser PARSER = CelPolicyParserFactory.newYamlParserBuilder()
+      .enableSimpleVariables(true)
+      .build();
+
+  private static final CelPolicyCompiler POLICY_COMPILER =
+      CelPolicyCompilerFactory.newPolicyCompiler(CEL).build();
+
+  // Verifiers are immutable and thread-safe, making them safe to store as static constants
+  private static final CelVerifier AST_VERIFIER = CelVerifierFactory.newVerifier().build();
+
+  private static final CelPolicyVerifier POLICY_VERIFIER =
+      CelPolicyVerifierFactory.newVerifier(POLICY_COMPILER, AST_VERIFIER).build();
+
+  public static void main(String[] args) throws Exception {
+    // Define legacy policy (single complex expression)
+    String yamlLegacy = """
+        name: legacy_authz
+        rule:
+          match:
+            - output: '(role == "admin" || (role == "editor" && country == "US")) && port == 443'
+        """;
+
+    // Define refactored policy with a bug (missing country check)
+    String yamlRefactored = """
+        name: refactored_authz
+        rule:
+          variables:
+            - is_admin: 'role == "admin"'
+            - is_editor: 'role == "editor"' # Bug: Missing country == 'US' check!
+            - is_secure: 'port == 443'
+          match:
+            - output: '(variables.is_admin || variables.is_editor) && variables.is_secure'
+        """;
+
+    // Parse both policies
+    CelPolicy policyLegacy = PARSER.parse(yamlLegacy);
+    CelPolicy policyRefactored = PARSER.parse(yamlRefactored);
+
+    CelVerificationResult result;
+    try {
+      // Verify equivalence
+      result = POLICY_VERIFIER.verifyEquivalence(policyLegacy, policyRefactored);
+    } catch (CelVerificationException e) {
+      System.out.println("Verification failed or timed out: " + e.getMessage());
+      return;
+    }
+
+    if (result.status() == VerificationStatus.VERIFIED) {
+      System.out.println("Policies are equivalent!");
+    } else if (result.status() == VerificationStatus.VIOLATED) {
+      System.out.println("Refactoring bug detected!");
+      System.out.println(result.message());
+      // Output:
+      // Equivalence violation detected. Counterexample input:
+      //   country = "a"
+      //   role = "editor"
+      //   port = 443
+    } else {
+      System.out.println("Verification was inconclusive: " + result.message());
+    }
+  }
+}
+```
+
+---
+
+## Limitations & Best Practices
+
+### Limitations
+
+*   **Cross-Type Numeric Comparisons:**
+    *   **Equality (`==`, `!=`):** Equality comparisons between different
+        numeric types (e.g., `int` vs `double` or `uint` vs `double`) are
+        currently not supported and will evaluate to `false` during
+        verification, even if they have the same mathematical value (e.g.,
+        `dyn(1) == dyn(1.0)` is false). Note that `int` vs `uint` equality *is*
+        supported.
+    *   **Relational Operators (`<`, `>`, `<=`, `>=`):** Cross-type relational
+        comparisons are fully supported mathematically across all numeric
+        combinations (`int`, `uint`, and `double`).
+*   **Unsupported Standard Functions (Uninterpreted Functions):** Not all
+    CEL standard library functions have SMT axioms defined yet. Unsupported
+    functions are treated as *uninterpreted functions* by Z3 (the solver
+    only guarantees that identical inputs yield identical outputs, but does
+    not understand the function's internal logic or return types).
+    Consequently, verifications that rely on the specific semantics of
+    these functions may return `VerificationStatus.INCONCLUSIVE`. Support for
+    more standard library functions will be added incrementally.
+
+### Best Practices & Performance
+
+*   **Prefer Strong Typing over `dyn`:** Always declare variables with
+    specific concrete types (e.g., `int`, `string`, `bool`, or specific
+    protobuf message types). Omitting the type or using `dyn` forces the
+    verifier to perform expensive runtime type checks symbolically across
+    multiple theories, which significantly slows down verification. Using
+    concrete types allows Z3 to use specialized solvers directly for much
+    faster results.
+*   **Avoid Floating Point Numbers:** Using floating point numbers in your
+    CEL expressions can significantly increase the time it takes for the
+    verifier to produce a result. It is recommended to use integers for all
+    counting and comparison logic unless floating point precision is
+    explicitly required.
+
+---
+
+## Configuration & Tuning
+
+### Timeouts
+
+SMT solving is NP-complete and can theoretically stop responding or take an
+exponential amount of time for complex formulas.
+The verifier uses a default timeout of 10 seconds. It is recommended to
+configure this to a reasonable duration for your specific use case using
+`setTimeout(Duration)`. Note that this is a soft timeout evaluated periodically
+by the Z3 solver during its search phase.
+If the solver times out, the verifier will throw a `CelVerificationException`
+which should be explicitly caught and handled by the caller.
+
+### Comprehensions and Bounded Model Checking
+
+Because CEL lists/maps can be dynamically sized, the verifier cannot
+statically evaluate loops of infinite or unknown size.
+To handle comprehensions (`all`, `exists`, `map`, `filter`), the verifier uses
+Bounded Model Checking (BMC) to statically unroll loops up to a limit
+configured via `setComprehensionUnrollLimit(int)` (defaults to 5).
+
+What this means for verification:
+
+*   **Equivalence Checking:** Works seamlessly out-of-the-box for refactored
+    policies containing matching comprehensions, as both sides are unrolled
+    to the same limit.
+*   **Inconclusive Verification:** Expressions with comprehensions over
+    unconstrained dynamic lists will safely evaluate to `Unknown` for
+    inputs exceeding the unroll limit. If the verifier cannot definitively
+    prove or disprove a property for all possible list sizes (e.g., when
+    checking `isAlwaysTrue` or `isSatisfiable`), it will return
+    `VerificationStatus.INCONCLUSIVE`.
+*   **Warning:** Setting the unroll limit too high will exponentially
+    increase verification time and memory usage. Prefer keeping it near the
+    default unless you have a specific need and bounded inputs.
+
+---

verifier/src/main/java/dev/cel/verifier/BUILD.bazel

@@ -2,7 +2,10 @@ load("@rules_java//java:defs.bzl", "java_library")
 
 package(
     default_applicable_licenses = ["//:license"],
-    default_visibility = ["//verifier:__pkg__"],
+    default_visibility = [
+        "//publish:__pkg__",
+        "//verifier:__pkg__",
+    ],
 )
 
 java_library(
@@ -19,6 +22,7 @@ java_library(
         "//:auto_value",
         "//common:cel_ast",
         "//common/types:type_providers",
+        "@maven//:com_google_errorprone_error_prone_annotations",
     ],
 )
 
@@ -119,6 +123,7 @@ java_library(
         "//verifier/axioms",
         "@maven//:com_google_errorprone_error_prone_annotations",
         "@maven//:com_google_guava_guava",
+        "@maven//:org_jspecify_jspecify",
         "@maven//:tools_aqua_z3_turnkey",
     ],
 )