diff --git a/verifier/BUILD.bazel b/verifier/BUILD.bazel index a7d620d1d..cc2f01810 100644 --- a/verifier/BUILD.bazel +++ b/verifier/BUILD.bazel @@ -2,14 +2,25 @@ load("@rules_java//java:defs.bzl", "java_library") package( default_applicable_licenses = ["//:license"], - default_visibility = ["//:internal"], + default_visibility = [":verifier_allow_list"], +) + +VERIFIER_ALLOW_LIST = [ + "//...", +] + +package_group( + name = "verifier_allow_list", + packages = VERIFIER_ALLOW_LIST, +) + +package_group( + name = "verifier_internal", + packages = ["//verifier/..."], ) java_library( name = "verifier", - visibility = [ - "//:internal", - ], exports = ["//verifier/src/main/java/dev/cel/verifier"], ) @@ -27,22 +38,19 @@ java_library( java_library( name = "verifier_factory", compatible_with = [], - visibility = [ - "//:internal", - ], exports = ["//verifier/src/main/java/dev/cel/verifier:verifier_factory"], ) java_library( name = "type_system", compatible_with = [], - visibility = ["//:internal"], + visibility = [":verifier_internal"], exports = ["//verifier/src/main/java/dev/cel/verifier:type_system"], ) java_library( name = "z3_impl", compatible_with = [], - visibility = ["//:internal"], + visibility = [":verifier_internal"], exports = ["//verifier/src/main/java/dev/cel/verifier:z3_impl"], ) diff --git a/verifier/README.md b/verifier/README.md index c8d838e95..db797a283 100644 --- a/verifier/README.md +++ b/verifier/README.md @@ -353,7 +353,7 @@ public class InvariantsExample { System.out.println("Invariant violated!"); System.out.println(result.message()); // Output: - // Implication violation detected. Counterexample input: + // Invariant 'always_secure' violation detected. Counterexample input: // port = 80 break; case INCONCLUSIVE: diff --git a/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifierImpl.java b/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifierImpl.java index 885201190..96473c16f 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifierImpl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifierImpl.java @@ -145,10 +145,15 @@ public ImmutableMap verifyInvariants(CelPolicy po throw new UnsupportedOperationException( "Invariants verification requires Z3 verifier implementation."); } + String invariantId = invariant.invariantId().value(); CelVerificationResult result = ((CelVerifierZ3Impl) astVerifier) - .verifyImplication(assumeAst, assertAst, boundSymbols); - resultsBuilder.put(invariant.invariantId().value(), result); + .verifyImplication( + assumeAst, + assertAst, + boundSymbols, + String.format("Invariant '%s'", invariantId)); + resultsBuilder.put(invariantId, result); } return resultsBuilder.buildOrThrow(); diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java b/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java index f243537e1..5a4c7ada6 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java @@ -33,26 +33,48 @@ public enum VerificationStatus { /** Returns the status of the verification check. */ public abstract VerificationStatus status(); + /** + * Returns the primary reason for the verification outcome. + */ + public abstract String reason(); + + /** + * Returns a detailed counterexample or satisfying model assignment, if one was found. + */ + public abstract String counterexample(); + /** * Returns a message detailing the outcome of the verification check, such as a counterexample * input, satisfying model assignments, or truncation reason. May be empty if status is VERIFIED * and no model inputs apply (e.g., when verifying isAlwaysTrue without counterexamples). */ - public abstract String message(); + public String message() { + return reason() + counterexample(); + } static CelVerificationResult verified() { - return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, ""); + return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", ""); + } + + static CelVerificationResult verified(String reason) { + return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, ""); + } + + static CelVerificationResult failed(String reason) { + return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, ""); } - static CelVerificationResult verified(String message) { - return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, message); + static CelVerificationResult failed(String reason, String counterexample) { + return new AutoValue_CelVerificationResult( + VerificationStatus.VIOLATED, reason, counterexample); } - static CelVerificationResult failed(String message) { - return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, message); + static CelVerificationResult inconclusive(String reason) { + return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, ""); } - static CelVerificationResult inconclusive(String message) { - return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, message); + static CelVerificationResult inconclusive(String reason, String counterexample) { + return new AutoValue_CelVerificationResult( + VerificationStatus.INCONCLUSIVE, reason, counterexample); } } diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index ce2705b56..510d88ec0 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -36,6 +36,7 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.List; +import java.util.Locale; import java.util.Map; import java.util.Optional; import org.jspecify.annotations.Nullable; @@ -193,23 +194,23 @@ public CelVerificationResult verifyEquivalence( switch (result.outcome) { case EXACT_MATCH: return CelVerificationResult.failed( - "Equivalence violation detected." - + getCounterexampleString( - ctx, - translator.getTypeSystem(), - result.model, - /* isApproximate= */ false, - /* isCounterexample= */ true)); + "Equivalence violation detected.", + getCounterexampleString( + ctx, + translator.getTypeSystem(), + result.model, + /* isApproximate= */ false, + /* isCounterexample= */ true)); case APPROXIMATE_MATCH: return CelVerificationResult.inconclusive( "Inconclusive: a divergence may exist, but it depends on approximations, missing" - + " theories, or loop bounds." - + getCounterexampleString( - ctx, - translator.getTypeSystem(), - result.model, - /* isApproximate= */ true, - /* isCounterexample= */ true)); + + " theories, or loop bounds.", + getCounterexampleString( + ctx, + translator.getTypeSystem(), + result.model, + /* isApproximate= */ true, + /* isCounterexample= */ true)); case TRUNCATED: return CelVerificationResult.inconclusive( "Inconclusive: expressions are equivalent within the current loop unroll limit, but" @@ -227,7 +228,8 @@ public CelVerificationResult verifyEquivalence( CelVerificationResult verifyImplication( CelAbstractSyntaxTree assumeAst, CelAbstractSyntaxTree assertAst, - Map boundSymbols) + Map boundSymbols, + String subjectName) throws CelVerificationException { Preconditions.checkArgument(assumeAst.isChecked(), "assumeAst must be type-checked."); Preconditions.checkArgument(assertAst.isChecked(), "assertAst must be type-checked."); @@ -282,27 +284,27 @@ CelVerificationResult verifyImplication( switch (result.outcome) { case EXACT_MATCH: return CelVerificationResult.failed( - "Implication violation detected." - + getCounterexampleString( - ctx, - translator.getTypeSystem(), - result.model, - /* isApproximate= */ false, - /* isCounterexample= */ true)); + String.format("%s violation detected.", subjectName), + getCounterexampleString( + ctx, + translator.getTypeSystem(), + result.model, + /* isApproximate= */ false, + /* isCounterexample= */ true)); case APPROXIMATE_MATCH: return CelVerificationResult.inconclusive( "Inconclusive: a counterexample may exist, but it depends on approximations, missing" - + " theories, or loop bounds." - + getCounterexampleString( - ctx, - translator.getTypeSystem(), - result.model, - /* isApproximate= */ true, - /* isCounterexample= */ true)); + + " theories, or loop bounds.", + getCounterexampleString( + ctx, + translator.getTypeSystem(), + result.model, + /* isApproximate= */ true, + /* isCounterexample= */ true)); case TRUNCATED: return CelVerificationResult.inconclusive( - "Inconclusive: implication holds within the current loop unroll limit, but" - + " may be violated for larger collections."); + String.format("Inconclusive: %s holds within the current loop unroll limit, but" + + " may be violated for larger collections.", subjectName.toLowerCase(Locale.US))); case NO_MATCH: return CelVerificationResult.verified(); case SOLVER_UNKNOWN: @@ -345,13 +347,13 @@ private CelVerificationResult checkSatisfiability( case EXACT_MATCH: return searchForCounterexample ? CelVerificationResult.failed( - "Condition is not always true." - + getCounterexampleString( - ctx, - translator.getTypeSystem(), - result.model, - /* isApproximate= */ false, - /* isCounterexample= */ true)) + "Condition is not always true.", + getCounterexampleString( + ctx, + translator.getTypeSystem(), + result.model, + /* isApproximate= */ false, + /* isCounterexample= */ true)) : CelVerificationResult.verified( "Condition is satisfiable." + getCounterexampleString( @@ -369,13 +371,13 @@ private CelVerificationResult checkSatisfiability( : "Inconclusive: a satisfying model may exist, but it depends on" + " approximations, missing theories, or loop bounds."; return CelVerificationResult.inconclusive( - prefix - + getCounterexampleString( - ctx, - translator.getTypeSystem(), - result.model, - /* isApproximate= */ true, - /* isCounterexample= */ searchForCounterexample)); + prefix, + getCounterexampleString( + ctx, + translator.getTypeSystem(), + result.model, + /* isApproximate= */ true, + /* isCounterexample= */ searchForCounterexample)); case TRUNCATED: return CelVerificationResult.inconclusive( diff --git a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java index 09f205f04..5a9eaea02 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java @@ -526,7 +526,8 @@ public void verifyInvariants_workloadAdmissionFlawed_violationsDetected() throws .isEqualTo(VerificationStatus.VIOLATED); assertThat(results.get("universal_no_unapproved_privileged_prod").message()) .isEqualTo( - "Implication violation detected. Counterexample input:\n" + "Invariant 'universal_no_unapproved_privileged_prod' violation detected." + + " Counterexample input:\n" + " is_owner = false\n" + " is_privileged = true\n" + " is_prod = true\n" diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 20b410a5c..7f9f61520 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -2604,7 +2604,7 @@ public void verifyImplication_loopExceedsLimit_returnsTruncatedInconclusive() th CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(2).build(); CelVerificationResult result = ((CelVerifierZ3Impl) verifier) - .verifyImplication(assumeAst, assertAst, ImmutableMap.of()); + .verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Implication"); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); assertThat(result.message())