fix(prover): match runtime query wildcard semantics

Signed-off-by: Kirit93 <kthadaka@nvidia.com>

Author: kirit93

architecture/security-policy.md

@@ -395,7 +395,10 @@ or decide whether an in-boundary change is eligible for automatic approval.
 
 The containment model covers filesystem paths, supported process identities,
 Landlock compatibility requirements, L4 destinations including IP ranges, and
-enforced REST method and path authority. Identity comparisons assume consistent
+enforced REST method, path, and supported query-parameter authority. Query checks
+support exact ASCII values and `*` with the runtime's dot-delimited glob semantics,
+including missing and repeated parameters. Other query matchers remain unsupported.
+Identity comparisons assume consistent
 user and group resolution. Compatibility checks compare requested enforcement
 requirements, not the actual kernel state of a running sandbox.
 It returns explicit unsupported or inconclusive

crates/openshell-prover/README.md

@@ -24,7 +24,18 @@ endpoint host and path selectors, and REST allow and deny method and path
 selectors. It returns `unsupported_policy_shape` when either policy uses a
 non-ASCII literal in one of those fields. This boundary does not apply to
 filesystem paths or unrelated policy text. Embedded NUL bytes in network
-selector fields are also unsupported. ASCII wildcards are modeled over the
+selector fields are also unsupported. REST query keys and exact values must be
+ASCII without NUL. Supported query matchers are exact strings and `*`; partial
+globs and `any` matchers remain unsupported. The runtime treats `.` as a glob
+delimiter, so `*` matches an empty value or `a/b`, but not `a.b`. Configured keys
+must be present. All repeated values must match an allow constraint; any matching
+value satisfies each configured deny constraint. Unconfigured keys are unrestricted.
+The model separates wildcard-matching and nonmatching values, including in decoded
+`query_params` counterexamples. It does not infer application-specific permissions.
+At most 256 query matchers are admitted across both policies; their keys and values
+count toward the existing pattern-byte limits.
+
+ASCII wildcards are modeled over the
 runtime match language and can therefore match non-ASCII runtime values. A
 solver string that cannot be decoded and validated exactly produces
 `invalid_witness` rather than counterexample evidence.

crates/openshell-prover/src/containment/query.rs

@@ -3,7 +3,9 @@
 
 //! Exact finite abstraction of decoded REST query parameters for exact / `*`
 //! matchers. Each key has one Boolean per literal mentioned by either policy,
-//! plus one shared class for all other values. Multiple classes may be present:
+//! plus separate wildcard-matching and nonmatching classes for other values.
+//! The runtime's `glob.match(pattern, [], value)` uses `.` as a delimiter,
+//! so `*` does not match dotted values. Multiple classes may be present:
 //! runtime allow rules require ALL repeated values to match, while deny rules
 //! require ANY value to match. Multiplicity and order do not affect either rule.
 //! All-false represents an absent key. The REST parser never produces a present
