feat(prover): support REST query parameter containment

[kirit93]

Summary

Add generic REST query-parameter containment to the standalone policy prover. This lets it distinguish requests with the same method and path but different query values, such as Git discovery requests for service=git-upload-pack versus service=git-receive-pack.

Also improve counterexample search so a straightforward permission expansion in a later rule can be found before falling through to a slow solver check.

Related Issue

No directly matching accepted issue is linked yet. Maintainer resolution of this requirement is still needed before merge.

Changes

Query containment

• Support exact ASCII query values and the whole * wildcard on REST allow and deny rules.
• Match the existing runtime semantics: * uses . as a delimiter, so it matches an empty value or a/b, but not a.b. Both the structural shortcut and symbolic model respect this distinction.
• Keep wildcard-matching and nonmatching values separate in the finite model and decoded counterexamples.
• Preserve required-key presence, empty values, and repeated-parameter semantics: all values must match an allow constraint; any matching value satisfies each configured deny constraint.
• Include decoded query_params in network counterexamples and CLI JSON/text output; omit the map when empty.
• Limit query matchers to 256 across both policies and count their keys and values toward existing pattern-size limits.
• Keep partial globs, any matchers, non-ASCII policy literals, and embedded NULs unsupported. Do not infer application-specific read/write ordering.

Counterexample search

• Try requests from multiple candidate allow rules, including required query values.
• Replay each request against both complete policies before reporting a violation.
• Limit probing to eight endpoints, 64 rules, and 64 request replays per binary-identity mode, sharing the solver deadline and cancellation flag.
• Fall back to the solver when probing finds no violation; probes never establish containment.

Review follow-up

Addresses the code and documentation findings in the panel review:

• Add regressions for both reported false-containment cases: wildcard allow versus dotted exact allow, and dotted exact deny versus wildcard deny.
• Replay the resulting counterexamples against the actual runtime Rego allow_request rule.
• Compare mixed repeated values such as ["a", "a.b"] against runtime query matching, and test solver decoding of both matching and nonmatching values.
• Update the existing architecture overview, prover README, and reference documentation with supported query semantics, decoded output, and combined-input limits.

No runtime glob behavior, dependencies, or POC code is changed.

Testing

• cargo test --locked -p openshell-prover -p openshell-prover-cli: 147 unit/integration tests and one doc test passed using local system Z3.
• Query allow/deny, missing/empty/repeated values, unsupported shapes, and resource-limit coverage.
• Dotted-value and mixed-repeat regressions, runtime Rego parity, and CLI counterexample tests.
• GitHub regression tests covering all 24 rule orderings, probe exhaustion, cancellation, and solver fallback.
• Focused Clippy with --all-targets -- -D warnings.
• Rust formatting and git diff --check.
• mise run pre-commit passed, including workspace Rust linting, format checks, Markdown/Mermaid lint, license checks, and Python/TypeScript/Helm/protobuf/lockfile checks.
• Full repository CI and E2E validation.

Checklist

• Conventional Commits with DCO sign-off.
• Existing architecture and reference documentation updated.
• No runtime behavior changes, dependency changes, or unrelated refactoring.
• Accepted issue linked.

[copy-pr-bot]

Auto-sync is disabled for draft pull requests in this repository. Workflows must be run manually.

Contributors can view more details about this message here.

[johnnygreco]

Panel review: OpenShell PR #3533

Result: changes required before merge. The panel found one high-severity policy-modeling defect that can produce a false containment proof, plus an incomplete documentation update. The PR also lacks the accepted issue required by repository conventions. No PR code, commits, branches, or GitHub discussion were changed.

Reviewed September 22, 2026: feat(prover): support REST query parameter containment.

Findings

High: query * does not have the runtime meaning assumed by the prover

Locations: query.rs:66, query.rs:170–177.

Before this PR, query-constrained policies were unsupported. With this PR, a boundary allowing q: "*" and an otherwise identical candidate allowing q: "a.b" produce within_boundary and exit code 0. At runtime, /?q=a.b is rejected by the boundary and allowed by the candidate. A caller relying on the prover can therefore approve a policy expansion incorrectly.

