From ff7bccfe61d49894e156c1e994a2c4f161627340 Mon Sep 17 00:00:00 2001 From: Sokwhan Huh Date: Fri, 17 Jul 2026 21:19:31 -0700 Subject: [PATCH] Open source the CEL formal verification framework PiperOrigin-RevId: 949908577 --- .../cross_artifact_dependencies_check.sh | 1 + MODULE.bazel | 1 + publish/BUILD.bazel | 33 ++ verifier/README.md | 304 ++++++++++++++++++ .../main/java/dev/cel/verifier/BUILD.bazel | 7 +- .../java/dev/cel/verifier/axioms/BUILD.bazel | 5 +- 6 files changed, 349 insertions(+), 2 deletions(-) create mode 100644 verifier/README.md diff --git a/.github/workflows/cross_artifact_dependencies_check.sh b/.github/workflows/cross_artifact_dependencies_check.sh index 0802a299a..de213e125 100755 --- a/.github/workflows/cross_artifact_dependencies_check.sh +++ b/.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 "------------------------------------------------" diff --git a/MODULE.bazel b/MODULE.bazel index fcaf041ba..ce9c67fde 100644 --- a/MODULE.bazel +++ b/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", diff --git a/publish/BUILD.bazel b/publish/BUILD.bazel index 69622aada..185c7fb7d 100644 --- a/publish/BUILD.bazel +++ b/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"], +) diff --git a/verifier/README.md b/verifier/README.md new file mode 100644 index 000000000..a5889d5db --- /dev/null +++ b/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. + +--- diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index 09a2039b4..6cdb793db 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/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", ], ) diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel index d5f9bf74a..02752c10e 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel @@ -2,7 +2,10 @@ load("@rules_java//java:defs.bzl", "java_library") package( default_applicable_licenses = ["//:license"], - default_visibility = ["//verifier/axioms:__pkg__"], + default_visibility = [ + "//publish:__pkg__", + "//verifier/axioms:__pkg__", + ], ) java_library(