@@ -45,8 +47,13 @@ pub(super) struct SymbolicQuery(BTreeMap<String, QueryKey>);
 
 struct QueryKey {
     literals: BTreeMap<String, Bool>,
-    other: Bool,
-    other_value: String,
+    // Index 0 matches `*`; index 1 does not.
+    other: [Bool; 2],
+    other_values: [String; 2],
+}
+
+fn wildcard_matches(value: &str) -> bool {
+    !value.contains('.')
 }
 
 pub(super) fn supported(rules: &QueryRules) -> bool {
@@ -63,7 +70,9 @@ pub(super) fn supported(rules: &QueryRules) -> bool {
 pub(super) fn contains(boundary: &QueryRules, candidate: &QueryRules) -> bool {
     boundary.iter().all(|(key, required)| {
         candidate.get(key).is_some_and(|proposed| {
-            required == proposed || matches!(required, QueryMatcher::Glob(value) if value == "*")
+            required == proposed
+                || (matches!(required, QueryMatcher::Glob(value) if value == "*")
+                    && matches!(proposed, QueryMatcher::Glob(value) if wildcard_matches(value)))
         })
     })
 }
@@ -110,9 +119,11 @@ impl SymbolicQuery {
                 .into_iter()
                 .enumerate()
                 .map(|(key_index, (key, values))| {
-                    let mut other_value = String::new();
-                    while values.contains(&other_value) {
-                        other_value.push('a');
+                    let mut other_values = [String::new(), ".".to_owned()];
+                    for value in &mut other_values {
+                        while values.contains(value) {
+                            value.push('a');
+                        }
                     }
                     (
                         key,
@@ -129,8 +140,10 @@ impl SymbolicQuery {
                                     )
                                 })
                                 .collect(),
-                            other: Bool::new_const(format!("{name}_query_{key_index}_other")),
-                            other_value,
+                            other: std::array::from_fn(|class| {
+                                Bool::new_const(format!("{name}_query_{key_index}_other_{class}"))
+                            }),
+                            other_values,
                         },
                     )
                 })
@@ -146,11 +159,12 @@ impl SymbolicQuery {
         let mut query = Self::new("concrete", boundary, candidate);
         for (key, classes) in &mut query.0 {
             let present = values.get(key).map_or(&[][..], Vec::as_slice);
-            classes.other = Bool::from_bool(
-                present
-                    .iter()
-                    .any(|value| !classes.literals.contains_key(value)),
-            );
+            classes.other = std::array::from_fn(|class| {
+                Bool::from_bool(present.iter().any(|value| {
+                    !classes.literals.contains_key(value)
+                        && usize::from(!wildcard_matches(value)) == class
+                }))
+            });
             for (value, flag) in &mut classes.literals {
                 *flag = Bool::from_bool(present.contains(value));
             }
@@ -168,19 +182,35 @@ impl SymbolicQuery {
                         unreachable!("query matchers must be validated before modeling")
                     };
                     if value == "*" {
-                        bool_or(
+                        let matching = bool_or(
                             classes
                                 .literals
-                                .values()
-                                .cloned()
-                                .chain([classes.other.clone()]),
-                        )
+                                .iter()
+                                .filter(|(literal, _)| wildcard_matches(literal))
+                                .map(|(_, flag)| flag.clone())
+                                .chain([classes.other[0].clone()]),
+                        );
+                        if deny {
+                            matching
+                        } else {
+                            Bool::and(&[
+                                matching,
+                                !bool_or(
+                                    classes
+                                        .literals
+                                        .iter()
+                                        .filter(|(literal, _)| !wildcard_matches(literal))
+                                        .map(|(_, flag)| flag.clone())
+                                        .chain([classes.other[1].clone()]),
+                                ),
+                            ])
+                        }
                     } else if deny {
                         classes.literals[value].clone()
                     } else {
                         Bool::and(&[
                             classes.literals[value].clone(),
-                            !classes.other.clone(),
+                            !bool_or(classes.other.iter().cloned()),
                             !bool_or(
                                 classes
                                     .literals
@@ -204,8 +234,10 @@ impl SymbolicQuery {
                     values.push(literal.clone());
                 }
             }
-            if model.eval(&classes.other, true)?.as_bool()? {
-                values.push(classes.other_value.clone());
+            for (flag, value) in classes.other.iter().zip(&classes.other_values) {
+                if model.eval(flag, true)?.as_bool()? {
+                    values.push(value.clone());
+                }
             }
             if !values.is_empty() {
                 query.insert(key.clone(), values);
@@ -222,6 +254,36 @@ mod tests {
     use serde_json::json;
     use z3::ast::Ast;
 
+    #[test]
+    fn symbolic_wildcard_preserves_mixed_other_values_in_witness() {
+        let policy = super::super::parse_policy_str(
+            r#"{"version":1,"network_policies":{"n":{"endpoints":[{
+                "host":"example.com","port":443,"protocol":"rest","enforcement":"enforce",
+                "rules":[{"allow":{"method":"GET","path":"/**","query":{"q":"*"}}}]
+            }]}}}"#,
+        )
+        .unwrap();
+        let query = SymbolicQuery::new("mixed", &policy, &policy);
+        let rules = BTreeMap::from([("q".to_owned(), QueryMatcher::Glob("*".to_owned()))]);
+        let solver = z3::Solver::new();
+        solver.assert(&query.0["q"].other[0]);
+        solver.assert(&query.0["q"].other[1]);
+        solver.assert(!query.matches(&rules, false));
+        solver.assert(query.matches(&rules, true));
+        assert_eq!(solver.check(), z3::SatResult::Sat);
+        let decoded = query.decode(&solver.get_model().unwrap()).unwrap();
+        assert_eq!(decoded["q"], ["", "."]);
+        let concrete = SymbolicQuery::concrete(&policy, &policy, &decoded);
+        assert_eq!(
+            concrete.matches(&rules, false).simplify().as_bool(),
+            Some(false)
+        );
+        assert_eq!(
+            concrete.matches(&rules, true).simplify().as_bool(),
+            Some(true)
+        );
+    }
+
     #[test]
     fn decoded_query_model_matches_runtime_for_missing_and_repeated_values() {
         let mut engine = Engine::new();
@@ -248,6 +310,7 @@ deny := data.openshell.sandbox.deny_query_params_match(input.request, input.rule
             json!({}),
             json!({"service":"*"}),
             json!({"service":"a"}),
+            json!({"service":"a.b"}),
             json!({"service":""}),
             json!({"service":"a", "v":"2"}),
             json!({"":"*"}),
@@ -265,6 +328,12 @@ deny := data.openshell.sandbox.deny_query_params_match(input.request, input.rule
                 json!({}),
                 json!({"service":["a"]}),
                 json!({"service":["b"]}),
+                json!({"service":["a.b"]}),
+                json!({"service":["a", "a.b"]}),
+                json!({"service":["a.b", "a"]}),
+                json!({"service":["a.b", "a.b"]}),
+                json!({"service":["."]}),
+                json!({"service":["/", "a/b", "é", "\n"]}),
                 json!({"service":["a","a"]}),
                 json!({"service":["a","b"]}),
                 json!({"service":[""]}),

crates/openshell-prover/tests/query_containment.rs

@@ -38,6 +38,8 @@ fn check(boundary: &str, candidate: &str) -> CheckResult {
 #[test]
 fn exact_wildcard_and_required_keys() {
     for (parent, child, within) in [
+        (json!({"service":"*"}), json!({"service":"a.b"}), false),
+        (json!({"service":"*"}), json!({"service":"a/b"}), true),
         (
             json!({"service":"git-upload-pack"}),
             json!({"service":"git-upload-pack"}),
@@ -112,6 +114,11 @@ fn exact_wildcard_and_required_keys() {
 #[test]
 fn query_denies_and_allow_unions() {
     for (parent, child, within) in [
+        (
+            policy(&[json!({})], &[json!({"service":"a.b"})]),
+            policy(&[json!({})], &[json!({"service":"*"})]),
+            false,
+        ),
         (
             policy(&[json!({})], &[json!({"service":"git-receive-pack"})]),
             policy(&[json!({"service":"git-upload-pack"})], &[]),

crates/openshell-prover/tests/runtime_parity.rs

@@ -98,6 +98,14 @@ fn query_counterexamples_replay_against_runtime() {
         }}}).to_string()
     };
     for (boundary, candidate) in [
+        (
+            policy(json!({"service":"*"}), None),
+            policy(json!({"service":"a.b"}), None),
+        ),
+        (
+            policy(json!({}), Some(json!({"service":"a.b"}))),
+            policy(json!({}), Some(json!({"service":"*"}))),
+        ),
         (
             policy(json!({"service":"git-upload-pack"}), None),
             policy(json!({"service":"git-receive-pack"}), None),

docs/reference/policy-prover.mdx

@@ -121,14 +121,18 @@ The `counterexample.domain` field selects one of these objects:
 | `filesystem` | `access` (`read` or `write`) and `path`. |
 | `process` | `field` (`run_as_user` or `run_as_group`), `boundary`, and `candidate`. |
 | `landlock` | `boundary` and `candidate` compatibility modes. |
-| `network` | `binary`, `ancestor_binary`, `binary_identity_required`, `host`, `destination_ip`, `trusted_gateway`, `port`, `protocol`, `method`, and `path`. |
+| `network` | `binary`, `ancestor_binary`, `binary_identity_required`, `host`, `destination_ip`, `trusted_gateway`, `port`, `protocol`, `method`, `path`, and optional `query_params`. |
 
 Network `binary` and `ancestor_binary` values are `null` when binary identity
 enforcement is disabled. `method` and `path` are `null` for L4 witnesses.
 `trusted_gateway: true` means the witness uses a recognized host-gateway alias
 with a runtime-provided trusted gateway binding; `false` uses ordinary
 destination validation.
 
+`query_params` contains decoded query values as arrays, preserving distinct repeated
+values. It is omitted when empty. Percent-encode keys and values when constructing
+a request to replay the counterexample.
+
 The stable reason codes are `invalid_input`, `unsupported_policy_shape`,
 `unresolved_workdir`, `unresolved_binary_path`,
 `unresolved_filesystem_path`, `solver_timeout`, `solver_unknown`,
@@ -161,7 +165,7 @@ inconclusive results as failures in CI.
 
 The containment check covers filesystem paths, process identity settings,
 Landlock compatibility requirements, L4 destination authority, and enforced
-REST method and path authority, including explicit REST denies. The result
+REST method, path, and supported query constraints, including explicit REST denies. The result
 object reports the policy domains modeled by each check. Policies that use
 recognized authority outside that coverage return `unsupported` rather than
 silently ignoring it.
@@ -175,13 +179,28 @@ containment model return `unsupported` and exit `3`.
 The prover applies aggregate limits across the candidate and boundary before
 semantic shape validation: 1,024 network rules, 4,096 endpoints, 4,096 binary
 selectors, 65,536 authored port entries, 4,096 `allowed_ips` entries, 16,384
-REST rules, 4 KiB per modeled pattern, and 1 MiB of modeled pattern text.
+REST rules, 256 query matchers, 4 KiB per modeled pattern, and 1 MiB of modeled pattern text.
+Query keys and values count toward the pattern-byte limits. These limits combine
+both inputs: comparing identical policies with 129 query matchers exceeds the limit.
 Exceeding any limit returns `inconclusive` with `reason_code: resource_limit`.
 A cancellation already requested at preflight takes precedence over that
 result; otherwise a resource limit takes precedence over unsupported
 policy-shape diagnostics. This ordering keeps validation work bounded for
 checked-in CI inputs.
 
+### REST query constraints
+
+Query keys and exact values must be ASCII without NUL. Exact strings and the whole
+`*` wildcard are supported; partial globs and `any` matchers return `unsupported`.
+The runtime uses `.` as a glob delimiter: `*` matches `a` and an empty value, but
+not `a.b`. A boundary `q: "*"` therefore does not contain a candidate `q: "a.b"`.
+
+Every configured key must be present. All repeated values must match an allow
+constraint; any matching value satisfies each configured deny constraint. Thus
+`q=a&q=a.b` fails an allow `q: "*"` but matches a deny `q: "*"`.
+Unconfigured keys are unrestricted. Comparisons use decoded values and do not
+infer that one application operation includes another.
+
 ### Process and Landlock settings
 
 Matching supported `run_as_user` and `run_as_group` values do not expand the