The runtime calls glob.match(matcher, [], value) in sandbox-policy.rego:742–745. The pinned Regorus 0.9.1 implementation interprets an empty delimiter list as the default . delimiter. Consequently, * does not match a.b.

Both new modeling paths make the same incorrect assumption:

• The structural shortcut accepts every supported candidate matcher under a boundary *, including dotted exact literals.
• The symbolic model treats * as key presence. Its single “other value” class combines values with different runtime matching behavior. Wildcard allow rules also need all repeated values to match, while wildcard deny rules need any value to match. For q=["a", "a.b"], runtime wildcard allow is false and wildcard deny is true; presence alone cannot express that distinction.

The lead independently reproduced the CLI result and ran the reviewer's reproduction against the actual runtime Rego allow_request rule. Results for q=["a.b"] were:

Case	Boundary	Candidate	Runtime boundary allows	Runtime candidate allows	Prover
Allow	Allow q: "*"	Allow q: "a.b"	false	true	within_boundary
Deny	Unrestricted allow; deny q: "a.b"	Unrestricted allow; deny q: "*"	false	true	within_boundary

The deny case also exercises the symbolic path because boundary denies disable the structural shortcut. The lead confirmed its CLI result without solver warnings using /** paths. An earlier exact / version emitted warnings from the installed system Z3; that earlier invocation is not needed for the finding. The primary allow case returns through the structural shortcut and does not depend on solver behavior.

Smallest appropriate correction: preserve runtime semantics and make the finite abstraction distinguish wildcard-matching and nonmatching values; use all/any matching for allow/deny rules and correct the structural implication check. A conservative alternative is to return unsupported for * until it is modeled correctly. Add focused dotted-value and mixed-repeat runtime parity regressions. Changing runtime glob semantics or introducing a general glob framework would exceed this PR's scope.

Low: update the existing prover contract documentation

The new supported query forms, decoded query_params output, and aggregate limit of 256 query matchers are missing from the authoritative documentation:

• docs/reference/policy-prover.mdx:124 omits query_params from network counterexamples; its coverage description at line 164 remains method/path-only and its limits at line 175 omit query matchers.
• architecture/security-policy.md:396–398 retains the previous coverage description.
• crates/openshell-prover/README.md:22 does not include the new query literal restrictions in its scope description.

For example, comparing identical policies with 129 query matchers now exceeds the combined-input limit, despite satisfying the published numeric limits. The PR explicitly excludes documentation, but AGENTS.md requires relevant published and architecture updates for user-facing behavior changes.

Minimal correction: update those existing contract descriptions with the final supported semantics, repeated-value behavior, decoded output and empty-map omission, and the combined-input matcher limit. No new documentation structure or unrelated skill changes are needed.

Repository readiness

The PR body acknowledges that no accepted issue is linked. Repository conventions require an accepted issue for a new feature or user-visible behavior. A maintainer must resolve that gate; the review did not create an issue, apply acceptance labels, or expand the feature scope.

Other checked conventions were followed: the commit is conventional and DCO-signed; the new module has appropriate ownership and license headers; the public counterexample addition uses the existing non-exhaustive API pattern; tests follow existing fixture and integration conventions. Relevant sync-agent-infra maintenance routing found no stale standalone-prover contract in agent skills and no inventory changes requiring broader synchronization.

The PR body describes draft submission, but GitHub reported draft: false at final verification. The available CI snapshot includes successful lint, DCO, and vouch checks, while the main PR test/build and E2E jobs were skipped. Green aggregate statuses therefore do not establish that those suites ran. Repository-wide local CI and E2E were not run during this review.

Panel and scope control

Three independent reviewers inspected the same frozen target concurrently:

Reviewer	Scope	Result
Policy-model soundness	Finite abstraction, runtime equivalence, structural implication, witness realizability, containment security	Wildcard soundness finding
Probe and integration	Complete-policy replay, budgets, cancellation/deadline, solver fallback, CLI output, regression coverage	No independent findings
Implementation clarity and conventions	Modeling clarity, ownership, complexity, repository patterns, docs and skill maintenance	Documentation finding

The lead monitored progress, requested concrete reproductions, independently verified findings, consolidated duplicated documentation observations, and kept proposed corrections at the existing model boundary. No broad refactor, runtime behavior change, unsupported matcher expansion, or new abstraction was requested.

The exact-only abstraction, missing versus empty values, repeated-value sets, conjunction across keys, validation before shortcuts, bounded probing, full-policy replay, and conservative solver fallback had no additional confirmed findings. The code is generally cohesive; the high-severity finding concerns semantic correctness rather than implementation style.

No relevant core review lens was omitted: correctness/security, tests, maintainability, CLI experience, documentation, and API/integration concerns were covered across the three reviewers. Separate deployment, database migration, dependency/supply-chain, GUI accessibility, and FFI reviews were inapplicable to this diff. Performance review was limited to the changed probe/model bounds; no benchmark project was warranted.

One review round was completed, with no code edits or reruns. Findings remain unresolved because this was a review-and-report task. All reviewer sessions were concluded after their results were captured.

Validation

Run from the isolated checkout at the reviewed head:

cargo test --locked -p openshell-prover -p openshell-prover-cli --target-dir /tmp/pr3533-target
git diff --check fa8f6d394983b541ac31363f8a2d5ea027b08acf 48e12bdbf15d7f202456b6bcc9667cc6cdebe85d

• Focused tests: 146 unit/integration tests and 1 doc test passed, using installed system Z3 4.8.12.
• Diff whitespace check: passed.
• Actual runtime Rego reproduction: boundary rejects and candidate allows the dotted query, for both allow and deny examples.
• Existing query parity tests pass but omit dotted wildcard behavior; passing tests do not resolve the soundness finding.
• Reviewed checkout remained clean. The only workspace deliverable is this report.

Reproduce the primary finding

At the reviewed commit, create these two authored policies and run the CLI. They differ only in the query constraint:

cat > /tmp/pr3533-boundary.json <<'EOF'
{"version":1,"network_policies":{"n":{"endpoints":[{"host":"example.com","port":443,"protocol":"rest","enforcement":"enforce","rules":[{"allow":{"method":"GET","path":"/","query":{"q":"*"}}}]}]}}}
EOF
cat > /tmp/pr3533-candidate.json <<'EOF'
{"version":1,"network_policies":{"n":{"endpoints":[{"host":"example.com","port":443,"protocol":"rest","enforcement":"enforce","rules":[{"allow":{"method":"GET","path":"/","query":{"q":"a.b"}}}]}]}}}
EOF
cargo run --locked -p openshell-prover-cli --bin openshell-prover -- check /tmp/pr3533-candidate.json --boundary /tmp/pr3533-boundary.json --output json

Observed: result: "within_boundary", exit_code: 0. Correct result with complete modeling: exceeds_boundary, because GET /?q=a.b distinguishes the policies. A conservative unsupported result is also preferable to an unsound proof.

For runtime verification, load the checked-in supervisor Rego with normalized endpoint ports: [443], set the policy's runtime binary-identity configuration, and evaluate data.openshell.sandbox.allow_request on the same request with decoded query_params: {"q":["a.b"]}. The standalone review reproduction is available locally at /tmp/pr3533-query-full-repro.rs; it evaluates both allow and deny pairs against that actual rule. The main finding is also directly traceable to the pinned Regorus src/builtins/glob.rs default-delimiter logic and the runtime call cited above.

Frozen target and reproduction of the diff

• Base ref: main at 96c08f111b7ccf3d048a876c23e724014babb585.
• Head ref: kirit93/prover-query-containment at 48e12bdbf15d7f202456b6bcc9667cc6cdebe85d.
• Actual PR diff baseline / merge-base: fa8f6d394983b541ac31363f8a2d5ea027b08acf.
• One commit: feat(prover): support REST query parameter containment.
• Scope: 12 files, 1,209 additions, 50 deletions.
• Isolated checkout: /tmp/openshell-pr3533-review; clean detached head, no uncommitted work included.
• GitHub head was rechecked and remained unchanged.

git diff fa8f6d394983b541ac31363f8a2d5ea027b08acf 48e12bdbf15d7f202456b6bcc9667cc6cdebe85d

Accepted findings are the wildcard modeling defect and documentation gap. No separate finding was raised for a missing mixed-value integration witness without a demonstrated defect; the necessary wildcard regression is included in the confirmed finding. Decoded NUL handling raised a runtime evaluation error and was not elevated into a speculative second bug. Generic hardening and stylistic refactors were excluded. No additional out-of-scope engineering follow-up was requested.

[github-actions]

🌿 Preview your docs: https://nvidia-preview-pr-3533.docs.buildwithfern.com/openshell

[johnnygreco]

The follow-up panel review now comes up clean at commit 91abe12. All three independent reviewers reported no actionable code findings across query-model correctness and security soundness; bounded probing, cancellation, replay, and solver fallback; and runtime parity, tests, CLI/API contracts, and documentation.

Validation: cargo test --locked --offline -p openshell-prover -p openshell-prover-cli passed all 147 tests plus one doc test, and git diff --check passed. No code changes were made during this review. Full repository CI/E2E was not independently rerun.

The accepted-issue linkage already noted in the PR remains a separate maintainer requirement before merge.

[johnnygreco]

@kirit93 — I completed an additional QA campaign against 91abe12. No new merge-blocking containment defect was found. The dotted-wildcard fixes behaved correctly, and the two observations below are compatibility/diagnostic follow-ups, not demonstrated unsound proofs.

Validation included:

• 626 unique policy-file scenarios passed: 355 scenarios against both debug and release CLI builds, plus 271 additional release cases.
• 11,440 production evaluator decisions agreed, including replay of all 142 REST counterexamples against both candidate and boundary.
• 40/41 real TCP/HTTP relay experiments matched expectations; the exception was a decoded NUL rejected fail-closed with zero upstream bytes.
• 28 operational checks passed, including 120 concurrent CLI invocations, resource limits, solver timeout/cancellation, and output failures; 206 existing regression tests passed.

These exercised the actual CLI, production policy loader/parser/evaluator, and HTTP relay with loopback TCP. They did not exercise a deployed gateway/sandbox, TLS interception, or an external Git server.

Actionable feedback

1. Add a short compatibility clarification to the prover reference. Exact-empty query matchers (query: {q: ""}) are modeled correctly and work through local YAML loading, but the protobuf runtime-loading path rejects them. I reproduced this for both allow and deny rules: a self-comparison returns within_boundary, while authored policy → protobuf → OpaEngine::from_proto fails validation. The existing runtime test explicitly documents this as OPA-only. Please state this limitation in the REST query section and distinguish containment from deployment compatibility. No protobuf redesign or change to the containment algorithm is requested for this PR. Supporting empty exact matchers through protobuf can be a separate follow-up.

2. Track decoded-NUL handling as a runtime diagnostics follow-up. With an allow rule q: "*", GET /items?q=%00 reaches query decoding but fails glob evaluation with string contains internal glob placeholder; the connection closes without an HTTP response and nothing reaches the upstream. Rejecting the value is appropriate. The improvement is to specify the unsupported runtime input and, if consistent with existing error handling, return a predictable client-facing rejection. Add a wire-level regression asserting zero upstream bytes. Do not relax rejection or treat this as a new containment vulnerability.

3. Retain a compact production-path regression suite from this coverage. Prioritize authored policy → runtime load → HTTP request checks for q=a.b under *, q=a&q=a.b, missing versus empty keys, repeated-value deny precedence, and percent-encoded keys/values. The existing direct-Rego/model tests are useful; loader and wire coverage additionally catches representation and decoding differences.

My recommendation is to proceed with the core containment change, make the small documentation clarification, and handle runtime representation/diagnostic improvements separately. These observations do not reopen the earlier wildcard soundness finding.