From 0480e3a058b97ad38d841134ac908cb6bc590583 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Tue, 9 Jun 2026 12:35:49 -0700 Subject: [PATCH 1/3] feat(policy): spike maximum policy envelope prover --- .../MAXIMUM_POLICY_ENVELOPE_SPIKE.md | 247 +++++ crates/openshell-prover/README.md | 40 + crates/openshell-prover/src/envelope.rs | 885 ++++++++++++++++++ crates/openshell-prover/src/lib.rs | 1 + crates/openshell-prover/src/policy.rs | 111 +++ 5 files changed, 1284 insertions(+) create mode 100644 crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md create mode 100644 crates/openshell-prover/src/envelope.rs diff --git a/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md b/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md new file mode 100644 index 000000000..8e6dbc53a --- /dev/null +++ b/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md @@ -0,0 +1,247 @@ + + + +# Maximum Policy Envelope Spike + +This spike tests whether OpenShell can compare a candidate policy against a +security-approved maximum policy and reject any candidate that allows more than +the maximum. + +Core check: + +```text +exists x: + candidate_allows(x) + AND NOT maximum_allows(x) +``` + +Rust normalizes schema-level OpenShell policy semantics, such as access presets +and unsupported field detection. Z3 owns the action variables (`binary`, `host`, +`port`, `protocol`, `method`, and `path`) and checks whether any symbolic action +is allowed by the candidate but not by the maximum. Host, path, and binary globs +compile to Z3 regular-expression constraints. If the solver finds such an `x`, +the candidate exceeds the maximum. If no such `x` exists, the candidate is within +the modeled maximum. If either policy uses a surface the spike does not model +yet, the check fails closed as `Unsupported`. + +## Demo 1: Narrow Candidate Within Maximum + +Maximum: + +```yaml +version: 1 +network_policies: + github: + endpoints: + - host: api.github.com + port: 443 + protocol: rest + enforcement: enforce + rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/* + binaries: + - path: /usr/bin/gh +``` + +Candidate: + +```yaml +version: 1 +network_policies: + github: + endpoints: + - host: api.github.com + port: 443 + protocol: rest + enforcement: enforce + rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123 + binaries: + - path: /usr/bin/gh +``` + +Result: + +```text +WithinMax +``` + +Why: the candidate narrows the approved path from one issue path glob to one +specific issue. + +## Demo 2: Broad Path Proposal Exceeds Maximum + +Maximum: + +```yaml +rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/* +``` + +Candidate: + +```yaml +rules: + - allow: + method: GET + path: /repos/NVIDIA/** +``` + +Result: + +```text +ExceedsMax { + binary: "/usr/bin/gh", + host: "api.github.com", + port: 443, + protocol: "rest", + method: "GET", + path: "/repos/NVIDIA/", + reason: "candidate allows an action outside the maximum policy" +} +``` + +Why: the candidate allows requests outside the approved issue path. The +counterexample is a concrete model selected by Z3: a request the broader +candidate would allow but the maximum would not. + +## Demo 3: Method Escalation Exceeds Maximum + +Maximum: + +```yaml +rules: + - allow: + method: GET + path: /repos/NVIDIA/** +``` + +Candidate: + +```yaml +rules: + - allow: + method: POST + path: /repos/NVIDIA/OpenShell/issues +``` + +Result: + +```text +ExceedsMax { + method: "POST", + ... +} +``` + +Why: the candidate adds a mutating HTTP method outside the maximum's approved +read-only method. + +## Demo 4: Host, Binary, and Port Broadening + +These candidate changes all exceed a narrower maximum: + +```text +host: api.github.com -> *.github.com +binary: /usr/bin/gh -> /usr/bin/* +port: 443 -> [443, 8443] +L7 REST maximum -> L4-only candidate +``` + +Why: each change creates at least one action that the maximum does not allow. + +## Demo 5: Unsupported Surfaces Fail Closed + +Maximum: + +```yaml +access: full +deny_rules: + - method: POST + path: /admin/** +``` + +Result: + +```text +Unsupported { + reason: "maximum policy rule 'github' uses deny_rules, which maximum containment does not model yet" +} +``` + +Why: deny rules change containment semantics. Until the prover models allow plus +deny precedence, the check must not approve these cases. + +Other surfaces currently fail closed: + +```text +query constraints +GraphQL operation and field constraints +MCP tool/resource constraints +CIDR-only allowed_ips +endpoint path scoping +``` + +## Narrowness Companion + +The maximum-policy check answers whether a candidate stays under a +security-approved ceiling. That is the immediate enterprise gate. The related +narrowness question is different: + +```text +How much broader is this candidate than the current policy? +``` + +A first useful shape is to reuse the same symbolic model and score the proposed +delta: + +```text +delta = candidate_allows(x) AND NOT current_allows(x) +score(delta) <= budget +``` + +This could support: + +- per-update budgets, such as "one new REST method" or "one new concrete path"; +- total sandbox budgets, such as "no more than N endpoint families"; +- hard caps, such as rejecting `**` unless the maximum explicitly grants it; +- reviewer-facing explanations that identify why a change is too broad. + +This spike should not over-design the product surface yet. The useful next proof +is a small set of tests showing whether Z3 can produce and classify policy +deltas well enough to enforce simple budgets. + +## Current Test Command + +```shell +mise exec -- cargo test -p openshell-prover +``` + +Maximal-policy tests include: + +```text +envelope::tests::exact_rest_rule_is_within_maximum +envelope::tests::broader_rest_path_exceeds_maximum +envelope::tests::method_escalation_exceeds_maximum +envelope::tests::host_wildcard_broadening_exceeds_maximum +envelope::tests::binary_wildcard_broadening_exceeds_maximum +envelope::tests::port_broadening_exceeds_maximum +envelope::tests::l4_candidate_exceeds_l7_maximum +envelope::tests::maximum_wildcards_cover_exact_candidate +envelope::tests::deny_rules_are_unsupported_until_modeled +envelope::tests::query_graphql_cidr_and_mcp_surfaces_are_unsupported +``` + +## Readout + +This validates the product shape for REST/path/binary/host/port maximum-policy +envelopes with a symbolic Z3 counterexample query. The next research step on +this branch is a narrowness budget proof over policy deltas. Deny rules, MCP, +GraphQL, query constraints, and CIDR can land as follow-on modeled surfaces once +the containment and delta mechanics are proven useful. diff --git a/crates/openshell-prover/README.md b/crates/openshell-prover/README.md index f8b45eca6..db6c9f67d 100644 --- a/crates/openshell-prover/README.md +++ b/crates/openshell-prover/README.md @@ -30,6 +30,46 @@ The first two are unconditional risks. The latter two are *delta* properties — the gateway runs the prover on both the baseline policy and the merged policy and surfaces only the new paths. +## Maximum-policy containment + +The prover also exposes a maximum-policy containment check for spike +work on security-approved policy envelopes. This is separate from the +risk/finding queries above: it compares a candidate policy with a +maximum policy and asks whether the candidate allows any modeled action +outside the maximum. + +The check is shaped around this counterexample query: + +```text +exists x: + candidate_allows(x) + AND NOT maximum_allows(x) +``` + +The first implementation models REST allow surfaces for binaries, +hosts, ports, protocols, methods, paths, access presets, and the +supported host/path/binary glob subset. Rust normalizes policy schema +details such as access presets and fail-closed unsupported fields, then +encodes candidate and maximum allow predicates as Z3 constraints over +symbolic action variables (`binary`, `host`, `port`, `protocol`, +`method`, and `path`). Host, path, and binary globs are encoded as Z3 +regular-expression membership constraints. Query parameters are not +modeled yet. It returns: + +- `WithinMax` when every modeled candidate action is covered. +- `ExceedsMax` with a solver-produced counterexample when the candidate + is broader. +- `Unsupported` when either policy uses a surface not modeled yet, such + as deny rules, query constraints, GraphQL controls, MCP controls, + endpoint path scoping, or CIDR-only `allowed_ips`. + +Unsupported is intentionally fail-closed. Future work can flip those +fixtures to modeled results as deny rules, MCP, GraphQL, and richer +symbolic path/query encodings land. See +[`MAXIMUM_POLICY_ENVELOPE_SPIKE.md`](MAXIMUM_POLICY_ENVELOPE_SPIKE.md) +for a walkthrough of the current spike behavior and the companion +narrowness-budget direction. + ## Evidence shape Each finding carries one or more [`FindingPath::Exfil`](src/finding.rs) diff --git a/crates/openshell-prover/src/envelope.rs b/crates/openshell-prover/src/envelope.rs new file mode 100644 index 000000000..1b64eeb1c --- /dev/null +++ b/crates/openshell-prover/src/envelope.rs @@ -0,0 +1,885 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Maximum-policy containment checks. +//! +//! This module answers a different question than the existing prover findings: +//! given a security-approved maximum policy and a candidate policy, does the +//! candidate allow any modeled action outside the maximum envelope? + +use std::str::FromStr; + +use crate::policy::{Endpoint, L7Rule, NetworkPolicyRule, PolicyModel}; +use z3::ast::{Bool, Int, Regexp, String as Z3String}; +use z3::{Context, SatResult, Solver}; + +const READ_ONLY_METHODS: &[&str] = &["GET", "HEAD", "OPTIONS"]; +const READ_WRITE_METHODS: &[&str] = &["GET", "HEAD", "OPTIONS", "POST", "PUT", "PATCH"]; +const ALL_METHODS: &[&str] = &["GET", "HEAD", "OPTIONS", "POST", "PUT", "PATCH", "DELETE"]; + +/// Result of checking whether a candidate policy is inside a maximum policy. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum MaximumPolicyCheck { + /// Every modeled candidate action is contained by the maximum policy. + WithinMax, + /// The candidate allows at least one modeled action outside the maximum. + ExceedsMax { + /// Concrete action allowed by the candidate but not by the maximum. + counterexample: PolicyCounterexample, + }, + /// The policy uses a surface the first containment slice does not model. + Unsupported { + /// Human-readable reason. The check must fail closed at callers. + reason: String, + }, +} + +/// A representative action that witnesses maximum-policy violation. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct PolicyCounterexample { + pub binary: String, + pub host: String, + pub port: u16, + pub protocol: String, + pub method: String, + pub path: String, + pub reason: String, +} + +struct SymbolicAction { + binary: Z3String, + host: Z3String, + port: Int, + protocol: Z3String, + method: Z3String, + path: Z3String, +} + +/// Check whether `candidate` is semantically contained by `maximum` for the +/// currently modeled allow surface. +pub fn check_within_maximum(maximum: &PolicyModel, candidate: &PolicyModel) -> MaximumPolicyCheck { + if let Some(reason) = unsupported_reason("maximum", maximum) { + return MaximumPolicyCheck::Unsupported { reason }; + } + if let Some(reason) = unsupported_reason("candidate", candidate) { + return MaximumPolicyCheck::Unsupported { reason }; + } + + match find_z3_violation(maximum, candidate) { + Z3EnvelopeResult::WithinMax => MaximumPolicyCheck::WithinMax, + Z3EnvelopeResult::ExceedsMax { counterexample } => { + MaximumPolicyCheck::ExceedsMax { counterexample } + } + Z3EnvelopeResult::Unsupported { reason } => MaximumPolicyCheck::Unsupported { reason }, + } +} + +enum Z3EnvelopeResult { + WithinMax, + ExceedsMax { + counterexample: PolicyCounterexample, + }, + Unsupported { + reason: String, + }, +} + +fn find_z3_violation(maximum: &PolicyModel, candidate: &PolicyModel) -> Z3EnvelopeResult { + let _ctx = Context::thread_local(); + let solver = Solver::new(); + let action = SymbolicAction { + binary: Z3String::new_const("action_binary"), + host: Z3String::new_const("action_host"), + port: Int::new_const("action_port"), + protocol: Z3String::new_const("action_protocol"), + method: Z3String::new_const("action_method"), + path: Z3String::new_const("action_path"), + }; + + solver.assert(action.binary.regex_matches(&glob_regex("/**", "/"))); + solver.assert(action.host.regex_matches(&Regexp::full())); + solver.assert(Int::from_u64(1).le(&action.port)); + solver.assert(action.port.le(65535)); + solver.assert(str_eq_any(&action.protocol, &["rest"])); + solver.assert(str_eq_any(&action.method, ALL_METHODS)); + solver.assert( + Z3String::from_str("/") + .expect("literal") + .prefix(&action.path), + ); + + let candidate_allows = policy_allows(candidate, &action); + let maximum_allows = policy_allows(maximum, &action); + let violation = Bool::and(&[candidate_allows, !maximum_allows]); + solver.assert(&violation); + + match solver.check() { + SatResult::Unsat => Z3EnvelopeResult::WithinMax, + SatResult::Unknown => Z3EnvelopeResult::Unsupported { + reason: "Z3 returned unknown while checking maximum-policy containment".to_owned(), + }, + SatResult::Sat => { + let Some(model) = solver.get_model() else { + return Z3EnvelopeResult::Unsupported { + reason: "Z3 returned sat without a model for maximum-policy containment" + .to_owned(), + }; + }; + let Some(counterexample) = counterexample_from_model(&model, &action) else { + return Z3EnvelopeResult::Unsupported { + reason: "Z3 returned sat but the model could not be decoded into a maximum-policy counterexample".to_owned(), + }; + }; + Z3EnvelopeResult::ExceedsMax { counterexample } + } + } +} + +fn policy_allows(policy: &PolicyModel, action: &SymbolicAction) -> Bool { + bool_or( + policy + .network_policies + .values() + .map(|rule| rule_allows(rule, action)), + ) +} + +fn rule_allows(rule: &NetworkPolicyRule, action: &SymbolicAction) -> Bool { + Bool::and(&[ + bool_or( + rule.binaries + .iter() + .map(|binary| action.binary.regex_matches(&glob_regex(&binary.path, "/"))), + ), + bool_or( + rule.endpoints + .iter() + .map(|endpoint| endpoint_allows(endpoint, action)), + ), + ]) +} + +fn endpoint_allows(endpoint: &Endpoint, action: &SymbolicAction) -> Bool { + let mut constraints = vec![ + bool_or( + endpoint + .effective_ports() + .into_iter() + .map(|port| action.port.eq(Int::from_u64(u64::from(port)))), + ), + action + .host + .regex_matches(&glob_regex(&endpoint.host.to_ascii_lowercase(), ".")), + ]; + + if !normalized_protocol(&endpoint.protocol).is_empty() { + constraints.push(action.protocol.eq(normalized_protocol(&endpoint.protocol))); + constraints.push(bool_or(effective_rest_allows(endpoint).into_iter().map( + |(method, path)| { + Bool::and(&[ + action.method.eq(method.as_str()), + action.path.regex_matches(&glob_regex(&path, "/")), + ]) + }, + ))); + } + + Bool::and(&constraints) +} + +fn counterexample_from_model( + model: &z3::Model, + action: &SymbolicAction, +) -> Option { + let port = model.eval(&action.port, true)?.as_u64()?; + Some(PolicyCounterexample { + binary: model.eval(&action.binary, true)?.as_string()?, + host: model.eval(&action.host, true)?.as_string()?, + port: u16::try_from(port).ok()?, + protocol: model.eval(&action.protocol, true)?.as_string()?, + method: model.eval(&action.method, true)?.as_string()?, + path: model.eval(&action.path, true)?.as_string()?, + reason: "candidate allows an action outside the maximum policy".to_owned(), + }) +} + +fn bool_or(values: impl IntoIterator) -> Bool { + let values: Vec = values.into_iter().collect(); + if values.is_empty() { + Bool::from_bool(false) + } else { + Bool::or(&values) + } +} + +fn str_eq_any(value: &Z3String, options: &[&str]) -> Bool { + bool_or(options.iter().map(|option| value.eq(*option))) +} + +fn glob_regex(pattern: &str, separator: &str) -> Regexp { + if pattern == "**" { + return Regexp::full(); + } + + let mut parts = Vec::new(); + let mut chars = pattern.chars().peekable(); + while let Some(ch) = chars.next() { + if ch == '*' && chars.peek() == Some(&'*') { + chars.next(); + parts.push(Regexp::full()); + } else if ch == '*' { + parts.push(non_separator_regex(separator).star()); + } else { + parts.push(Regexp::literal(&ch.to_string())); + } + } + + if parts.is_empty() { + Regexp::literal("") + } else { + let refs: Vec<&Regexp> = parts.iter().collect(); + Regexp::concat(&refs) + } +} + +fn non_separator_regex(separator: &str) -> Regexp { + match separator { + "/" => Regexp::union(&[&Regexp::range(&' ', &'.'), &Regexp::range(&'0', &'~')]), + "." => Regexp::union(&[&Regexp::range(&' ', &'-'), &Regexp::range(&'/', &'~')]), + _ => Regexp::full(), + } +} + +fn unsupported_reason(prefix: &str, policy: &PolicyModel) -> Option { + for (rule_name, rule) in &policy.network_policies { + for endpoint in &rule.endpoints { + if !endpoint.path.is_empty() { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses endpoint path scoping, which maximum containment does not model yet" + )); + } + if unsupported_glob_pattern(&endpoint.host) { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses a host glob pattern outside the modeled subset" + )); + } + if !endpoint.allowed_ips.is_empty() { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses allowed_ips/CIDR scoping, which maximum containment does not model yet" + )); + } + if !endpoint.deny_rules.is_empty() { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses deny_rules, which maximum containment does not model yet" + )); + } + if endpoint.effective_ports().is_empty() { + return Some(format!( + "{prefix} policy rule '{rule_name}' endpoint {} has no modeled port", + endpoint_label(endpoint) + )); + } + if !endpoint.tls.is_empty() { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses tls '{}', which maximum containment does not model yet", + endpoint.tls + )); + } + if endpoint.allow_encoded_slash + || endpoint.websocket_credential_rewrite + || endpoint.request_body_credential_rewrite + { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses endpoint behavior flags that maximum containment does not model yet" + )); + } + if !endpoint.persisted_queries.is_empty() + || !endpoint.graphql_persisted_queries.is_empty() + || endpoint.graphql_max_body_bytes != 0 + { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses GraphQL persisted-query controls, which maximum containment does not model yet" + )); + } + if !endpoint.mcp_server.is_empty() + || !endpoint.mcp_tool.is_empty() + || !endpoint.mcp_resource.is_empty() + { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses MCP controls, which maximum containment does not model yet" + )); + } + if normalized_protocol(&endpoint.protocol) == "graphql" { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses GraphQL protocol controls, which maximum containment does not model yet" + )); + } + let protocol = normalized_protocol(&endpoint.protocol); + if !protocol.is_empty() && !protocol.eq_ignore_ascii_case("rest") { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses protocol '{}', which maximum containment does not model yet", + endpoint.protocol + )); + } + if !protocol.is_empty() && endpoint.enforcement != "enforce" { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses L7 protocol '{}' without enforcement mode 'enforce'", + endpoint.protocol + )); + } + for rule in &endpoint.rules { + if l7_rule_is_unsupported(rule) { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses L7 query, SQL, or GraphQL allow controls, which maximum containment does not model yet" + )); + } + if !rule.method.is_empty() && !modeled_rest_method(&rule.method) { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses REST method '{}', which maximum containment does not model yet", + rule.method + )); + } + if unsupported_glob_pattern(&rule.path) { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses a path glob pattern outside the modeled subset" + )); + } + } + } + for binary in &rule.binaries { + if unsupported_glob_pattern(&binary.path) { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses a binary glob pattern outside the modeled subset" + )); + } + } + } + None +} + +fn l7_rule_is_unsupported(rule: &L7Rule) -> bool { + !rule.command.is_empty() + || !rule.query.is_empty() + || !rule.operation_type.is_empty() + || !rule.operation_name.is_empty() + || !rule.fields.is_empty() +} + +fn effective_rest_allows(endpoint: &Endpoint) -> Vec<(String, String)> { + if normalized_protocol(&endpoint.protocol).is_empty() { + return ALL_METHODS + .iter() + .map(|method| ((*method).to_owned(), "**".to_owned())) + .collect(); + } + + match endpoint.access.as_str() { + "read-only" => methods_with_path(READ_ONLY_METHODS, "**"), + "read-write" => methods_with_path(READ_WRITE_METHODS, "**"), + "full" => methods_with_path(ALL_METHODS, "**"), + _ if endpoint.rules.is_empty() => Vec::new(), + _ => { + let mut allows = Vec::new(); + for rule in &endpoint.rules { + if rule.method.is_empty() { + continue; + } + let path = if rule.path.is_empty() { + "**".to_owned() + } else { + rule.path.clone() + }; + if rule.method == "*" { + allows.extend(methods_with_path(ALL_METHODS, &path)); + } else if rule.method.eq_ignore_ascii_case("GET") { + allows.extend(methods_with_path(&["GET", "HEAD"], &path)); + } else { + allows.push((rule.method.to_ascii_uppercase(), path)); + } + } + allows + } + } +} + +fn methods_with_path(methods: &[&str], path: &str) -> Vec<(String, String)> { + methods + .iter() + .map(|method| ((*method).to_owned(), path.to_owned())) + .collect() +} + +fn modeled_rest_method(method: &str) -> bool { + method == "*" || ALL_METHODS.contains(&method.to_ascii_uppercase().as_str()) +} + +fn unsupported_glob_pattern(pattern: &str) -> bool { + pattern + .chars() + .any(|ch| matches!(ch, '?' | '[' | ']' | '{' | '}' | '\\')) +} + +fn normalized_protocol(protocol: &str) -> &str { + protocol.trim() +} + +fn endpoint_label(endpoint: &Endpoint) -> String { + if endpoint.host.is_empty() { + "".to_owned() + } else { + endpoint.host.clone() + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::policy::parse_policy_str; + + fn policy(endpoint: &str, binaries: &str) -> PolicyModel { + parse_policy_str(&format!( + r" +version: 1 +network_policies: + test: + name: test + endpoints: +{endpoint} + binaries: +{binaries} +" + )) + .expect("parse policy") + } + + fn one_rest_endpoint(extra: &str) -> String { + format!( + r" - host: api.github.com + port: 443 + protocol: rest + enforcement: enforce +{extra}" + ) + } + + fn gh_binary() -> &'static str { + " - path: /usr/bin/gh" + } + + #[test] + fn exact_rest_rule_is_within_maximum() { + let maximum = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/*", + ), + gh_binary(), + ); + let candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123", + ), + gh_binary(), + ); + + assert_eq!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::WithinMax + ); + } + + #[test] + fn broader_rest_path_exceeds_maximum() { + let maximum = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/*", + ), + gh_binary(), + ); + let candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/**", + ), + gh_binary(), + ); + + let MaximumPolicyCheck::ExceedsMax { counterexample } = + check_within_maximum(&maximum, &candidate) + else { + panic!("expected candidate to exceed maximum"); + }; + assert_eq!(counterexample.method, "GET"); + assert_eq!(counterexample.host, "api.github.com"); + assert!(counterexample.path.starts_with("/repos/NVIDIA/")); + assert!( + !counterexample + .path + .starts_with("/repos/NVIDIA/OpenShell/issues/") + ); + } + + #[test] + fn method_escalation_exceeds_maximum() { + let maximum = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/**", + ), + gh_binary(), + ); + let candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: POST + path: /repos/NVIDIA/OpenShell/issues", + ), + gh_binary(), + ); + + let MaximumPolicyCheck::ExceedsMax { counterexample } = + check_within_maximum(&maximum, &candidate) + else { + panic!("expected method escalation"); + }; + assert_eq!(counterexample.method, "POST"); + } + + #[test] + fn head_is_contained_by_get_like_runtime_method_matching() { + let maximum = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/**", + ), + gh_binary(), + ); + let candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: HEAD + path: /repos/NVIDIA/OpenShell/issues", + ), + gh_binary(), + ); + + assert_eq!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::WithinMax + ); + } + + #[test] + fn custom_rest_methods_are_unsupported_until_modeled() { + let maximum = policy(&one_rest_endpoint(" access: read-only"), gh_binary()); + let candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: TRACE + path: /repos/NVIDIA/OpenShell/issues", + ), + gh_binary(), + ); + + assert!(matches!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::Unsupported { .. } + )); + } + + #[test] + fn host_wildcard_broadening_exceeds_maximum() { + let maximum = policy(&one_rest_endpoint(" access: read-only"), gh_binary()); + let candidate = policy( + r#" - host: "*.github.com" + port: 443 + protocol: rest + enforcement: enforce + access: read-only"#, + gh_binary(), + ); + + assert!(matches!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::ExceedsMax { .. } + )); + } + + #[test] + fn binary_wildcard_broadening_exceeds_maximum() { + let maximum = policy(&one_rest_endpoint(" access: read-only"), gh_binary()); + let candidate = policy( + &one_rest_endpoint(" access: read-only"), + " - path: /usr/bin/*", + ); + + assert!(matches!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::ExceedsMax { .. } + )); + } + + #[test] + fn port_broadening_exceeds_maximum() { + let maximum = policy(&one_rest_endpoint(" access: read-only"), gh_binary()); + let candidate = policy( + r" - host: api.github.com + ports: [443, 8443] + protocol: rest + enforcement: enforce + access: read-only", + gh_binary(), + ); + + let MaximumPolicyCheck::ExceedsMax { counterexample } = + check_within_maximum(&maximum, &candidate) + else { + panic!("expected port broadening"); + }; + assert_eq!(counterexample.port, 8443); + } + + #[test] + fn l4_candidate_exceeds_l7_maximum() { + let maximum = policy(&one_rest_endpoint(" access: read-only"), gh_binary()); + let candidate = policy( + r" - host: api.github.com + port: 443", + gh_binary(), + ); + + assert!(matches!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::ExceedsMax { .. } + )); + } + + #[test] + fn maximum_l4_covers_l7_candidate() { + let maximum = policy( + r" - host: api.github.com + port: 443", + gh_binary(), + ); + let candidate = policy( + &one_rest_endpoint(" access: read-write"), + gh_binary(), + ); + + assert_eq!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::WithinMax + ); + } + + #[test] + fn maximum_wildcards_cover_exact_candidate() { + let maximum = policy( + r#" - host: "*.github.com" + port: 443 + protocol: rest + enforcement: enforce + rules: + - allow: + method: GET + path: /repos/NVIDIA/**"#, + " - path: /usr/bin/*", + ); + let candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123", + ), + gh_binary(), + ); + + assert_eq!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::WithinMax + ); + } + + #[test] + fn deny_rules_are_unsupported_until_modeled() { + let maximum = policy( + r" - host: api.github.com + port: 443 + protocol: rest + enforcement: enforce + access: full + deny_rules: + - method: POST + path: /admin/**", + gh_binary(), + ); + let candidate = policy(&one_rest_endpoint(" access: read-only"), gh_binary()); + + let MaximumPolicyCheck::Unsupported { reason } = check_within_maximum(&maximum, &candidate) + else { + panic!("expected unsupported deny rule"); + }; + assert!(reason.contains("deny_rules")); + } + + #[test] + fn query_graphql_cidr_and_mcp_surfaces_are_unsupported() { + let maximum = policy(&one_rest_endpoint(" access: read-only"), gh_binary()); + + let query_candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /search/issues + query: + org: NVIDIA", + ), + gh_binary(), + ); + assert!(matches!( + check_within_maximum(&maximum, &query_candidate), + MaximumPolicyCheck::Unsupported { .. } + )); + + let graphql_candidate = policy( + r" - host: api.github.com + port: 443 + protocol: graphql + enforcement: enforce + rules: + - allow: + operation_type: query + fields: [repository]", + gh_binary(), + ); + assert!(matches!( + check_within_maximum(&maximum, &graphql_candidate), + MaximumPolicyCheck::Unsupported { .. } + )); + + let cidr_candidate = policy( + r#" - port: 443 + allowed_ips: ["10.0.5.0/24"]"#, + gh_binary(), + ); + assert!(matches!( + check_within_maximum(&maximum, &cidr_candidate), + MaximumPolicyCheck::Unsupported { .. } + )); + + let mcp_candidate = policy( + r" - host: github.mcp.local + port: 443 + protocol: rest + mcp_server: github + mcp_tool: get_issue", + gh_binary(), + ); + assert!(matches!( + check_within_maximum(&maximum, &mcp_candidate), + MaximumPolicyCheck::Unsupported { .. } + )); + } + + #[test] + fn non_enforcing_l7_modes_are_unsupported_until_modeled() { + let enforced_maximum = policy(&one_rest_endpoint(" access: read-only"), gh_binary()); + + let audit_candidate = policy( + r" - host: api.github.com + port: 443 + protocol: rest + enforcement: audit + access: read-only", + gh_binary(), + ); + assert!(matches!( + check_within_maximum(&enforced_maximum, &audit_candidate), + MaximumPolicyCheck::Unsupported { .. } + )); + + let tls_skip_candidate = policy( + r" - host: api.github.com + port: 443 + protocol: rest + enforcement: enforce + tls: skip + access: read-only", + gh_binary(), + ); + assert!(matches!( + check_within_maximum(&enforced_maximum, &tls_skip_candidate), + MaximumPolicyCheck::Unsupported { .. } + )); + + let websocket_candidate = policy( + r" - host: api.github.com + port: 443 + protocol: websocket + enforcement: enforce + access: read-only", + gh_binary(), + ); + assert!(matches!( + check_within_maximum(&enforced_maximum, &websocket_candidate), + MaximumPolicyCheck::Unsupported { .. } + )); + } + + #[test] + fn endpoint_behavior_flags_are_unsupported_until_modeled() { + let maximum = policy(&one_rest_endpoint(" access: read-only"), gh_binary()); + let candidate = policy( + r" - host: api.github.com + port: 443 + protocol: rest + enforcement: enforce + access: read-only + allow_encoded_slash: true", + gh_binary(), + ); + + assert!(matches!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::Unsupported { .. } + )); + } + + #[test] + fn unsupported_glob_syntax_fails_closed() { + let maximum = policy(&one_rest_endpoint(" access: read-only"), gh_binary()); + let candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/?", + ), + gh_binary(), + ); + + assert!(matches!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::Unsupported { .. } + )); + } +} diff --git a/crates/openshell-prover/src/lib.rs b/crates/openshell-prover/src/lib.rs index 226705204..04e19034d 100644 --- a/crates/openshell-prover/src/lib.rs +++ b/crates/openshell-prover/src/lib.rs @@ -9,6 +9,7 @@ pub mod accepted_risks; pub mod credentials; +pub mod envelope; pub mod finding; pub mod model; pub mod policy; diff --git a/crates/openshell-prover/src/policy.rs b/crates/openshell-prover/src/policy.rs index 8aea4b7d0..8b720ca31 100644 --- a/crates/openshell-prover/src/policy.rs +++ b/crates/openshell-prover/src/policy.rs @@ -50,6 +50,7 @@ const ALL_METHODS: &[&str] = &["GET", "HEAD", "OPTIONS", "POST", "PUT", "PATCH", // --------------------------------------------------------------------------- #[derive(Debug, Deserialize)] +#[serde(deny_unknown_fields)] struct PolicyFile { #[allow(dead_code)] version: Option, @@ -67,6 +68,7 @@ struct PolicyFile { } #[derive(Debug, Deserialize)] +#[serde(deny_unknown_fields)] struct FilesystemDef { #[serde(default)] include_workdir: bool, @@ -77,6 +79,7 @@ struct FilesystemDef { } #[derive(Debug, Deserialize)] +#[serde(deny_unknown_fields)] struct NetworkPolicyRuleDef { #[serde(default)] name: Option, @@ -87,10 +90,13 @@ struct NetworkPolicyRuleDef { } #[derive(Debug, Deserialize)] +#[serde(deny_unknown_fields)] struct EndpointDef { #[serde(default)] host: String, #[serde(default)] + path: String, + #[serde(default)] port: u16, #[serde(default)] ports: Vec, @@ -106,14 +112,36 @@ struct EndpointDef { rules: Vec, #[serde(default)] allowed_ips: Vec, + #[serde(default)] + deny_rules: Vec, + #[serde(default)] + persisted_queries: String, + #[serde(default)] + graphql_persisted_queries: BTreeMap, + #[serde(default)] + graphql_max_body_bytes: u32, + #[serde(default)] + allow_encoded_slash: bool, + #[serde(default)] + websocket_credential_rewrite: bool, + #[serde(default)] + request_body_credential_rewrite: bool, + #[serde(default)] + mcp_server: String, + #[serde(default)] + mcp_tool: String, + #[serde(default)] + mcp_resource: String, } #[derive(Debug, Deserialize)] +#[serde(deny_unknown_fields)] struct L7RuleDef { allow: L7AllowDef, } #[derive(Debug, Deserialize)] +#[serde(deny_unknown_fields)] struct L7AllowDef { #[serde(default)] method: String, @@ -121,9 +149,37 @@ struct L7AllowDef { path: String, #[serde(default)] command: String, + #[serde(default)] + query: BTreeMap, + #[serde(default)] + operation_type: String, + #[serde(default)] + operation_name: String, + #[serde(default)] + fields: Vec, } #[derive(Debug, Deserialize)] +#[serde(deny_unknown_fields)] +struct L7DenyRuleDef { + #[serde(default)] + method: String, + #[serde(default)] + path: String, + #[serde(default)] + command: String, + #[serde(default)] + query: BTreeMap, + #[serde(default)] + operation_type: String, + #[serde(default)] + operation_name: String, + #[serde(default)] + fields: Vec, +} + +#[derive(Debug, Deserialize)] +#[serde(deny_unknown_fields)] struct BinaryDef { path: String, } @@ -138,12 +194,29 @@ pub struct L7Rule { pub method: String, pub path: String, pub command: String, + pub query: BTreeMap, + pub operation_type: String, + pub operation_name: String, + pub fields: Vec, +} + +/// A single L7 deny rule on an endpoint. +#[derive(Debug, Clone)] +pub struct L7DenyRule { + pub method: String, + pub path: String, + pub command: String, + pub query: BTreeMap, + pub operation_type: String, + pub operation_name: String, + pub fields: Vec, } /// A network endpoint in the policy. #[derive(Debug, Clone)] pub struct Endpoint { pub host: String, + pub path: String, pub port: u16, pub ports: Vec, pub protocol: String, @@ -152,6 +225,16 @@ pub struct Endpoint { pub access: String, pub rules: Vec, pub allowed_ips: Vec, + pub deny_rules: Vec, + pub persisted_queries: String, + pub graphql_persisted_queries: BTreeMap, + pub graphql_max_body_bytes: u32, + pub allow_encoded_slash: bool, + pub websocket_credential_rewrite: bool, + pub request_body_credential_rewrite: bool, + pub mcp_server: String, + pub mcp_tool: String, + pub mcp_resource: String, } impl Endpoint { @@ -372,10 +455,28 @@ pub fn parse_policy_str(yaml: &str) -> Result { method: r.allow.method, path: r.allow.path, command: r.allow.command, + query: r.allow.query, + operation_type: r.allow.operation_type, + operation_name: r.allow.operation_name, + fields: r.allow.fields, + }) + .collect(); + let deny_rules = ep_raw + .deny_rules + .into_iter() + .map(|r| L7DenyRule { + method: r.method, + path: r.path, + command: r.command, + query: r.query, + operation_type: r.operation_type, + operation_name: r.operation_name, + fields: r.fields, }) .collect(); Endpoint { host: ep_raw.host, + path: ep_raw.path, port: ep_raw.port, ports: ep_raw.ports, protocol: ep_raw.protocol, @@ -384,6 +485,16 @@ pub fn parse_policy_str(yaml: &str) -> Result { access: ep_raw.access, rules, allowed_ips: ep_raw.allowed_ips, + deny_rules, + persisted_queries: ep_raw.persisted_queries, + graphql_persisted_queries: ep_raw.graphql_persisted_queries, + graphql_max_body_bytes: ep_raw.graphql_max_body_bytes, + allow_encoded_slash: ep_raw.allow_encoded_slash, + websocket_credential_rewrite: ep_raw.websocket_credential_rewrite, + request_body_credential_rewrite: ep_raw.request_body_credential_rewrite, + mcp_server: ep_raw.mcp_server, + mcp_tool: ep_raw.mcp_tool, + mcp_resource: ep_raw.mcp_resource, } }) .collect(); From 46cc861bb9e70611be005e5618fa76ad35ac2623 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Tue, 9 Jun 2026 12:57:33 -0700 Subject: [PATCH 2/3] feat(policy): add narrowness budget prover spike --- .../MAXIMUM_POLICY_ENVELOPE_SPIKE.md | 137 +++- crates/openshell-prover/README.md | 14 +- crates/openshell-prover/src/envelope.rs | 704 +++++++++++++++++- 3 files changed, 799 insertions(+), 56 deletions(-) diff --git a/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md b/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md index 8e6dbc53a..b915606d6 100644 --- a/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md +++ b/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md @@ -151,11 +151,14 @@ These candidate changes all exceed a narrower maximum: host: api.github.com -> *.github.com binary: /usr/bin/gh -> /usr/bin/* port: 443 -> [443, 8443] -L7 REST maximum -> L4-only candidate ``` Why: each change creates at least one action that the maximum does not allow. +L4-only endpoints are not modeled in this spike. They fail closed as +`Unsupported` rather than being compared against the REST-only symbolic action +domain. + ## Demo 5: Unsupported Surfaces Fail Closed Maximum: @@ -171,7 +174,7 @@ Result: ```text Unsupported { - reason: "maximum policy rule 'github' uses deny_rules, which maximum containment does not model yet" + reason: "maximum policy rule 'github' uses deny_rules, which policy envelope checks do not model yet" } ``` @@ -186,6 +189,7 @@ GraphQL operation and field constraints MCP tool/resource constraints CIDR-only allowed_ips endpoint path scoping +L4-only endpoints ``` ## Narrowness Companion @@ -206,16 +210,119 @@ delta = candidate_allows(x) AND NOT current_allows(x) score(delta) <= budget ``` -This could support: +The current spike includes a first narrowness check. Z3 proves whether each +modeled candidate grant adds any action outside the current policy: + +```text +exists x: + candidate_grant_allows(x) + AND NOT current_policy_allows(x) +``` + +Rust then scores the shape of each delta grant. This is deliberately coarse for +the spike: + +```text +exact new grant: +1 +single path wildcard: +2 +host/binary wildcard: +3 +recursive glob (**): +6 +``` + +A conservative budget can allow one exact grant and reject recursive globs: + +```rust +NarrownessBudget { + max_delta_grants: 1, + max_total_score: 1, + allow_recursive_globs: false, +} +``` + +## Demo 6: One Exact Path Fits A Narrow Budget + +Current: + +```yaml +rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123 +``` + +Candidate: + +```yaml +rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123 + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/456 +``` + +Result: + +```text +WithinBudget { + total_score: 1, + delta_grants: [ + { + method: "GET", + path: "/repos/NVIDIA/OpenShell/issues/456", + reasons: [NewGrant] + } + ] +} +``` + +Why: the candidate adds one exact modeled grant. The grant allows both `GET` and +runtime-implied `HEAD`, but the budget counts the source grant once. + +## Demo 7: Lazy Recursive Path Exceeds A Narrow Budget + +Current: + +```yaml +rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123 +``` + +Candidate: + +```yaml +rules: + - allow: + method: GET + path: /repos/NVIDIA/** +``` + +Result: + +```text +ExceedsBudget { + total_score: 7, + delta_grants: [ + { + method: "GET", + path: "/repos/NVIDIA/**", + reasons: [NewGrant, RecursivePathGlob] + } + ] +} +``` -- per-update budgets, such as "one new REST method" or "one new concrete path"; -- total sandbox budgets, such as "no more than N endpoint families"; -- hard caps, such as rejecting `**` unless the maximum explicitly grants it; -- reviewer-facing explanations that identify why a change is too broad. +Why: the candidate still fits under a maximum policy if that maximum is broad +enough, but it is not a narrow update over the current policy. This is the +mechanism that can pressure agents away from requesting lazy `**` access. This spike should not over-design the product surface yet. The useful next proof -is a small set of tests showing whether Z3 can produce and classify policy -deltas well enough to enforce simple budgets. +is validating whether this budget shape is useful enough for policy proposal +auto-approval, or whether we need richer semantic categories before productizing +it. ## Current Test Command @@ -236,12 +343,16 @@ envelope::tests::l4_candidate_exceeds_l7_maximum envelope::tests::maximum_wildcards_cover_exact_candidate envelope::tests::deny_rules_are_unsupported_until_modeled envelope::tests::query_graphql_cidr_and_mcp_surfaces_are_unsupported +envelope::tests::narrowness_allows_one_exact_path_delta_within_budget +envelope::tests::narrowness_allows_one_exact_method_delta_within_budget +envelope::tests::narrowness_rejects_multiple_exact_grants_over_budget +envelope::tests::narrowness_rejects_recursive_path_glob_as_too_broad ``` ## Readout This validates the product shape for REST/path/binary/host/port maximum-policy -envelopes with a symbolic Z3 counterexample query. The next research step on -this branch is a narrowness budget proof over policy deltas. Deny rules, MCP, -GraphQL, query constraints, and CIDR can land as follow-on modeled surfaces once -the containment and delta mechanics are proven useful. +envelopes and narrowness budgets with symbolic Z3 counterexample queries. Deny +rules, MCP, GraphQL, query constraints, CIDR, and L4-only endpoints can land as +follow-on modeled surfaces once the containment and delta mechanics are proven +useful. diff --git a/crates/openshell-prover/README.md b/crates/openshell-prover/README.md index db6c9f67d..04fd55bb0 100644 --- a/crates/openshell-prover/README.md +++ b/crates/openshell-prover/README.md @@ -61,14 +61,20 @@ modeled yet. It returns: is broader. - `Unsupported` when either policy uses a surface not modeled yet, such as deny rules, query constraints, GraphQL controls, MCP controls, - endpoint path scoping, or CIDR-only `allowed_ips`. + endpoint path scoping, CIDR-only `allowed_ips`, or L4-only endpoints. Unsupported is intentionally fail-closed. Future work can flip those fixtures to modeled results as deny rules, MCP, GraphQL, and richer -symbolic path/query encodings land. See +symbolic path/query encodings land. + +The spike also includes a narrowness-budget check for candidate updates +against the current policy. It uses the same symbolic action model to +prove whether candidate grants add reach, then scores the shape of the +delta so exact grants can fit a small budget while broad globs such as +`**` exceed it. See [`MAXIMUM_POLICY_ENVELOPE_SPIKE.md`](MAXIMUM_POLICY_ENVELOPE_SPIKE.md) -for a walkthrough of the current spike behavior and the companion -narrowness-budget direction. +for a walkthrough of the current maximum-policy and narrowness-budget +behavior. ## Evidence shape diff --git a/crates/openshell-prover/src/envelope.rs b/crates/openshell-prover/src/envelope.rs index 1b64eeb1c..066f960ad 100644 --- a/crates/openshell-prover/src/envelope.rs +++ b/crates/openshell-prover/src/envelope.rs @@ -7,7 +7,7 @@ //! given a security-approved maximum policy and a candidate policy, does the //! candidate allow any modeled action outside the maximum envelope? -use std::str::FromStr; +use std::{collections::BTreeSet, str::FromStr}; use crate::policy::{Endpoint, L7Rule, NetworkPolicyRule, PolicyModel}; use z3::ast::{Bool, Int, Regexp, String as Z3String}; @@ -46,6 +46,102 @@ pub struct PolicyCounterexample { pub reason: String, } +/// Budget for a candidate policy's modeled scope increase over the current policy. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct NarrownessBudget { + /// Maximum number of modeled candidate grants that add new reach. + pub max_delta_grants: usize, + /// Maximum total score across all modeled delta grants. + pub max_total_score: u32, + /// Whether candidate delta grants may use modeled recursive globs (`**`). + pub allow_recursive_globs: bool, +} + +impl NarrownessBudget { + /// Conservative spike budget: one small exact grant, no recursive globs. + pub const fn one_exact_grant() -> Self { + Self { + max_delta_grants: 1, + max_total_score: 1, + allow_recursive_globs: false, + } + } +} + +/// Result of checking whether a candidate policy is a narrow update over current. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum NarrownessCheck { + /// The candidate adds no modeled reach over the current policy. + NoIncrease, + /// The candidate adds modeled reach, but it fits the supplied budget. + WithinBudget { + /// Summary of the modeled scope increase. + summary: NarrownessSummary, + }, + /// The candidate adds modeled reach outside the supplied budget. + ExceedsBudget { + /// Summary of the modeled scope increase. + summary: NarrownessSummary, + }, + /// The policy uses a surface the first narrowness slice does not model. + Unsupported { + /// Human-readable reason. The check must fail closed at callers. + reason: String, + }, +} + +/// Summary of the modeled scope increase from current policy to candidate policy. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct NarrownessSummary { + pub total_score: u32, + pub delta_grants: Vec, +} + +/// One modeled candidate grant that adds reach over the current policy. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct ScopeDelta { + pub rule_name: String, + pub binary: String, + pub host: String, + pub port: u16, + pub protocol: String, + pub method: String, + pub path: String, + pub score: u32, + pub reasons: Vec, + pub counterexample: PolicyCounterexample, +} + +/// Coarse reasons used by the spike budget scorer. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum ScopeIncreaseReason { + NewGrant, + PathWildcard, + HostWildcard, + BinaryWildcard, + RecursivePathGlob, + RecursiveHostGlob, + RecursiveBinaryGlob, +} + +impl ScopeIncreaseReason { + fn score(self) -> u32 { + match self { + Self::NewGrant => 1, + Self::PathWildcard => 2, + Self::HostWildcard | Self::BinaryWildcard => 3, + Self::RecursivePathGlob | Self::RecursiveHostGlob | Self::RecursiveBinaryGlob => 6, + } + } + + fn is_recursive(self) -> bool { + matches!( + self, + Self::RecursivePathGlob | Self::RecursiveHostGlob | Self::RecursiveBinaryGlob + ) + } +} + struct SymbolicAction { binary: Z3String, host: Z3String, @@ -55,6 +151,18 @@ struct SymbolicAction { path: Z3String, } +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)] +struct ModeledGrant { + rule_name: String, + binary: String, + host: String, + port: u16, + protocol: String, + method_label: String, + methods: Vec, + path: String, +} + /// Check whether `candidate` is semantically contained by `maximum` for the /// currently modeled allow surface. pub fn check_within_maximum(maximum: &PolicyModel, candidate: &PolicyModel) -> MaximumPolicyCheck { @@ -74,6 +182,72 @@ pub fn check_within_maximum(maximum: &PolicyModel, candidate: &PolicyModel) -> M } } +/// Check whether `candidate` is a narrow modeled update over `current`. +/// +/// The spike budget is intentionally coarse: Z3 proves whether each candidate +/// grant adds any action outside the current policy, then Rust scores the shape +/// of those delta grants so broad globs consume more budget than exact grants. +pub fn check_narrowness( + current: &PolicyModel, + candidate: &PolicyModel, + budget: &NarrownessBudget, +) -> NarrownessCheck { + if let Some(reason) = unsupported_reason("current", current) { + return NarrownessCheck::Unsupported { reason }; + } + if let Some(reason) = unsupported_reason("candidate", candidate) { + return NarrownessCheck::Unsupported { reason }; + } + + let mut delta_grants = Vec::new(); + for grant in modeled_grants(candidate) { + match find_z3_grant_delta(current, &grant) { + Z3GrantDelta::NoIncrease => {} + Z3GrantDelta::Increases { counterexample } => { + let (score, reasons) = score_grant(&grant); + delta_grants.push(ScopeDelta { + rule_name: grant.rule_name, + binary: grant.binary, + host: grant.host, + port: grant.port, + protocol: grant.protocol, + method: grant.method_label, + path: grant.path, + score, + reasons, + counterexample, + }); + } + Z3GrantDelta::Unsupported { reason } => { + return NarrownessCheck::Unsupported { reason }; + } + } + } + + if delta_grants.is_empty() { + return NarrownessCheck::NoIncrease; + } + + let total_score = delta_grants.iter().map(|delta| delta.score).sum(); + let exceeds_budget = delta_grants.len() > budget.max_delta_grants + || total_score > budget.max_total_score + || (!budget.allow_recursive_globs + && delta_grants + .iter() + .flat_map(|delta| delta.reasons.iter()) + .any(|reason| reason.is_recursive())); + let summary = NarrownessSummary { + total_score, + delta_grants, + }; + + if exceeds_budget { + NarrownessCheck::ExceedsBudget { summary } + } else { + NarrownessCheck::WithinBudget { summary } + } +} + enum Z3EnvelopeResult { WithinMax, ExceedsMax { @@ -84,29 +258,20 @@ enum Z3EnvelopeResult { }, } +enum Z3GrantDelta { + NoIncrease, + Increases { + counterexample: PolicyCounterexample, + }, + Unsupported { + reason: String, + }, +} + fn find_z3_violation(maximum: &PolicyModel, candidate: &PolicyModel) -> Z3EnvelopeResult { - let _ctx = Context::thread_local(); let solver = Solver::new(); - let action = SymbolicAction { - binary: Z3String::new_const("action_binary"), - host: Z3String::new_const("action_host"), - port: Int::new_const("action_port"), - protocol: Z3String::new_const("action_protocol"), - method: Z3String::new_const("action_method"), - path: Z3String::new_const("action_path"), - }; - - solver.assert(action.binary.regex_matches(&glob_regex("/**", "/"))); - solver.assert(action.host.regex_matches(&Regexp::full())); - solver.assert(Int::from_u64(1).le(&action.port)); - solver.assert(action.port.le(65535)); - solver.assert(str_eq_any(&action.protocol, &["rest"])); - solver.assert(str_eq_any(&action.method, ALL_METHODS)); - solver.assert( - Z3String::from_str("/") - .expect("literal") - .prefix(&action.path), - ); + let action = symbolic_action("action"); + assert_action_domain(&solver, &action); let candidate_allows = policy_allows(candidate, &action); let maximum_allows = policy_allows(maximum, &action); @@ -125,7 +290,11 @@ fn find_z3_violation(maximum: &PolicyModel, candidate: &PolicyModel) -> Z3Envelo .to_owned(), }; }; - let Some(counterexample) = counterexample_from_model(&model, &action) else { + let Some(counterexample) = counterexample_from_model( + &model, + &action, + "candidate allows an action outside the maximum policy", + ) else { return Z3EnvelopeResult::Unsupported { reason: "Z3 returned sat but the model could not be decoded into a maximum-policy counterexample".to_owned(), }; @@ -135,6 +304,66 @@ fn find_z3_violation(maximum: &PolicyModel, candidate: &PolicyModel) -> Z3Envelo } } +fn find_z3_grant_delta(current: &PolicyModel, grant: &ModeledGrant) -> Z3GrantDelta { + let solver = Solver::new(); + let action = symbolic_action("narrowness_action"); + assert_action_domain(&solver, &action); + + let current_allows = policy_allows(current, &action); + let grant_allows = grant_allows(grant, &action); + solver.assert(Bool::and(&[grant_allows, !current_allows])); + + match solver.check() { + SatResult::Unsat => Z3GrantDelta::NoIncrease, + SatResult::Unknown => Z3GrantDelta::Unsupported { + reason: "Z3 returned unknown while checking policy narrowness".to_owned(), + }, + SatResult::Sat => { + let Some(model) = solver.get_model() else { + return Z3GrantDelta::Unsupported { + reason: "Z3 returned sat without a model for policy narrowness".to_owned(), + }; + }; + let Some(counterexample) = counterexample_from_model( + &model, + &action, + "candidate grant allows an action outside the current policy", + ) else { + return Z3GrantDelta::Unsupported { + reason: "Z3 returned sat but the model could not be decoded into a policy narrowness counterexample".to_owned(), + }; + }; + Z3GrantDelta::Increases { counterexample } + } + } +} + +fn symbolic_action(name: &str) -> SymbolicAction { + let _ctx = Context::thread_local(); + SymbolicAction { + binary: Z3String::new_const(format!("{name}_binary")), + host: Z3String::new_const(format!("{name}_host")), + port: Int::new_const(format!("{name}_port")), + protocol: Z3String::new_const(format!("{name}_protocol")), + method: Z3String::new_const(format!("{name}_method")), + path: Z3String::new_const(format!("{name}_path")), + } +} + +fn assert_action_domain(solver: &Solver, action: &SymbolicAction) { + solver.assert(action.binary.regex_matches(&glob_regex("/**", "/"))); + solver.assert(action.host.regex_matches(&Regexp::full())); + solver.assert(Int::from_u64(1).le(&action.port)); + solver.assert(action.port.le(65535)); + solver.assert(str_eq_any(&action.protocol, &["rest"])); + solver.assert(str_eq_any(&action.method, ALL_METHODS)); + solver.assert( + Z3String::from_str("/") + .expect("literal") + .prefix(&action.path), + ); +} + fn policy_allows(policy: &PolicyModel, action: &SymbolicAction) -> Bool { bool_or( policy @@ -187,9 +416,23 @@ fn endpoint_allows(endpoint: &Endpoint, action: &SymbolicAction) -> Bool { Bool::and(&constraints) } +fn grant_allows(grant: &ModeledGrant, action: &SymbolicAction) -> Bool { + Bool::and(&[ + action.binary.regex_matches(&glob_regex(&grant.binary, "/")), + action + .host + .regex_matches(&glob_regex(&grant.host.to_ascii_lowercase(), ".")), + action.port.eq(Int::from_u64(u64::from(grant.port))), + action.protocol.eq(grant.protocol.as_str()), + str_eq_any_owned(&action.method, &grant.methods), + action.path.regex_matches(&glob_regex(&grant.path, "/")), + ]) +} + fn counterexample_from_model( model: &z3::Model, action: &SymbolicAction, + reason: &str, ) -> Option { let port = model.eval(&action.port, true)?.as_u64()?; Some(PolicyCounterexample { @@ -199,7 +442,7 @@ fn counterexample_from_model( protocol: model.eval(&action.protocol, true)?.as_string()?, method: model.eval(&action.method, true)?.as_string()?, path: model.eval(&action.path, true)?.as_string()?, - reason: "candidate allows an action outside the maximum policy".to_owned(), + reason: reason.to_owned(), }) } @@ -216,6 +459,10 @@ fn str_eq_any(value: &Z3String, options: &[&str]) -> Bool { bool_or(options.iter().map(|option| value.eq(*option))) } +fn str_eq_any_owned(value: &Z3String, options: &[String]) -> Bool { + bool_or(options.iter().map(|option| value.eq(option.as_str()))) +} + fn glob_regex(pattern: &str, separator: &str) -> Regexp { if pattern == "**" { return Regexp::full(); @@ -255,7 +502,7 @@ fn unsupported_reason(prefix: &str, policy: &PolicyModel) -> Option { for endpoint in &rule.endpoints { if !endpoint.path.is_empty() { return Some(format!( - "{prefix} policy rule '{rule_name}' uses endpoint path scoping, which maximum containment does not model yet" + "{prefix} policy rule '{rule_name}' uses endpoint path scoping, which policy envelope checks do not model yet" )); } if unsupported_glob_pattern(&endpoint.host) { @@ -265,12 +512,12 @@ fn unsupported_reason(prefix: &str, policy: &PolicyModel) -> Option { } if !endpoint.allowed_ips.is_empty() { return Some(format!( - "{prefix} policy rule '{rule_name}' uses allowed_ips/CIDR scoping, which maximum containment does not model yet" + "{prefix} policy rule '{rule_name}' uses allowed_ips/CIDR scoping, which policy envelope checks do not model yet" )); } if !endpoint.deny_rules.is_empty() { return Some(format!( - "{prefix} policy rule '{rule_name}' uses deny_rules, which maximum containment does not model yet" + "{prefix} policy rule '{rule_name}' uses deny_rules, which policy envelope checks do not model yet" )); } if endpoint.effective_ports().is_empty() { @@ -281,7 +528,7 @@ fn unsupported_reason(prefix: &str, policy: &PolicyModel) -> Option { } if !endpoint.tls.is_empty() { return Some(format!( - "{prefix} policy rule '{rule_name}' uses tls '{}', which maximum containment does not model yet", + "{prefix} policy rule '{rule_name}' uses tls '{}', which policy envelope checks do not model yet", endpoint.tls )); } @@ -290,7 +537,7 @@ fn unsupported_reason(prefix: &str, policy: &PolicyModel) -> Option { || endpoint.request_body_credential_rewrite { return Some(format!( - "{prefix} policy rule '{rule_name}' uses endpoint behavior flags that maximum containment does not model yet" + "{prefix} policy rule '{rule_name}' uses endpoint behavior flags that policy envelope checks do not model yet" )); } if !endpoint.persisted_queries.is_empty() @@ -298,7 +545,7 @@ fn unsupported_reason(prefix: &str, policy: &PolicyModel) -> Option { || endpoint.graphql_max_body_bytes != 0 { return Some(format!( - "{prefix} policy rule '{rule_name}' uses GraphQL persisted-query controls, which maximum containment does not model yet" + "{prefix} policy rule '{rule_name}' uses GraphQL persisted-query controls, which policy envelope checks do not model yet" )); } if !endpoint.mcp_server.is_empty() @@ -306,18 +553,23 @@ fn unsupported_reason(prefix: &str, policy: &PolicyModel) -> Option { || !endpoint.mcp_resource.is_empty() { return Some(format!( - "{prefix} policy rule '{rule_name}' uses MCP controls, which maximum containment does not model yet" + "{prefix} policy rule '{rule_name}' uses MCP controls, which policy envelope checks do not model yet" )); } if normalized_protocol(&endpoint.protocol) == "graphql" { return Some(format!( - "{prefix} policy rule '{rule_name}' uses GraphQL protocol controls, which maximum containment does not model yet" + "{prefix} policy rule '{rule_name}' uses GraphQL protocol controls, which policy envelope checks do not model yet" )); } let protocol = normalized_protocol(&endpoint.protocol); + if protocol.is_empty() { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses L4-only endpoint, which policy envelope checks do not model beyond REST yet" + )); + } if !protocol.is_empty() && !protocol.eq_ignore_ascii_case("rest") { return Some(format!( - "{prefix} policy rule '{rule_name}' uses protocol '{}', which maximum containment does not model yet", + "{prefix} policy rule '{rule_name}' uses protocol '{}', which policy envelope checks do not model yet", endpoint.protocol )); } @@ -330,12 +582,12 @@ fn unsupported_reason(prefix: &str, policy: &PolicyModel) -> Option { for rule in &endpoint.rules { if l7_rule_is_unsupported(rule) { return Some(format!( - "{prefix} policy rule '{rule_name}' uses L7 query, SQL, or GraphQL allow controls, which maximum containment does not model yet" + "{prefix} policy rule '{rule_name}' uses L7 query, SQL, or GraphQL allow controls, which policy envelope checks do not model yet" )); } if !rule.method.is_empty() && !modeled_rest_method(&rule.method) { return Some(format!( - "{prefix} policy rule '{rule_name}' uses REST method '{}', which maximum containment does not model yet", + "{prefix} policy rule '{rule_name}' uses REST method '{}', which policy envelope checks do not model yet", rule.method )); } @@ -357,6 +609,144 @@ fn unsupported_reason(prefix: &str, policy: &PolicyModel) -> Option { None } +fn modeled_grants(policy: &PolicyModel) -> Vec { + let mut grants = BTreeSet::new(); + for (rule_name, rule) in &policy.network_policies { + for binary in &rule.binaries { + for endpoint in &rule.endpoints { + for port in endpoint.effective_ports() { + for (method_label, methods, path) in grant_method_groups(endpoint) { + grants.insert(ModeledGrant { + rule_name: rule_name.clone(), + binary: binary.path.clone(), + host: endpoint.host.clone(), + port, + protocol: "rest".to_owned(), + method_label, + methods, + path, + }); + } + } + } + } + } + grants.into_iter().collect() +} + +fn grant_method_groups(endpoint: &Endpoint) -> Vec<(String, Vec, String)> { + if normalized_protocol(&endpoint.protocol).is_empty() { + return vec![( + "*".to_owned(), + ALL_METHODS + .iter() + .map(|method| (*method).to_owned()) + .collect(), + "**".to_owned(), + )]; + } + + match endpoint.access.as_str() { + "read-only" => vec![( + "read-only".to_owned(), + READ_ONLY_METHODS + .iter() + .map(|method| (*method).to_owned()) + .collect(), + "**".to_owned(), + )], + "read-write" => vec![( + "read-write".to_owned(), + READ_WRITE_METHODS + .iter() + .map(|method| (*method).to_owned()) + .collect(), + "**".to_owned(), + )], + "full" => vec![( + "full".to_owned(), + ALL_METHODS + .iter() + .map(|method| (*method).to_owned()) + .collect(), + "**".to_owned(), + )], + _ if endpoint.rules.is_empty() => Vec::new(), + _ => endpoint + .rules + .iter() + .filter_map(|rule| { + if rule.method.is_empty() { + return None; + } + let path = if rule.path.is_empty() { + "**".to_owned() + } else { + rule.path.clone() + }; + let method = rule.method.to_ascii_uppercase(); + if method == "*" { + Some(( + "*".to_owned(), + ALL_METHODS + .iter() + .map(|method| (*method).to_owned()) + .collect(), + path, + )) + } else if method == "GET" { + Some(( + "GET".to_owned(), + vec!["GET".to_owned(), "HEAD".to_owned()], + path, + )) + } else { + Some((method.clone(), vec![method], path)) + } + }) + .collect(), + } +} + +fn score_grant(grant: &ModeledGrant) -> (u32, Vec) { + let mut reasons = vec![ScopeIncreaseReason::NewGrant]; + + add_glob_reasons( + &mut reasons, + &grant.path, + ScopeIncreaseReason::PathWildcard, + ScopeIncreaseReason::RecursivePathGlob, + ); + add_glob_reasons( + &mut reasons, + &grant.host, + ScopeIncreaseReason::HostWildcard, + ScopeIncreaseReason::RecursiveHostGlob, + ); + add_glob_reasons( + &mut reasons, + &grant.binary, + ScopeIncreaseReason::BinaryWildcard, + ScopeIncreaseReason::RecursiveBinaryGlob, + ); + + let score = reasons.iter().map(|reason| reason.score()).sum(); + (score, reasons) +} + +fn add_glob_reasons( + reasons: &mut Vec, + pattern: &str, + wildcard: ScopeIncreaseReason, + recursive: ScopeIncreaseReason, +) { + if pattern.contains("**") { + reasons.push(recursive); + } else if pattern.contains('*') { + reasons.push(wildcard); + } +} + fn l7_rule_is_unsupported(rule: &L7Rule) -> bool { !rule.command.is_empty() || !rule.query.is_empty() @@ -667,12 +1057,12 @@ network_policies: assert!(matches!( check_within_maximum(&maximum, &candidate), - MaximumPolicyCheck::ExceedsMax { .. } + MaximumPolicyCheck::Unsupported { .. } )); } #[test] - fn maximum_l4_covers_l7_candidate() { + fn l4_maximum_is_unsupported_until_modeled() { let maximum = policy( r" - host: api.github.com port: 443", @@ -683,10 +1073,26 @@ network_policies: gh_binary(), ); - assert_eq!( + assert!(matches!( check_within_maximum(&maximum, &candidate), - MaximumPolicyCheck::WithinMax + MaximumPolicyCheck::Unsupported { .. } + )); + } + + #[test] + fn rest_full_maximum_does_not_silently_cover_l4_candidate() { + let maximum = policy(&one_rest_endpoint(" access: full"), gh_binary()); + let candidate = policy( + r" - host: api.github.com + port: 443", + gh_binary(), ); + + let MaximumPolicyCheck::Unsupported { reason } = check_within_maximum(&maximum, &candidate) + else { + panic!("expected L4 candidate to fail closed"); + }; + assert!(reason.contains("L4-only endpoint")); } #[test] @@ -882,4 +1288,224 @@ network_policies: MaximumPolicyCheck::Unsupported { .. } )); } + + #[test] + fn narrowness_reports_no_increase_for_same_policy() { + let current = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123", + ), + gh_binary(), + ); + + assert_eq!( + check_narrowness(¤t, ¤t, &NarrownessBudget::one_exact_grant()), + NarrownessCheck::NoIncrease + ); + } + + #[test] + fn narrowness_allows_one_exact_path_delta_within_budget() { + let current = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123", + ), + gh_binary(), + ); + let candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123 + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/456", + ), + gh_binary(), + ); + + let NarrownessCheck::WithinBudget { summary } = + check_narrowness(¤t, &candidate, &NarrownessBudget::one_exact_grant()) + else { + panic!("expected one exact path delta to fit budget"); + }; + assert_eq!(summary.total_score, 1); + assert_eq!(summary.delta_grants.len(), 1); + assert_eq!(summary.delta_grants[0].method, "GET"); + assert_eq!( + summary.delta_grants[0].path, + "/repos/NVIDIA/OpenShell/issues/456" + ); + assert_eq!( + summary.delta_grants[0].reasons, + vec![ScopeIncreaseReason::NewGrant] + ); + } + + #[test] + fn narrowness_allows_one_exact_method_delta_within_budget() { + let current = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123", + ), + gh_binary(), + ); + let candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123 + - allow: + method: POST + path: /repos/NVIDIA/OpenShell/issues/123", + ), + gh_binary(), + ); + + let NarrownessCheck::WithinBudget { summary } = + check_narrowness(¤t, &candidate, &NarrownessBudget::one_exact_grant()) + else { + panic!("expected one exact method delta to fit budget"); + }; + assert_eq!(summary.total_score, 1); + assert_eq!(summary.delta_grants.len(), 1); + assert_eq!(summary.delta_grants[0].method, "POST"); + assert_eq!( + summary.delta_grants[0].counterexample.reason, + "candidate grant allows an action outside the current policy" + ); + } + + #[test] + fn narrowness_rejects_multiple_exact_grants_over_budget() { + let current = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123", + ), + gh_binary(), + ); + let candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123 + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/456 + - allow: + method: POST + path: /repos/NVIDIA/OpenShell/issues/123", + ), + gh_binary(), + ); + + let NarrownessCheck::ExceedsBudget { summary } = + check_narrowness(¤t, &candidate, &NarrownessBudget::one_exact_grant()) + else { + panic!("expected two exact deltas to exceed one-grant budget"); + }; + assert_eq!(summary.total_score, 2); + assert_eq!(summary.delta_grants.len(), 2); + } + + #[test] + fn narrowness_rejects_recursive_path_glob_as_too_broad() { + let current = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123", + ), + gh_binary(), + ); + let candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/**", + ), + gh_binary(), + ); + + let NarrownessCheck::ExceedsBudget { summary } = + check_narrowness(¤t, &candidate, &NarrownessBudget::one_exact_grant()) + else { + panic!("expected recursive path glob to exceed budget"); + }; + assert_eq!(summary.delta_grants.len(), 1); + assert_eq!(summary.total_score, 7); + assert_eq!( + summary.delta_grants[0].reasons, + vec![ + ScopeIncreaseReason::NewGrant, + ScopeIncreaseReason::RecursivePathGlob + ] + ); + } + + #[test] + fn narrowness_recursive_glob_can_fit_when_budget_explicitly_allows_it() { + let current = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/OpenShell/issues/123", + ), + gh_binary(), + ); + let candidate = policy( + &one_rest_endpoint( + r" rules: + - allow: + method: GET + path: /repos/NVIDIA/**", + ), + gh_binary(), + ); + let budget = NarrownessBudget { + max_delta_grants: 1, + max_total_score: 7, + allow_recursive_globs: true, + }; + + assert!(matches!( + check_narrowness(¤t, &candidate, &budget), + NarrownessCheck::WithinBudget { .. } + )); + } + + #[test] + fn narrowness_l4_candidate_is_unsupported_until_modeled() { + let current = policy(&one_rest_endpoint(" access: full"), gh_binary()); + let candidate = policy( + r" - host: api.github.com + port: 443", + gh_binary(), + ); + + let NarrownessCheck::Unsupported { reason } = + check_narrowness(¤t, &candidate, &NarrownessBudget::one_exact_grant()) + else { + panic!("expected L4 candidate to fail closed"); + }; + assert!(reason.contains("L4-only endpoint")); + } } From df0ee1aaaf6af7ee6193b785fd189449a3848fe0 Mon Sep 17 00:00:00 2001 From: Alexander Watson Date: Tue, 9 Jun 2026 15:37:59 -0700 Subject: [PATCH 3/3] feat(policy): model l4 envelope and narrowness checks --- .../MAXIMUM_POLICY_ENVELOPE_SPIKE.md | 179 +++- crates/openshell-prover/README.md | 22 +- crates/openshell-prover/src/envelope.rs | 832 ++++++++++++++++-- 3 files changed, 930 insertions(+), 103 deletions(-) diff --git a/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md b/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md index b915606d6..8a5b99a1f 100644 --- a/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md +++ b/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md @@ -17,13 +17,25 @@ exists x: Rust normalizes schema-level OpenShell policy semantics, such as access presets and unsupported field detection. Z3 owns the action variables (`binary`, `host`, -`port`, `protocol`, `method`, and `path`) and checks whether any symbolic action -is allowed by the candidate but not by the maximum. Host, path, and binary globs +`port`, `layer`, `method`, and `path`) and checks whether any symbolic action is +allowed by the candidate but not by the maximum. Host, path, and binary globs compile to Z3 regular-expression constraints. If the solver finds such an `x`, the candidate exceeds the maximum. If no such `x` exists, the candidate is within the modeled maximum. If either policy uses a surface the spike does not model yet, the check fails closed as `Unsupported`. +The first modeled action layers are: + +```text +L4: binary, host, port +REST: binary, host, port, method, path +WebSocket: binary, host, port, method, path +``` + +An L4 endpoint is broader than inspected protocols: it covers raw L4, REST, and +WebSocket actions on the same binary/host/port. REST and WebSocket endpoints +cover only their own inspected action layer. + ## Demo 1: Narrow Candidate Within Maximum Maximum: @@ -155,11 +167,66 @@ port: 443 -> [443, 8443] Why: each change creates at least one action that the maximum does not allow. -L4-only endpoints are not modeled in this spike. They fail closed as -`Unsupported` rather than being compared against the REST-only symbolic action -domain. +## Demo 5: L4, REST, And WebSocket Layering + +An L4 maximum covers a narrower REST candidate on the same binary/host/port: + +```yaml +maximum: + endpoints: + - host: api.github.com + port: 443 + +candidate: + endpoints: + - host: api.github.com + port: 443 + protocol: rest + enforcement: enforce + access: read-write +``` + +Result: + +```text +WithinMax +``` + +A REST maximum does not cover a raw L4 candidate: -## Demo 5: Unsupported Surfaces Fail Closed +```text +ExceedsMax { + protocol: "l4", + host: "api.github.com", + port: 443, + ... +} +``` + +Why: raw L4 egress is broader and less inspected than an enforced REST or +WebSocket surface. + +WebSocket endpoints are modeled as their own inspected layer with `GET` and +`WEBSOCKET_TEXT` actions. `read-only` WebSocket access covers the opening +`GET`, not text send authority. Credential rewrite flags fail closed until the +prover has an explicit authority check for introducing credential injection. + +## Demo 6: Credentialed L4 Is A Separate High-Risk Check + +The spike also includes a separate check for uninspected credentialed L4 reach: + +```text +exists x: + policy_allows(x) + AND x.layer = L4 + AND credential_target_matches(x.host) +``` + +This is intentionally separate from maximum containment. It lets product policy +decide whether credentialed L4 should be explicitly allowed, auto-denied, or +sent to human review without changing the meaning of the signed maximum. + +## Demo 7: Unsupported Surfaces Fail Closed Maximum: @@ -189,7 +256,7 @@ GraphQL operation and field constraints MCP tool/resource constraints CIDR-only allowed_ips endpoint path scoping -L4-only endpoints +credential rewrite flags ``` ## Narrowness Companion @@ -227,9 +294,11 @@ exact new grant: +1 single path wildcard: +2 host/binary wildcard: +3 recursive glob (**): +6 +L7-to-L4 broadening: +8 ``` -A conservative budget can allow one exact grant and reject recursive globs: +A conservative budget can allow one exact grant, including an exact L4 +host/port grant, while rejecting recursive globs and L7-to-L4 broadening: ```rust NarrownessBudget { @@ -239,7 +308,12 @@ NarrownessBudget { } ``` -## Demo 6: One Exact Path Fits A Narrow Budget +Credentialed raw L4 is handled by the separate credentialed-L4 check above. A +production auto-approval gate can combine that result with this budget, for +example by assigning a high score or requiring human review when raw L4 reaches +a credential target. + +## Demo 8: One Exact Path Fits A Narrow Budget Current: @@ -280,7 +354,59 @@ WithinBudget { Why: the candidate adds one exact modeled grant. The grant allows both `GET` and runtime-implied `HEAD`, but the budget counts the source grant once. -## Demo 7: Lazy Recursive Path Exceeds A Narrow Budget +## Demo 9: Exact L4 Versus L7-To-L4 Broadening + +An exact L4 grant to a new normal host is still one exact grant: + +```yaml +candidate: + endpoints: + - host: files.pythonhosted.org + port: 443 +``` + +Result: + +```text +WithinBudget { + total_score: 1, + reasons: [NewGrant] +} +``` + +If the current policy already has inspected REST/WebSocket access for the same +authority and the candidate asks for raw L4, the same exact host/port becomes a +larger jump: + +```yaml +current: + endpoints: + - host: api.github.com + port: 443 + protocol: rest + enforcement: enforce + access: full + +candidate: + endpoints: + - host: api.github.com + port: 443 +``` + +Result: + +```text +ExceedsBudget { + total_score: 9, + reasons: [NewGrant, L7ToL4Broadening] +} +``` + +Why: the candidate is not just adding a host. It is replacing inspected +method/path reasoning with raw host/port authority for a service the current +policy already modeled at L7. + +## Demo 10: Lazy Recursive Path Exceeds A Narrow Budget Current: @@ -330,29 +456,22 @@ it. mise exec -- cargo test -p openshell-prover ``` -Maximal-policy tests include: +Coverage includes: ```text -envelope::tests::exact_rest_rule_is_within_maximum -envelope::tests::broader_rest_path_exceeds_maximum -envelope::tests::method_escalation_exceeds_maximum -envelope::tests::host_wildcard_broadening_exceeds_maximum -envelope::tests::binary_wildcard_broadening_exceeds_maximum -envelope::tests::port_broadening_exceeds_maximum -envelope::tests::l4_candidate_exceeds_l7_maximum -envelope::tests::maximum_wildcards_cover_exact_candidate -envelope::tests::deny_rules_are_unsupported_until_modeled -envelope::tests::query_graphql_cidr_and_mcp_surfaces_are_unsupported -envelope::tests::narrowness_allows_one_exact_path_delta_within_budget -envelope::tests::narrowness_allows_one_exact_method_delta_within_budget -envelope::tests::narrowness_rejects_multiple_exact_grants_over_budget -envelope::tests::narrowness_rejects_recursive_path_glob_as_too_broad +REST method/path/host/binary/port containment +L4 versus REST/WebSocket layer containment +WebSocket text-send and read-only behavior +credentialed raw L4 detection +fail-closed unsupported deny/query/GraphQL/MCP/CIDR/rewrite surfaces +exact, wildcard, recursive-glob, L4, and WebSocket narrowness deltas +representative provider-shaped accept/reject cases ``` ## Readout -This validates the product shape for REST/path/binary/host/port maximum-policy -envelopes and narrowness budgets with symbolic Z3 counterexample queries. Deny -rules, MCP, GraphQL, query constraints, CIDR, and L4-only endpoints can land as -follow-on modeled surfaces once the containment and delta mechanics are proven -useful. +This validates the product shape for L4, REST, and WebSocket maximum-policy +envelopes, narrowness budgets, and uninspected credentialed L4 detection with +symbolic Z3 counterexample queries. Deny rules, MCP, GraphQL, query constraints, +and CIDR can land as follow-on modeled surfaces once the containment and delta +mechanics are proven useful. diff --git a/crates/openshell-prover/README.md b/crates/openshell-prover/README.md index 04fd55bb0..66cfd2032 100644 --- a/crates/openshell-prover/README.md +++ b/crates/openshell-prover/README.md @@ -46,14 +46,16 @@ exists x: AND NOT maximum_allows(x) ``` -The first implementation models REST allow surfaces for binaries, -hosts, ports, protocols, methods, paths, access presets, and the +The first implementation models L4, REST, and WebSocket allow surfaces +for binaries, hosts, ports, methods, paths, access presets, and the supported host/path/binary glob subset. Rust normalizes policy schema details such as access presets and fail-closed unsupported fields, then encodes candidate and maximum allow predicates as Z3 constraints over -symbolic action variables (`binary`, `host`, `port`, `protocol`, -`method`, and `path`). Host, path, and binary globs are encoded as Z3 -regular-expression membership constraints. Query parameters are not +symbolic action variables (`binary`, `host`, `port`, `layer`, `method`, +and `path`). L4 endpoints cover raw L4, REST, and WebSocket actions on +the same binary/host/port; REST and WebSocket endpoints cover only their +own inspected action layer. Host, path, and binary globs are encoded as +Z3 regular-expression membership constraints. Query parameters are not modeled yet. It returns: - `WithinMax` when every modeled candidate action is covered. @@ -61,7 +63,8 @@ modeled yet. It returns: is broader. - `Unsupported` when either policy uses a surface not modeled yet, such as deny rules, query constraints, GraphQL controls, MCP controls, - endpoint path scoping, CIDR-only `allowed_ips`, or L4-only endpoints. + endpoint path scoping, credential rewrite flags, or CIDR-only + `allowed_ips`. Unsupported is intentionally fail-closed. Future work can flip those fixtures to modeled results as deny rules, MCP, GraphQL, and richer @@ -71,11 +74,16 @@ The spike also includes a narrowness-budget check for candidate updates against the current policy. It uses the same symbolic action model to prove whether candidate grants add reach, then scores the shape of the delta so exact grants can fit a small budget while broad globs such as -`**` exceed it. See +`**` and L7-to-L4 broadening exceed the conservative default. See [`MAXIMUM_POLICY_ENVELOPE_SPIKE.md`](MAXIMUM_POLICY_ENVELOPE_SPIKE.md) for a walkthrough of the current maximum-policy and narrowness-budget behavior. +The spike also exposes a credentialed-L4 check that asks whether any +modeled raw L4 action can reach a credential target. This keeps +uninspected credentialed authority separate from plain outbound egress +and from the maximum-policy containment proof. + ## Evidence shape Each finding carries one or more [`FindingPath::Exfil`](src/finding.rs) diff --git a/crates/openshell-prover/src/envelope.rs b/crates/openshell-prover/src/envelope.rs index 066f960ad..56fa0f7d0 100644 --- a/crates/openshell-prover/src/envelope.rs +++ b/crates/openshell-prover/src/envelope.rs @@ -9,6 +9,7 @@ use std::{collections::BTreeSet, str::FromStr}; +use crate::credentials::CredentialSet; use crate::policy::{Endpoint, L7Rule, NetworkPolicyRule, PolicyModel}; use z3::ast::{Bool, Int, Regexp, String as Z3String}; use z3::{Context, SatResult, Solver}; @@ -16,6 +17,20 @@ use z3::{Context, SatResult, Solver}; const READ_ONLY_METHODS: &[&str] = &["GET", "HEAD", "OPTIONS"]; const READ_WRITE_METHODS: &[&str] = &["GET", "HEAD", "OPTIONS", "POST", "PUT", "PATCH"]; const ALL_METHODS: &[&str] = &["GET", "HEAD", "OPTIONS", "POST", "PUT", "PATCH", "DELETE"]; +const WEBSOCKET_METHODS: &[&str] = &["GET", "WEBSOCKET_TEXT"]; +const ACTION_METHODS: &[&str] = &[ + "GET", + "HEAD", + "OPTIONS", + "POST", + "PUT", + "PATCH", + "DELETE", + "WEBSOCKET_TEXT", +]; +const LAYER_L4: &str = "l4"; +const LAYER_REST: &str = "rest"; +const LAYER_WEBSOCKET: &str = "websocket"; /// Result of checking whether a candidate policy is inside a maximum policy. #[derive(Debug, Clone, PartialEq, Eq)] @@ -40,6 +55,8 @@ pub struct PolicyCounterexample { pub binary: String, pub host: String, pub port: u16, + /// Modeled action layer (`l4`, `rest`, or `websocket`) retained under the + /// policy protocol field name for this spike. pub protocol: String, pub method: String, pub path: String, @@ -58,7 +75,7 @@ pub struct NarrownessBudget { } impl NarrownessBudget { - /// Conservative spike budget: one small exact grant, no recursive globs. + /// Conservative spike budget: one small exact grant. pub const fn one_exact_grant() -> Self { Self { max_delta_grants: 1, @@ -90,6 +107,23 @@ pub enum NarrownessCheck { }, } +/// Result of checking for credentialed authority over uninspected L4 egress. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum CredentialedL4Check { + /// No modeled L4 action reaches a credential target. + NoUninspectedCredentialedL4, + /// The policy allows at least one uninspected L4 action to a credential target. + HasUninspectedCredentialedL4 { + /// Representative action allowed by the policy. + counterexample: PolicyCounterexample, + }, + /// The policy uses a surface the first credentialed-L4 slice does not model. + Unsupported { + /// Human-readable reason. The check must fail closed at callers. + reason: String, + }, +} + /// Summary of the modeled scope increase from current policy to candidate policy. #[derive(Debug, Clone, PartialEq, Eq)] pub struct NarrownessSummary { @@ -104,6 +138,8 @@ pub struct ScopeDelta { pub binary: String, pub host: String, pub port: u16, + /// Modeled action layer (`l4`, `rest`, or `websocket`) retained under the + /// policy protocol field name for this spike. pub protocol: String, pub method: String, pub path: String, @@ -122,6 +158,7 @@ pub enum ScopeIncreaseReason { RecursivePathGlob, RecursiveHostGlob, RecursiveBinaryGlob, + L7ToL4Broadening, } impl ScopeIncreaseReason { @@ -131,6 +168,7 @@ impl ScopeIncreaseReason { Self::PathWildcard => 2, Self::HostWildcard | Self::BinaryWildcard => 3, Self::RecursivePathGlob | Self::RecursiveHostGlob | Self::RecursiveBinaryGlob => 6, + Self::L7ToL4Broadening => 8, } } @@ -146,7 +184,7 @@ struct SymbolicAction { binary: Z3String, host: Z3String, port: Int, - protocol: Z3String, + layer: Z3String, method: Z3String, path: Z3String, } @@ -157,7 +195,7 @@ struct ModeledGrant { binary: String, host: String, port: u16, - protocol: String, + layer: String, method_label: String, methods: Vec, path: String, @@ -204,13 +242,13 @@ pub fn check_narrowness( match find_z3_grant_delta(current, &grant) { Z3GrantDelta::NoIncrease => {} Z3GrantDelta::Increases { counterexample } => { - let (score, reasons) = score_grant(&grant); + let (score, reasons) = score_grant(current, &grant); delta_grants.push(ScopeDelta { rule_name: grant.rule_name, binary: grant.binary, host: grant.host, port: grant.port, - protocol: grant.protocol, + protocol: grant.layer, method: grant.method_label, path: grant.path, score, @@ -248,6 +286,52 @@ pub fn check_narrowness( } } +/// Check whether a policy grants uninspected L4 reach to any host with an +/// injected credential in scope. +pub fn check_uninspected_credentialed_l4( + policy: &PolicyModel, + credentials: &CredentialSet, +) -> CredentialedL4Check { + if let Some(reason) = unsupported_reason("policy", policy) { + return CredentialedL4Check::Unsupported { reason }; + } + + let solver = Solver::new(); + let action = symbolic_action("credentialed_l4_action"); + assert_action_domain(&solver, &action); + solver.assert(Bool::and(&[ + policy_allows(policy, &action), + action.layer.eq(LAYER_L4), + credential_target_matches(credentials, &action), + ])); + + match solver.check() { + SatResult::Unsat => CredentialedL4Check::NoUninspectedCredentialedL4, + SatResult::Unknown => CredentialedL4Check::Unsupported { + reason: "Z3 returned unknown while checking uninspected credentialed L4 reach" + .to_owned(), + }, + SatResult::Sat => { + let Some(model) = solver.get_model() else { + return CredentialedL4Check::Unsupported { + reason: "Z3 returned sat without a model for uninspected credentialed L4 reach" + .to_owned(), + }; + }; + let Some(counterexample) = counterexample_from_model( + &model, + &action, + "policy allows uninspected L4 reach to a credential target", + ) else { + return CredentialedL4Check::Unsupported { + reason: "Z3 returned sat but the model could not be decoded into an uninspected credentialed L4 counterexample".to_owned(), + }; + }; + CredentialedL4Check::HasUninspectedCredentialedL4 { counterexample } + } + } +} + enum Z3EnvelopeResult { WithinMax, ExceedsMax { @@ -344,7 +428,7 @@ fn symbolic_action(name: &str) -> SymbolicAction { binary: Z3String::new_const(format!("{name}_binary")), host: Z3String::new_const(format!("{name}_host")), port: Int::new_const(format!("{name}_port")), - protocol: Z3String::new_const(format!("{name}_protocol")), + layer: Z3String::new_const(format!("{name}_layer")), method: Z3String::new_const(format!("{name}_method")), path: Z3String::new_const(format!("{name}_path")), } @@ -355,8 +439,11 @@ fn assert_action_domain(solver: &Solver, action: &SymbolicAction) { solver.assert(action.host.regex_matches(&Regexp::full())); solver.assert(Int::from_u64(1).le(&action.port)); solver.assert(action.port.le(65535)); - solver.assert(str_eq_any(&action.protocol, &["rest"])); - solver.assert(str_eq_any(&action.method, ALL_METHODS)); + solver.assert(str_eq_any( + &action.layer, + &[LAYER_L4, LAYER_REST, LAYER_WEBSOCKET], + )); + solver.assert(str_eq_any(&action.method, ACTION_METHODS)); solver.assert( Z3String::from_str("/") .expect("literal") @@ -401,9 +488,9 @@ fn endpoint_allows(endpoint: &Endpoint, action: &SymbolicAction) -> Bool { .regex_matches(&glob_regex(&endpoint.host.to_ascii_lowercase(), ".")), ]; - if !normalized_protocol(&endpoint.protocol).is_empty() { - constraints.push(action.protocol.eq(normalized_protocol(&endpoint.protocol))); - constraints.push(bool_or(effective_rest_allows(endpoint).into_iter().map( + if let Some(layer) = endpoint_layer(endpoint) { + constraints.push(action.layer.eq(layer)); + constraints.push(bool_or(effective_l7_allows(endpoint).into_iter().map( |(method, path)| { Bool::and(&[ action.method.eq(method.as_str()), @@ -417,16 +504,46 @@ fn endpoint_allows(endpoint: &Endpoint, action: &SymbolicAction) -> Bool { } fn grant_allows(grant: &ModeledGrant, action: &SymbolicAction) -> Bool { - Bool::and(&[ + let mut constraints = vec![ action.binary.regex_matches(&glob_regex(&grant.binary, "/")), action .host .regex_matches(&glob_regex(&grant.host.to_ascii_lowercase(), ".")), action.port.eq(Int::from_u64(u64::from(grant.port))), - action.protocol.eq(grant.protocol.as_str()), - str_eq_any_owned(&action.method, &grant.methods), - action.path.regex_matches(&glob_regex(&grant.path, "/")), - ]) + ]; + + if grant.layer == LAYER_L4 { + constraints.push(str_eq_any( + &action.layer, + &[LAYER_L4, LAYER_REST, LAYER_WEBSOCKET], + )); + } else { + constraints.push(action.layer.eq(grant.layer.as_str())); + constraints.push(str_eq_any_owned(&action.method, &grant.methods)); + constraints.push(action.path.regex_matches(&glob_regex(&grant.path, "/"))); + } + + Bool::and(&constraints) +} + +fn credential_target_matches(credentials: &CredentialSet, action: &SymbolicAction) -> Bool { + bool_or( + credentials + .credentials + .iter() + .flat_map(|credential| credential.target_hosts.iter()) + .filter_map(|target| { + let normalized = target.trim().trim_end_matches('.'); + if normalized.is_empty() { + return None; + } + Some( + action + .host + .regex_matches(&glob_regex(&normalized.to_ascii_lowercase(), ".")), + ) + }), + ) } fn counterexample_from_model( @@ -435,13 +552,24 @@ fn counterexample_from_model( reason: &str, ) -> Option { let port = model.eval(&action.port, true)?.as_u64()?; + let layer = model.eval(&action.layer, true)?.as_string()?; + let method = if layer == LAYER_L4 { + String::new() + } else { + model.eval(&action.method, true)?.as_string()? + }; + let path = if layer == LAYER_L4 { + String::new() + } else { + model.eval(&action.path, true)?.as_string()? + }; Some(PolicyCounterexample { binary: model.eval(&action.binary, true)?.as_string()?, host: model.eval(&action.host, true)?.as_string()?, port: u16::try_from(port).ok()?, - protocol: model.eval(&action.protocol, true)?.as_string()?, - method: model.eval(&action.method, true)?.as_string()?, - path: model.eval(&action.path, true)?.as_string()?, + protocol: layer, + method, + path, reason: reason.to_owned(), }) } @@ -532,14 +660,16 @@ fn unsupported_reason(prefix: &str, policy: &PolicyModel) -> Option { endpoint.tls )); } - if endpoint.allow_encoded_slash - || endpoint.websocket_credential_rewrite - || endpoint.request_body_credential_rewrite - { + if endpoint.allow_encoded_slash { return Some(format!( "{prefix} policy rule '{rule_name}' uses endpoint behavior flags that policy envelope checks do not model yet" )); } + if endpoint.request_body_credential_rewrite || endpoint.websocket_credential_rewrite { + return Some(format!( + "{prefix} policy rule '{rule_name}' uses credential rewrite flags that policy envelope checks do not model yet" + )); + } if !endpoint.persisted_queries.is_empty() || !endpoint.graphql_persisted_queries.is_empty() || endpoint.graphql_max_body_bytes != 0 @@ -562,12 +692,10 @@ fn unsupported_reason(prefix: &str, policy: &PolicyModel) -> Option { )); } let protocol = normalized_protocol(&endpoint.protocol); - if protocol.is_empty() { - return Some(format!( - "{prefix} policy rule '{rule_name}' uses L4-only endpoint, which policy envelope checks do not model beyond REST yet" - )); - } - if !protocol.is_empty() && !protocol.eq_ignore_ascii_case("rest") { + if !protocol.is_empty() + && !protocol.eq_ignore_ascii_case("rest") + && !protocol.eq_ignore_ascii_case("websocket") + { return Some(format!( "{prefix} policy rule '{rule_name}' uses protocol '{}', which policy envelope checks do not model yet", endpoint.protocol @@ -585,9 +713,9 @@ fn unsupported_reason(prefix: &str, policy: &PolicyModel) -> Option { "{prefix} policy rule '{rule_name}' uses L7 query, SQL, or GraphQL allow controls, which policy envelope checks do not model yet" )); } - if !rule.method.is_empty() && !modeled_rest_method(&rule.method) { + if !rule.method.is_empty() && !modeled_l7_method(protocol, &rule.method) { return Some(format!( - "{prefix} policy rule '{rule_name}' uses REST method '{}', which policy envelope checks do not model yet", + "{prefix} policy rule '{rule_name}' uses method '{}', which policy envelope checks do not model yet", rule.method )); } @@ -621,7 +749,7 @@ fn modeled_grants(policy: &PolicyModel) -> Vec { binary: binary.path.clone(), host: endpoint.host.clone(), port, - protocol: "rest".to_owned(), + layer: endpoint_layer(endpoint).unwrap_or(LAYER_L4).to_owned(), method_label, methods, path, @@ -638,7 +766,7 @@ fn grant_method_groups(endpoint: &Endpoint) -> Vec<(String, Vec, String) if normalized_protocol(&endpoint.protocol).is_empty() { return vec![( "*".to_owned(), - ALL_METHODS + ACTION_METHODS .iter() .map(|method| (*method).to_owned()) .collect(), @@ -646,6 +774,10 @@ fn grant_method_groups(endpoint: &Endpoint) -> Vec<(String, Vec, String) )]; } + if normalized_protocol(&endpoint.protocol).eq_ignore_ascii_case("websocket") { + return websocket_grant_method_groups(endpoint); + } + match endpoint.access.as_str() { "read-only" => vec![( "read-only".to_owned(), @@ -708,15 +840,21 @@ fn grant_method_groups(endpoint: &Endpoint) -> Vec<(String, Vec, String) } } -fn score_grant(grant: &ModeledGrant) -> (u32, Vec) { +fn score_grant(current: &PolicyModel, grant: &ModeledGrant) -> (u32, Vec) { let mut reasons = vec![ScopeIncreaseReason::NewGrant]; - add_glob_reasons( - &mut reasons, - &grant.path, - ScopeIncreaseReason::PathWildcard, - ScopeIncreaseReason::RecursivePathGlob, - ); + if grant.layer == LAYER_L4 { + if grant_broadens_inspected_l7_to_l4(current, grant) { + reasons.push(ScopeIncreaseReason::L7ToL4Broadening); + } + } else { + add_glob_reasons( + &mut reasons, + &grant.path, + ScopeIncreaseReason::PathWildcard, + ScopeIncreaseReason::RecursivePathGlob, + ); + } add_glob_reasons( &mut reasons, &grant.host, @@ -734,6 +872,23 @@ fn score_grant(grant: &ModeledGrant) -> (u32, Vec) { (score, reasons) } +fn grant_broadens_inspected_l7_to_l4(current: &PolicyModel, grant: &ModeledGrant) -> bool { + if grant.layer != LAYER_L4 { + return false; + } + + let solver = Solver::new(); + let action = symbolic_action("l7_to_l4_overlap"); + assert_action_domain(&solver, &action); + solver.assert(Bool::and(&[ + grant_allows(grant, &action), + policy_allows(current, &action), + !action.layer.eq(LAYER_L4), + ])); + + matches!(solver.check(), SatResult::Sat) +} + fn add_glob_reasons( reasons: &mut Vec, pattern: &str, @@ -755,14 +910,71 @@ fn l7_rule_is_unsupported(rule: &L7Rule) -> bool { || !rule.fields.is_empty() } -fn effective_rest_allows(endpoint: &Endpoint) -> Vec<(String, String)> { +fn websocket_grant_method_groups(endpoint: &Endpoint) -> Vec<(String, Vec, String)> { + match endpoint.access.as_str() { + "read-only" => vec![( + "read-only".to_owned(), + vec!["GET".to_owned()], + "**".to_owned(), + )], + "read-write" | "full" => vec![( + endpoint.access.clone(), + WEBSOCKET_METHODS + .iter() + .map(|method| (*method).to_owned()) + .collect(), + "**".to_owned(), + )], + _ if endpoint.rules.is_empty() => Vec::new(), + _ => endpoint + .rules + .iter() + .filter_map(|rule| { + if rule.method.is_empty() { + return None; + } + let path = if rule.path.is_empty() { + "**".to_owned() + } else { + rule.path.clone() + }; + let method = rule.method.to_ascii_uppercase(); + if method == "*" { + Some(( + "*".to_owned(), + WEBSOCKET_METHODS + .iter() + .map(|method| (*method).to_owned()) + .collect(), + path, + )) + } else { + Some((method.clone(), vec![method], path)) + } + }) + .collect(), + } +} + +fn effective_l7_allows(endpoint: &Endpoint) -> Vec<(String, String)> { if normalized_protocol(&endpoint.protocol).is_empty() { - return ALL_METHODS + return ACTION_METHODS .iter() .map(|method| ((*method).to_owned(), "**".to_owned())) .collect(); } + if normalized_protocol(&endpoint.protocol).eq_ignore_ascii_case("websocket") { + return websocket_grant_method_groups(endpoint) + .into_iter() + .flat_map(|(_, methods, path)| { + methods + .into_iter() + .map(move |method| (method, path.clone())) + }) + .collect(); + } + match endpoint.access.as_str() { "read-only" => methods_with_path(READ_ONLY_METHODS, "**"), "read-write" => methods_with_path(READ_WRITE_METHODS, "**"), @@ -799,8 +1011,15 @@ fn methods_with_path(methods: &[&str], path: &str) -> Vec<(String, String)> { .collect() } -fn modeled_rest_method(method: &str) -> bool { - method == "*" || ALL_METHODS.contains(&method.to_ascii_uppercase().as_str()) +fn modeled_l7_method(protocol: &str, method: &str) -> bool { + if method == "*" { + return true; + } + let method = method.to_ascii_uppercase(); + if protocol.eq_ignore_ascii_case("websocket") { + return WEBSOCKET_METHODS.contains(&method.as_str()); + } + ALL_METHODS.contains(&method.as_str()) } fn unsupported_glob_pattern(pattern: &str) -> bool { @@ -813,6 +1032,17 @@ fn normalized_protocol(protocol: &str) -> &str { protocol.trim() } +fn endpoint_layer(endpoint: &Endpoint) -> Option<&'static str> { + let protocol = normalized_protocol(&endpoint.protocol); + if protocol.is_empty() { + None + } else if protocol.eq_ignore_ascii_case("websocket") { + Some(LAYER_WEBSOCKET) + } else { + Some(LAYER_REST) + } +} + fn endpoint_label(endpoint: &Endpoint) -> String { if endpoint.host.is_empty() { "".to_owned() @@ -824,7 +1054,9 @@ fn endpoint_label(endpoint: &Endpoint) -> String { #[cfg(test)] mod tests { use super::*; + use crate::credentials::{Credential, CredentialSet}; use crate::policy::parse_policy_str; + use std::collections::HashMap; fn policy(endpoint: &str, binaries: &str) -> PolicyModel { parse_policy_str(&format!( @@ -842,6 +1074,17 @@ network_policies: .expect("parse policy") } + fn policy_doc(network_policies: &str) -> PolicyModel { + parse_policy_str(&format!( + r" +version: 1 +network_policies: +{network_policies} +" + )) + .expect("parse policy") + } + fn one_rest_endpoint(extra: &str) -> String { format!( r" - host: api.github.com @@ -856,6 +1099,19 @@ network_policies: " - path: /usr/bin/gh" } + fn github_credentials() -> CredentialSet { + CredentialSet { + credentials: vec![Credential { + name: "github".to_owned(), + cred_type: "github-pat".to_owned(), + scopes: vec!["repo".to_owned()], + injected_via: "env".to_owned(), + target_hosts: vec!["api.github.com".to_owned()], + }], + api_registries: HashMap::new(), + } + } + #[test] fn exact_rest_rule_is_within_maximum() { let maximum = policy( @@ -1055,14 +1311,17 @@ network_policies: gh_binary(), ); - assert!(matches!( - check_within_maximum(&maximum, &candidate), - MaximumPolicyCheck::Unsupported { .. } - )); + let MaximumPolicyCheck::ExceedsMax { counterexample } = + check_within_maximum(&maximum, &candidate) + else { + panic!("expected L4 candidate to exceed REST maximum"); + }; + assert_eq!(counterexample.protocol, LAYER_L4); + assert_eq!(counterexample.host, "api.github.com"); } #[test] - fn l4_maximum_is_unsupported_until_modeled() { + fn l4_maximum_covers_rest_candidate_within_modeled_rest_domain() { let maximum = policy( r" - host: api.github.com port: 443", @@ -1073,10 +1332,29 @@ network_policies: gh_binary(), ); - assert!(matches!( + assert_eq!( check_within_maximum(&maximum, &candidate), - MaximumPolicyCheck::Unsupported { .. } - )); + MaximumPolicyCheck::WithinMax + ); + } + + #[test] + fn exact_l4_rule_is_within_l4_maximum() { + let maximum = policy( + r" - host: api.github.com + port: 443", + gh_binary(), + ); + let candidate = policy( + r" - host: api.github.com + port: 443", + gh_binary(), + ); + + assert_eq!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::WithinMax + ); } #[test] @@ -1088,11 +1366,55 @@ network_policies: gh_binary(), ); - let MaximumPolicyCheck::Unsupported { reason } = check_within_maximum(&maximum, &candidate) + let MaximumPolicyCheck::ExceedsMax { counterexample } = + check_within_maximum(&maximum, &candidate) else { - panic!("expected L4 candidate to fail closed"); + panic!("expected L4 candidate to exceed REST maximum"); }; - assert!(reason.contains("L4-only endpoint")); + assert_eq!(counterexample.protocol, LAYER_L4); + assert_eq!(counterexample.method, ""); + assert_eq!(counterexample.path, ""); + } + + #[test] + fn l4_host_wildcard_broadening_exceeds_maximum() { + let maximum = policy( + r" - host: api.github.com + port: 443", + gh_binary(), + ); + let candidate = policy( + r#" - host: "*.github.com" + port: 443"#, + gh_binary(), + ); + + assert!(matches!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::ExceedsMax { .. } + )); + } + + #[test] + fn l4_port_broadening_exceeds_maximum() { + let maximum = policy( + r" - host: api.github.com + port: 443", + gh_binary(), + ); + let candidate = policy( + r" - host: api.github.com + ports: [443, 8443]", + gh_binary(), + ); + + let MaximumPolicyCheck::ExceedsMax { counterexample } = + check_within_maximum(&maximum, &candidate) + else { + panic!("expected L4 port broadening"); + }; + assert_eq!(counterexample.protocol, LAYER_L4); + assert_eq!(counterexample.port, 8443); } #[test] @@ -1236,19 +1558,63 @@ network_policies: check_within_maximum(&enforced_maximum, &tls_skip_candidate), MaximumPolicyCheck::Unsupported { .. } )); + } - let websocket_candidate = policy( - r" - host: api.github.com + #[test] + fn websocket_endpoint_with_text_rules_is_modeled() { + let maximum = policy( + r#" - host: wss-primary.slack.com + port: 443 + protocol: websocket + enforcement: enforce + rules: + - allow: { method: GET, path: "/**" } + - allow: { method: WEBSOCKET_TEXT, path: "/**" }"#, + r#" - path: "/**""#, + ); + let candidate = policy( + r#" - host: wss-primary.slack.com + port: 443 + protocol: websocket + enforcement: enforce + rules: + - allow: { method: WEBSOCKET_TEXT, path: "/rooms/alerts" }"#, + " - path: /usr/bin/node", + ); + + assert_eq!( + check_within_maximum(&maximum, &candidate), + MaximumPolicyCheck::WithinMax + ); + } + + #[test] + fn websocket_read_only_does_not_cover_text_send() { + let maximum = policy( + r" - host: wss-primary.slack.com port: 443 protocol: websocket enforcement: enforce access: read-only", - gh_binary(), + " - path: /usr/bin/node", ); - assert!(matches!( - check_within_maximum(&enforced_maximum, &websocket_candidate), - MaximumPolicyCheck::Unsupported { .. } - )); + let candidate = policy( + r#" - host: wss-primary.slack.com + port: 443 + protocol: websocket + enforcement: enforce + rules: + - allow: { method: WEBSOCKET_TEXT, path: "/rooms/alerts" }"#, + " - path: /usr/bin/node", + ); + + let MaximumPolicyCheck::ExceedsMax { counterexample } = + check_within_maximum(&maximum, &candidate) + else { + panic!("expected text send to exceed read-only websocket maximum"); + }; + assert_eq!(counterexample.protocol, LAYER_WEBSOCKET); + assert_eq!(counterexample.method, "WEBSOCKET_TEXT"); } #[test] @@ -1268,6 +1634,34 @@ network_policies: check_within_maximum(&maximum, &candidate), MaximumPolicyCheck::Unsupported { .. } )); + + let rewrite_candidate = policy( + r" - host: api.github.com + port: 443 + protocol: rest + enforcement: enforce + access: read-only + request_body_credential_rewrite: true", + gh_binary(), + ); + assert!(matches!( + check_within_maximum(&maximum, &rewrite_candidate), + MaximumPolicyCheck::Unsupported { .. } + )); + + let websocket_rewrite_candidate = policy( + r" - host: wss-primary.slack.com + port: 443 + protocol: websocket + enforcement: enforce + access: read-write + websocket_credential_rewrite: true", + " - path: /usr/bin/node", + ); + assert!(matches!( + check_within_maximum(&websocket_rewrite_candidate, &websocket_rewrite_candidate), + MaximumPolicyCheck::Unsupported { .. } + )); } #[test] @@ -1493,7 +1887,31 @@ network_policies: } #[test] - fn narrowness_l4_candidate_is_unsupported_until_modeled() { + fn narrowness_exact_l4_candidate_fits_one_grant_budget_without_l7_overlap() { + let current = policy(&one_rest_endpoint(" access: full"), gh_binary()); + let candidate = policy( + r" - host: files.pythonhosted.org + port: 443", + gh_binary(), + ); + + let NarrownessCheck::WithinBudget { summary } = + check_narrowness(¤t, &candidate, &NarrownessBudget::one_exact_grant()) + else { + panic!("expected exact L4 delta to fit one-grant budget"); + }; + assert_eq!(summary.total_score, 1); + assert_eq!(summary.delta_grants.len(), 1); + assert_eq!(summary.delta_grants[0].protocol, LAYER_L4); + assert_eq!( + summary.delta_grants[0].reasons, + vec![ScopeIncreaseReason::NewGrant] + ); + assert_eq!(summary.delta_grants[0].counterexample.protocol, LAYER_L4); + } + + #[test] + fn narrowness_l7_to_l4_broadening_is_high_cost() { let current = policy(&one_rest_endpoint(" access: full"), gh_binary()); let candidate = policy( r" - host: api.github.com @@ -1501,11 +1919,293 @@ network_policies: gh_binary(), ); - let NarrownessCheck::Unsupported { reason } = + let NarrownessCheck::ExceedsBudget { summary } = check_narrowness(¤t, &candidate, &NarrownessBudget::one_exact_grant()) else { - panic!("expected L4 candidate to fail closed"); + panic!("expected L7-to-L4 broadening to exceed one-grant budget"); }; - assert!(reason.contains("L4-only endpoint")); + assert_eq!(summary.total_score, 9); + assert_eq!(summary.delta_grants.len(), 1); + assert_eq!(summary.delta_grants[0].protocol, LAYER_L4); + assert_eq!( + summary.delta_grants[0].reasons, + vec![ + ScopeIncreaseReason::NewGrant, + ScopeIncreaseReason::L7ToL4Broadening + ] + ); + + let broader_budget = NarrownessBudget { + max_delta_grants: 1, + max_total_score: 9, + allow_recursive_globs: false, + }; + assert!(matches!( + check_narrowness(¤t, &candidate, &broader_budget), + NarrownessCheck::WithinBudget { .. } + )); + } + + #[test] + fn narrowness_l4_current_covers_rest_candidate_within_modeled_rest_domain() { + let current = policy( + r" - host: api.github.com + port: 443", + gh_binary(), + ); + let candidate = policy(&one_rest_endpoint(" access: full"), gh_binary()); + + assert_eq!( + check_narrowness(¤t, &candidate, &NarrownessBudget::one_exact_grant()), + NarrownessCheck::NoIncrease + ); + } + + #[test] + fn narrowness_websocket_delta_preserves_modeled_layer() { + let current = policy( + r#" - host: wss-primary.slack.com + port: 443 + protocol: websocket + enforcement: enforce + rules: + - allow: { method: WEBSOCKET_TEXT, path: "/rooms/alerts" }"#, + " - path: /usr/bin/node", + ); + let candidate = policy( + r#" - host: wss-primary.slack.com + port: 443 + protocol: websocket + enforcement: enforce + rules: + - allow: { method: WEBSOCKET_TEXT, path: "/rooms/alerts" } + - allow: { method: WEBSOCKET_TEXT, path: "/rooms/incidents" }"#, + " - path: /usr/bin/node", + ); + + let NarrownessCheck::WithinBudget { summary } = + check_narrowness(¤t, &candidate, &NarrownessBudget::one_exact_grant()) + else { + panic!("expected one exact websocket delta to fit budget"); + }; + assert_eq!(summary.total_score, 1); + assert_eq!(summary.delta_grants.len(), 1); + assert_eq!(summary.delta_grants[0].protocol, LAYER_WEBSOCKET); + assert_eq!( + summary.delta_grants[0].counterexample.protocol, + LAYER_WEBSOCKET + ); + assert_eq!(summary.delta_grants[0].method, "WEBSOCKET_TEXT"); + } + + #[test] + fn mixed_l4_and_rest_fixture_is_modelable() { + let policy = parse_policy_str(include_str!("../testdata/policy.yaml")) + .expect("parse prover fixture"); + + assert_eq!( + check_within_maximum(&policy, &policy), + MaximumPolicyCheck::WithinMax + ); + } + + #[test] + fn credentialed_rest_is_not_uninspected_l4() { + let policy = policy( + &one_rest_endpoint(" access: read-write"), + gh_binary(), + ); + + assert_eq!( + check_uninspected_credentialed_l4(&policy, &github_credentials()), + CredentialedL4Check::NoUninspectedCredentialedL4 + ); + } + + #[test] + fn exact_l4_to_credential_target_is_reported() { + let policy = policy( + r" - host: api.github.com + port: 443", + gh_binary(), + ); + + let CredentialedL4Check::HasUninspectedCredentialedL4 { counterexample } = + check_uninspected_credentialed_l4(&policy, &github_credentials()) + else { + panic!("expected uninspected credentialed L4 finding"); + }; + assert_eq!(counterexample.protocol, LAYER_L4); + assert_eq!(counterexample.host, "api.github.com"); + } + + #[test] + fn broad_l4_to_credential_target_is_reported_with_symbolic_host() { + let policy = policy( + r#" - host: "**" + port: 443"#, + gh_binary(), + ); + + let CredentialedL4Check::HasUninspectedCredentialedL4 { counterexample } = + check_uninspected_credentialed_l4(&policy, &github_credentials()) + else { + panic!("expected broad L4 to overlap credential target"); + }; + assert_eq!(counterexample.protocol, LAYER_L4); + assert_eq!(counterexample.host, "api.github.com"); + } + + #[test] + fn credential_target_matching_normalizes_trailing_dot() { + let policy = policy( + r" - host: api.github.com + port: 443", + gh_binary(), + ); + let credentials = CredentialSet { + credentials: vec![Credential { + name: "github".to_owned(), + cred_type: "github-pat".to_owned(), + scopes: vec!["repo".to_owned()], + injected_via: "env".to_owned(), + target_hosts: vec![" API.GITHUB.COM. ".to_owned()], + }], + api_registries: HashMap::new(), + }; + + let CredentialedL4Check::HasUninspectedCredentialedL4 { counterexample } = + check_uninspected_credentialed_l4(&policy, &credentials) + else { + panic!("expected normalized credential target to match L4 policy host"); + }; + assert_eq!(counterexample.host, "api.github.com"); + } + + #[test] + fn provider_shaped_cursor_allows_known_download_but_rejects_new_url() { + let maximum = policy_doc( + r#" _provider_cursor: + name: _provider_cursor + endpoints: + - host: cursor.blob.core.windows.net + port: 443 + - host: api2.cursor.sh + port: 443 + - host: repo.cursor.sh + port: 443 + - host: download.cursor.sh + port: 443 + - host: cursor.download.prss.microsoft.com + port: 443 + binaries: + - path: /usr/bin/curl + - path: /usr/bin/wget + - path: "/sandbox/.cursor-server/**""#, + ); + let known_candidate = policy_doc( + r" cursor_bootstrap: + name: cursor_bootstrap + endpoints: + - host: repo.cursor.sh + port: 443 + binaries: + - path: /usr/bin/curl", + ); + let new_url_candidate = policy_doc( + r" cursor_bootstrap: + name: cursor_bootstrap + endpoints: + - host: updates.example.com + port: 443 + binaries: + - path: /usr/bin/curl", + ); + + assert_eq!( + check_within_maximum(&maximum, &known_candidate), + MaximumPolicyCheck::WithinMax + ); + let MaximumPolicyCheck::ExceedsMax { counterexample } = + check_within_maximum(&maximum, &new_url_candidate) + else { + panic!("expected new URL to exceed Cursor provider maximum"); + }; + assert_eq!(counterexample.protocol, LAYER_L4); + assert_eq!(counterexample.host, "updates.example.com"); + } + + #[test] + fn provider_shaped_copilot_mixed_rest_and_l4_are_modelable() { + let maximum = policy_doc( + r#" _provider_copilot: + name: _provider_copilot + endpoints: + - host: api.githubcopilot.com + port: 443 + protocol: rest + access: read-write + enforcement: enforce + - host: api.individual.githubcopilot.com + port: 443 + protocol: rest + access: read-write + enforcement: enforce + - host: api.business.githubcopilot.com + port: 443 + protocol: rest + access: read-write + enforcement: enforce + - host: api.enterprise.githubcopilot.com + port: 443 + protocol: rest + access: read-write + enforcement: enforce + - host: copilot-proxy.githubusercontent.com + port: 443 + protocol: rest + access: read-write + enforcement: enforce + - host: telemetry.enterprise.githubcopilot.com + port: 443 + - host: default.exp-tas.com + port: 443 + binaries: + - path: /usr/bin/copilot + - path: "/usr/lib/node_modules/@github/copilot/node_modules/@github/**/copilot""#, + ); + let rest_candidate = policy_doc( + r" copilot_api: + name: copilot_api + endpoints: + - host: api.githubcopilot.com + port: 443 + protocol: rest + enforcement: enforce + rules: + - allow: + method: POST + path: /chat/completions + binaries: + - path: /usr/bin/copilot", + ); + let l4_candidate = policy_doc( + r" copilot_telemetry: + name: copilot_telemetry + endpoints: + - host: telemetry.enterprise.githubcopilot.com + port: 443 + binaries: + - path: /usr/bin/copilot", + ); + + assert_eq!( + check_within_maximum(&maximum, &rest_candidate), + MaximumPolicyCheck::WithinMax + ); + assert_eq!( + check_within_maximum(&maximum, &l4_candidate), + MaximumPolicyCheck::WithinMax + ); } }