diff --git a/architecture/security-policy.md b/architecture/security-policy.md index 667694a1fc..5f098262f6 100644 --- a/architecture/security-policy.md +++ b/architecture/security-policy.md @@ -383,15 +383,20 @@ final enforcement boundary. The standalone `openshell-prover check` command compares a fully composed local candidate policy with an operator-supplied local boundary. It establishes -`Allowed(candidate) ⊆ Allowed(boundary)` for the model scope reported in its +`Allowed(candidate) ⊆ Allowed(boundary)` for the policy domains reported in its result. It does not fetch gateway state, compose provider rules, apply policy, or decide whether an in-boundary change is eligible for automatic approval. -The initial model covers filesystem paths, L4 network authority, and enforced -REST method and path authority. It returns explicit unsupported or inconclusive +The containment model covers filesystem paths, supported process identities, +Landlock compatibility requirements, L4 destinations including IP ranges, and +enforced REST method and path authority. Identity comparisons assume consistent +user and group resolution. Compatibility checks compare requested enforcement +requirements, not the actual kernel state of a running sandbox. +It returns explicit unsupported or inconclusive results when a sound decision depends on authority or runtime context outside -the model. The result records the model version and covered domains so callers -can bind a successful check to those semantics. +the model. The result records the covered domains so callers can require the +authority relevant to their decision. The JSON `schema_version` versions the +result contract, while `prover_version` identifies the producing implementation. Before semantic validation, the checker observes cancellation and applies aggregate limits across both inputs. Oversized checks therefore return @@ -403,8 +408,8 @@ The Rust containment API has an explicit extensibility contract: options and modeled-domain evidence permit additive growth, while the four `CheckResult` states remain exhaustive and authorization accepts only `Within`. This Rust source-compatibility boundary is separate from the CLI JSON schema and the -reported containment model version. See the `openshell-prover` crate README for -the supported construction and matching patterns. +reported modeled domains. See the `openshell-prover` crate README for the +supported construction and matching patterns. This containment operation is separate from the proposal-risk queries below. See the [standalone policy prover documentation](../docs/reference/policy-prover.mdx) diff --git a/crates/openshell-prover-cli/README.md b/crates/openshell-prover-cli/README.md index 9b9488b8c4..92050bc2b5 100644 --- a/crates/openshell-prover-cli/README.md +++ b/crates/openshell-prover-cli/README.md @@ -32,3 +32,9 @@ cargo test -p openshell-prover-cli ``` See the [policy prover reference](../../docs/reference/policy-prover.mdx) for installed usage and interpretation guidance. + +JSON output uses a numeric `schema_version` for the result contract and a +`prover_version` for the implementation that produced it. Consumers must inspect +`coverage.domains` for the machine-readable modeled-domain declaration. A +passing check compares configuration under the documented assumptions; it does +not attest that a running sandbox installed its restrictions. diff --git a/crates/openshell-prover-cli/src/main.rs b/crates/openshell-prover-cli/src/main.rs index 4dd621eade..69166c4e37 100644 --- a/crates/openshell-prover-cli/src/main.rs +++ b/crates/openshell-prover-cli/src/main.rs @@ -16,7 +16,7 @@ use std::time::Duration; use clap::{CommandFactory, Parser, Subcommand, ValueEnum}; use openshell_prover::containment::{ - CheckOptions, CheckResult, CheckScope, ContainmentPolicy, Counterexample, parse_policy_str, + CheckCoverage, CheckOptions, CheckResult, ContainmentPolicy, Counterexample, parse_policy_str, }; use serde::Serialize; @@ -62,7 +62,7 @@ struct Envelope<'a> { schema_version: u32, prover_version: &'static str, check: &'static str, - scope: Option>, + coverage: Option>, result: &'static str, exit_code: u8, inputs: InputsJson, @@ -72,9 +72,7 @@ struct Envelope<'a> { } #[derive(Debug, Serialize)] -struct ScopeJson<'a> { - model_version: &'a str, - policy_version: u32, +struct CoverageJson<'a> { domains: Vec<&'a str>, } @@ -87,6 +85,15 @@ struct InputsJson { #[derive(Debug, Serialize)] #[serde(tag = "domain", rename_all = "snake_case")] enum CounterexampleJson<'a> { + Process { + field: &'a str, + boundary: &'a str, + candidate: &'a str, + }, + Landlock { + boundary: &'a str, + candidate: &'a str, + }, Filesystem { access: &'a str, path: &'a str, @@ -96,6 +103,8 @@ enum CounterexampleJson<'a> { ancestor_binary: Option<&'a str>, binary_identity_required: bool, host: &'a str, + destination_ip: String, + trusted_gateway: bool, port: u16, protocol: &'a str, method: Option<&'a str>, @@ -284,7 +293,7 @@ fn render_input_error( schema_version: 1, prover_version: env!("CARGO_PKG_VERSION"), check: "boundary", - scope: None, + coverage: None, result: "error", exit_code: 2, inputs, @@ -308,10 +317,12 @@ fn render_cancelled(output: OutputFormat, inputs: InputsJson) -> Result Result, String> { - let (scope, result_name, exit_code, counterexample, reason_code, reason) = match result { - CheckResult::Within(evidence) => (evidence.scope(), "within_boundary", 0, None, None, None), + let (coverage, result_name, exit_code, counterexample, reason_code, reason) = match result { + CheckResult::Within(evidence) => { + (evidence.coverage(), "within_boundary", 0, None, None, None) + } CheckResult::Exceeds(evidence) => ( - evidence.scope(), + evidence.coverage(), "exceeds_boundary", 1, Some(counterexample_json(evidence.counterexample())?), @@ -319,7 +330,7 @@ fn result_envelope(result: &CheckResult, inputs: InputsJson) -> Result ( - evidence.scope(), + evidence.coverage(), "unsupported", 3, None, @@ -334,7 +345,7 @@ fn result_envelope(result: &CheckResult, inputs: InputsJson) -> Result Result Result ScopeJson<'_> { - ScopeJson { - model_version: scope.model_version, - policy_version: scope.policy_version, - domains: scope.domains.iter().map(|domain| domain.as_str()).collect(), +fn coverage_json(coverage: &CheckCoverage) -> CoverageJson<'_> { + CoverageJson { + domains: coverage + .domains + .iter() + .map(|domain| domain.as_str()) + .collect(), } } fn counterexample_json(counterexample: &Counterexample) -> Result, String> { let converted = match counterexample { + Counterexample::Process { + field, + boundary, + candidate, + .. + } => CounterexampleJson::Process { + field, + boundary, + candidate, + }, + Counterexample::Landlock { + boundary, + candidate, + .. + } => CounterexampleJson::Landlock { + boundary, + candidate, + }, Counterexample::Filesystem { access, path, .. } => CounterexampleJson::Filesystem { access: access.as_str(), path, @@ -376,6 +407,8 @@ fn counterexample_json(counterexample: &Counterexample) -> Result Result) -> Result<(), String> { fn render_text(mut writer: impl Write, envelope: &Envelope<'_>) -> Result<(), String> { writeln!(writer, "result: {}", envelope.result) .map_err(|error| format!("failed to write output: {error}"))?; - if let Some(scope) = &envelope.scope { - writeln!( - writer, - "scope: model={} policy={} domains={}", - escape_terminal(scope.model_version), - scope.policy_version, - scope.domains.join(",") - ) - .map_err(|error| format!("failed to write output: {error}"))?; + if let Some(coverage) = &envelope.coverage { + writeln!(writer, "coverage: domains={}", coverage.domains.join(",")) + .map_err(|error| format!("failed to write output: {error}"))?; } if let Some(counterexample) = &envelope.counterexample { match counterexample { + CounterexampleJson::Process { field, boundary, candidate } => writeln!(writer, "counterexample: process {} boundary={} candidate={}", escape_terminal(field), escape_terminal(boundary), escape_terminal(candidate)), + CounterexampleJson::Landlock { boundary, candidate } => writeln!(writer, "counterexample: landlock boundary={} candidate={}", escape_terminal(boundary), escape_terminal(candidate)), CounterexampleJson::Filesystem { access, path } => writeln!( writer, "counterexample: filesystem {access} {}", @@ -434,18 +465,22 @@ fn render_text(mut writer: impl Write, envelope: &Envelope<'_>) -> Result<(), St ancestor_binary, binary_identity_required, host, + destination_ip, + trusted_gateway, port, protocol, method, path, } => writeln!( writer, - "counterexample: network binary={} ancestor_binary={} binary_identity_required={} host={}:{} protocol={} method={} path={}", + "counterexample: network binary={} ancestor_binary={} binary_identity_required={} host={}:{} destination_ip={} trusted_gateway={} protocol={} method={} path={}", binary.map_or("-".to_owned(), escape_terminal), ancestor_binary.map_or("-".to_owned(), escape_terminal), binary_identity_required, escape_terminal(host), port, + destination_ip, + trusted_gateway, escape_terminal(protocol), method.map_or("-".to_owned(), escape_terminal), path.map_or("-".to_owned(), escape_terminal), @@ -557,7 +592,7 @@ mod tests { schema_version: 1, prover_version: env!("CARGO_PKG_VERSION"), check: "boundary", - scope: None, + coverage: None, result: "within_boundary", exit_code: 0, inputs: InputsJson { diff --git a/crates/openshell-prover-cli/tests/cli.rs b/crates/openshell-prover-cli/tests/cli.rs index 5c8fa44f99..414164c85d 100644 --- a/crates/openshell-prover-cli/tests/cli.rs +++ b/crates/openshell-prover-cli/tests/cli.rs @@ -78,16 +78,40 @@ fn contained_policy_returns_stable_json_and_zero() { assert_eq!(value["result"], "within_boundary"); assert_eq!(value["exit_code"], 0); assert_eq!( - value["scope"], + value["coverage"], serde_json::json!({ - "model_version": "boundary-v1", - "policy_version": 1, - "domains": ["filesystem", "network_l4", "network_rest"] + "domains": ["filesystem", "network_l4", "network_rest", "process", "landlock"] }) ); + assert!(value.get("scope").is_none()); assert!(value["counterexample"].is_null()); } +#[test] +fn contained_policy_returns_stable_text_coverage_and_zero() { + let output = run(&[ + "check", + fixture("candidate-contained.yaml") + .to_str() + .expect("UTF-8 fixture path"), + "--boundary", + fixture("boundary.yaml") + .to_str() + .expect("UTF-8 fixture path"), + ]); + assert_eq!( + output.status.code(), + Some(0), + "stderr: {}", + String::from_utf8_lossy(&output.stderr) + ); + assert!(output.stderr.is_empty()); + assert_eq!( + String::from_utf8(output.stdout).expect("UTF-8 text output"), + "result: within_boundary\ncoverage: domains=filesystem,network_l4,network_rest,process,landlock\n" + ); +} + #[test] fn exceeding_policy_returns_counterexample_and_one() { let output = check_json("candidate-exceeds.yaml", "boundary-no-write.yaml"); @@ -103,6 +127,58 @@ fn exceeding_policy_returns_counterexample_and_one() { assert_eq!(value["counterexample"]["domain"], "filesystem"); } +#[test] +fn counterexamples_have_stable_json_shapes() { + for (candidate, boundary, expected) in [ + ( + "candidate-process-root.yaml", + "boundary-execution.yaml", + serde_json::json!({ + "domain": "process", + "field": "run_as_user", + "boundary": "sandbox", + "candidate": "root" + }), + ), + ( + "candidate-landlock-best-effort.yaml", + "boundary-execution.yaml", + serde_json::json!({ + "domain": "landlock", + "boundary": "hard_requirement", + "candidate": "best_effort" + }), + ), + ( + "candidate-ipv6.yaml", + "boundary-empty.yaml", + serde_json::json!({ + "domain": "network", + "binary": null, + "ancestor_binary": null, + "binary_identity_required": false, + "host": "api.example.com", + "destination_ip": "2001:db8::", + "trusted_gateway": false, + "port": 443, + "protocol": "l4", + "method": null, + "path": null + }), + ), + ] { + let output = check_json(candidate, boundary); + assert_eq!( + output.status.code(), + Some(1), + "candidate={candidate}, stderr={}", + String::from_utf8_lossy(&output.stderr) + ); + let value: Value = serde_json::from_slice(&output.stdout).expect("single JSON object"); + assert_eq!(value["counterexample"], expected, "candidate={candidate}"); + } +} + #[test] fn unsupported_policy_returns_reason_and_three() { let output = check_json("unsupported.yaml", "boundary.yaml"); @@ -536,6 +612,9 @@ fn sigint_interrupts_the_check_with_exit_130() { policy( (0..300) .map(|index| format!("/route{index}/**/tail*")) + // Cover the bounded concrete-witness sample so this fixture + // still exercises interruption of the unrestricted solver. + .chain(std::iter::once("/routea/**/tail*".to_owned())) .collect(), ) .to_string(), diff --git a/crates/openshell-prover-cli/tests/fixtures/boundary-execution.yaml b/crates/openshell-prover-cli/tests/fixtures/boundary-execution.yaml new file mode 100644 index 0000000000..95656ad635 --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/boundary-execution.yaml @@ -0,0 +1,9 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 +process: + run_as_user: sandbox + run_as_group: sandbox +landlock: + compatibility: hard_requirement diff --git a/crates/openshell-prover-cli/tests/fixtures/candidate-ipv6.yaml b/crates/openshell-prover-cli/tests/fixtures/candidate-ipv6.yaml new file mode 100644 index 0000000000..ce116525f3 --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/candidate-ipv6.yaml @@ -0,0 +1,11 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 +network_policies: + api: + endpoints: + - host: api.example.com + port: 443 + allowed_ips: + - 2001:db8::/32 diff --git a/crates/openshell-prover-cli/tests/fixtures/candidate-landlock-best-effort.yaml b/crates/openshell-prover-cli/tests/fixtures/candidate-landlock-best-effort.yaml new file mode 100644 index 0000000000..0e0cc4195f --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/candidate-landlock-best-effort.yaml @@ -0,0 +1,9 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 +process: + run_as_user: sandbox + run_as_group: sandbox +landlock: + compatibility: best_effort diff --git a/crates/openshell-prover-cli/tests/fixtures/candidate-process-root.yaml b/crates/openshell-prover-cli/tests/fixtures/candidate-process-root.yaml new file mode 100644 index 0000000000..96b206546b --- /dev/null +++ b/crates/openshell-prover-cli/tests/fixtures/candidate-process-root.yaml @@ -0,0 +1,9 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +# SPDX-License-Identifier: Apache-2.0 + +version: 1 +process: + run_as_user: root + run_as_group: sandbox +landlock: + compatibility: hard_requirement diff --git a/crates/openshell-prover/README.md b/crates/openshell-prover/README.md index 130ffe5971..0026a04172 100644 --- a/crates/openshell-prover/README.md +++ b/crates/openshell-prover/README.md @@ -54,7 +54,7 @@ let authorized = matches!(result, CheckResult::Within(_)); ``` `ReasonCode`, `CheckDomain`, `Protocol`, and `Counterexample` are open to new -variants. `CheckOptions`, `CheckScope`, `WithinEvidence`, and existing +variants. `CheckOptions`, `CheckCoverage`, `WithinEvidence`, and existing counterexample variants are open to new fields. Match these types with `..` and wildcard arms, use their accessors and `as_str()` identifiers, and treat unknown values as a fail-closed result. Existing identifier strings are stable. @@ -63,7 +63,10 @@ unknown values as a fail-closed result. Existing identifier strings are stable. `Unsupported`, and `Inconclusive`. `FilesystemAccess` is likewise closed to `Read` and `Write`. Adding a result state or filesystem access mode is a breaking API change. Rust source compatibility is separate from the CLI JSON -schema and containment model versions; this contract changes neither. +schema contract. The CLI's numeric `schema_version` versions that JSON contract, +while `prover_version` identifies the implementation that produced a result. +The result's `coverage.domains` list is the machine-readable declaration of +modeled authority. Used by the gateway to gate auto-approval of agent-authored policy proposals: any finding blocks auto-approval, an empty delta lets the diff --git a/crates/openshell-prover/src/containment.rs b/crates/openshell-prover/src/containment.rs index 86cc9dcd59..86397f754c 100644 --- a/crates/openshell-prover/src/containment.rs +++ b/crates/openshell-prover/src/containment.rs @@ -12,7 +12,7 @@ //! remains exhaustive: its four outcomes are the stable, closed result-state //! contract, and authorization should accept only [`CheckResult::Within`]. -use std::collections::{BTreeMap, BTreeSet}; +use std::collections::BTreeMap; use std::fmt; use std::net::IpAddr; use std::str::FromStr; @@ -27,6 +27,9 @@ use openshell_policy_schema::{ use z3::ast::{Ast, Bool, Int, Regexp, String as Z3String}; use z3::{Context, Params, SatResult, Solver}; +mod execution; +mod ip; + const LAYER_L4: &str = "l4"; const LAYER_REST: &str = "rest"; const WORKDIR_SYMBOL: &str = ""; @@ -35,6 +38,7 @@ const MAX_ENDPOINTS: usize = 4_096; const MAX_BINARIES: usize = 4_096; const MAX_PORT_ENTRIES: usize = 65_536; const MAX_L7_RULES: usize = 16_384; +const MAX_IP_RANGES: usize = 4_096; const MAX_PATTERN_BYTES: usize = 4 * 1024; const MAX_TOTAL_PATTERN_BYTES: usize = 1024 * 1024; @@ -175,13 +179,15 @@ impl ReasonCode { } } -/// Authority domains modeled by this engine version. +/// Authority domains modeled by this check. #[derive(Debug, Clone, Copy, PartialEq, Eq)] #[non_exhaustive] pub enum CheckDomain { Filesystem, NetworkL4, NetworkRest, + Process, + Landlock, } impl CheckDomain { @@ -191,16 +197,17 @@ impl CheckDomain { Self::Filesystem => "filesystem", Self::NetworkL4 => "network_l4", Self::NetworkRest => "network_rest", + Self::Process => "process", + Self::Landlock => "landlock", } } } -/// Scope attached to every completed or recoverably incomplete check. +/// Modeled authority coverage attached to every completed or recoverably +/// incomplete check. #[derive(Debug, Clone, PartialEq, Eq)] #[non_exhaustive] -pub struct CheckScope { - pub model_version: &'static str, - pub policy_version: u32, +pub struct CheckCoverage { pub domains: &'static [CheckDomain], } @@ -208,14 +215,12 @@ static DOMAINS: &[CheckDomain] = &[ CheckDomain::Filesystem, CheckDomain::NetworkL4, CheckDomain::NetworkRest, + CheckDomain::Process, + CheckDomain::Landlock, ]; -fn check_scope() -> &'static CheckScope { - static SCOPE: CheckScope = CheckScope { - model_version: "boundary-v1", - policy_version: 1, - domains: DOMAINS, - }; - &SCOPE +fn check_coverage() -> &'static CheckCoverage { + static COVERAGE: CheckCoverage = CheckCoverage { domains: DOMAINS }; + &COVERAGE } #[derive(Debug, Clone, Copy, PartialEq, Eq)] @@ -255,6 +260,14 @@ impl Protocol { #[derive(Debug, Clone, PartialEq, Eq)] #[non_exhaustive] pub enum Counterexample { + #[non_exhaustive] + Process { + field: &'static str, + boundary: String, + candidate: String, + }, + #[non_exhaustive] + Landlock { boundary: String, candidate: String }, #[non_exhaustive] Filesystem { access: FilesystemAccess, @@ -266,6 +279,8 @@ pub enum Counterexample { ancestor_binary: Option, binary_identity_required: bool, host: String, + destination_ip: IpAddr, + trusted_gateway: bool, port: u16, protocol: Protocol, method: Option, @@ -279,8 +294,8 @@ pub struct WithinEvidence; impl WithinEvidence { #[must_use] - pub fn scope(&self) -> &'static CheckScope { - check_scope() + pub fn coverage(&self) -> &'static CheckCoverage { + check_coverage() } } @@ -289,8 +304,8 @@ pub struct ExceedsEvidence(Counterexample); impl ExceedsEvidence { #[must_use] - pub fn scope(&self) -> &'static CheckScope { - check_scope() + pub fn coverage(&self) -> &'static CheckCoverage { + check_coverage() } #[must_use] @@ -307,8 +322,8 @@ pub struct ReasonEvidence { impl ReasonEvidence { #[must_use] - pub fn scope(&self) -> &'static CheckScope { - check_scope() + pub fn coverage(&self) -> &'static CheckCoverage { + check_coverage() } #[must_use] @@ -347,6 +362,8 @@ struct SymbolicAction { layer: Z3String, method: Z3String, path: Z3String, + ip: ip::SymbolicIp, + trusted_gateway: Bool, } enum NetworkSolve { @@ -393,6 +410,10 @@ fn check_within_boundary_inner( if let Some(reason) = unresolved_workdir_reason(boundary, candidate) { return unsupported(ReasonCode::UnresolvedWorkdir, reason); } + let execution_result = execution::check(boundary, candidate); + if let Some(result @ CheckResult::Exceeds(_)) = execution_result.as_ref() { + return result.clone(); + } if boundary == candidate { return CheckResult::Within(WithinEvidence); } @@ -402,6 +423,13 @@ fn check_within_boundary_inner( } let started = Instant::now(); for binary_identity_required in [false, true] { + if binary_identity_required && has_ambiguous_candidate_binary_path(boundary, candidate) { + return unsupported( + ReasonCode::UnresolvedBinaryPath, + "network containment depends on image-specific binary symlink resolution" + .to_owned(), + ); + } match solve_network_mode( boundary, candidate, @@ -416,13 +444,6 @@ fn check_within_boundary_inner( } NetworkSolve::Incomplete(result) => return result, } - if binary_identity_required && has_ambiguous_candidate_binary_path(boundary, candidate) { - return unsupported( - ReasonCode::UnresolvedBinaryPath, - "network containment depends on image-specific binary symlink resolution" - .to_owned(), - ); - } } if unresolved_exact_deny_symlink(boundary, candidate) { return unsupported( @@ -431,7 +452,9 @@ fn check_within_boundary_inner( .to_owned(), ); } - filesystem_result.unwrap_or(CheckResult::Within(WithinEvidence)) + execution_result + .or(filesystem_result) + .unwrap_or(CheckResult::Within(WithinEvidence)) } fn preflight_and_validate_policies( @@ -494,6 +517,9 @@ fn solve_network_mode( if network_is_structurally_contained(boundary, candidate, binary_identity_required) { return NetworkSolve::Within; } + if let Some(witness) = concrete_network_witness(boundary, candidate, binary_identity_required) { + return NetworkSolve::Exceeds(witness); + } let solver = Solver::new(); let action = symbolic_action(if binary_identity_required { "strict_boundary_policy_action" @@ -501,10 +527,13 @@ fn solve_network_mode( "relaxed_boundary_policy_action" }); assert_action_domain(&solver, &action, binary_identity_required); - solver.assert(Bool::and(&[ - policy_allows(candidate, &action, binary_identity_required), - !policy_allows(boundary, &action, binary_identity_required), - ])); + solver.assert( + Bool::and(&[ + policy_allows(candidate, &action, binary_identity_required), + !policy_allows(boundary, &action, binary_identity_required), + ]) + .simplify(), + ); let Some(remaining) = timeout.checked_sub(started.elapsed()) else { return NetworkSolve::Incomplete(solver_timeout_result()); @@ -556,6 +585,72 @@ fn solve_network_mode( } } +/// A few concrete requests make common counterexamples cheap and readable. +/// Each is replayed against the full predicate. Failure to find one never +/// establishes containment: the unrestricted symbolic query still follows. +fn concrete_network_witness( + boundary: &ContainmentPolicy, + candidate: &ContainmentPolicy, + binary_identity_required: bool, +) -> Option { + for (rule, endpoint) in candidate + .network_policies + .values() + .flat_map(|rule| rule.endpoints.iter().map(move |endpoint| (rule, endpoint))) + .take(8) + { + let host = endpoint + .host + .to_ascii_lowercase() + .replace("**", "a") + .replace('*', "a"); + let binary = binary_identity_required.then(|| { + rule.binaries.first().map_or_else( + || "/usr/bin/worker".to_owned(), + |binary| binary.path.replace("**", "a").replace('*', "a"), + ) + }); + let method = endpoint + .rules + .first() + .map_or("GET", |rule| rule.allow.method.as_str()) + .to_ascii_uppercase(); + let path = endpoint + .rules + .first() + .map_or(endpoint.path.as_str(), |rule| rule.allow.path.as_str()); + let path = if path.is_empty() { + "/".to_owned() + } else { + path.replace("**", "a").replace('*', "a") + }; + if !is_canonical_dns_host(&host) + || !is_canonical_rest_path(&path) + || !is_http_method(&method) + { + continue; + } + for destination_ip in ip::sample_addresses(endpoint) { + let witness = Counterexample::Network { + binary: binary.clone(), + ancestor_binary: binary.clone(), + binary_identity_required, + host: host.clone(), + destination_ip, + trusted_gateway: false, + port: endpoint.effective_ports()[0], + protocol: endpoint.protocol_kind(), + method: (endpoint.protocol_kind() == Protocol::Rest).then(|| method.clone()), + path: (endpoint.protocol_kind() == Protocol::Rest).then(|| path.clone()), + }; + if counterexample_satisfies_predicate(boundary, candidate, &witness) { + return Some(witness); + } + } + } + None +} + fn solver_timeout_result() -> CheckResult { CheckResult::Inconclusive(ReasonEvidence { code: ReasonCode::SolverTimeout, @@ -645,6 +740,7 @@ fn rest_endpoint_structurally_contains(boundary: &Endpoint, candidate: &Endpoint || candidate.protocol_kind() != Protocol::Rest || !boundary.host.eq_ignore_ascii_case(&candidate.host) || boundary.path != candidate.path + || boundary.allowed_ips != candidate.allowed_ips || !candidate .effective_ports() .iter() @@ -702,10 +798,13 @@ fn symbolic_action(name: &str) -> SymbolicAction { layer: Z3String::new_const(format!("{name}_layer")), method: Z3String::new_const(format!("{name}_method")), path: Z3String::new_const(format!("{name}_path")), + ip: ip::SymbolicIp::new(name), + trusted_gateway: Bool::new_const(format!("{name}_trusted_gateway")), } } fn assert_action_domain(solver: &Solver, action: &SymbolicAction, binary_identity_required: bool) { + action.ip.assert_domain(solver); if binary_identity_required { solver.assert(action.binary.regex_matches(&glob_regex("/**", "/"))); solver.assert(action.binary.length().le(4_096)); @@ -755,7 +854,11 @@ fn policy_allows( .values() .map(|rule| rule_denies(rule, action, binary_identity_required)), ); - Bool::and(&[allowed, !denied]) + Bool::and(&[ + allowed, + !denied, + ip::policy_allows(policy, action, binary_identity_required), + ]) } fn rule_allows( @@ -945,6 +1048,8 @@ fn counterexample_from_model( ancestor_binary, binary_identity_required, host, + destination_ip: action.ip.decode(model)?, + trusted_gateway: model.eval(&action.trusted_gateway, true)?.as_bool()?, port: u16::try_from(port).ok()?, protocol, method, @@ -979,6 +1084,8 @@ fn counterexample_satisfies_predicate( ancestor_binary, binary_identity_required, host, + destination_ip, + trusted_gateway, port, protocol, method, @@ -995,6 +1102,8 @@ fn counterexample_satisfies_predicate( layer: Z3String::from_str(protocol.as_str()).unwrap(), method: Z3String::from_str(method.as_deref().unwrap_or("GET")).unwrap(), path: Z3String::from_str(path.as_deref().unwrap_or("/")).unwrap(), + ip: ip::SymbolicIp::concrete(*destination_ip), + trusted_gateway: Bool::from_bool(*trusted_gateway), }; Bool::and(&[ policy_allows(candidate, &concrete, *binary_identity_required), @@ -1378,12 +1487,12 @@ fn validate_supported_policy( } fn validate_supported_common_policy(policy: &ContainmentPolicy) -> Result<(), UnsupportedFeature> { - if policy.landlock.is_some() - || policy.process.is_some() - || !policy.network_middlewares.is_empty() - { + if let Some(reason) = execution::unsupported_reason(policy) { + return Err(UnsupportedFeature::policy_shape(reason)); + } + if !policy.network_middlewares.is_empty() { return Err(UnsupportedFeature::policy_shape( - "uses process, Landlock, or network middleware controls", + "uses network middleware controls", )); } Ok(()) @@ -1487,8 +1596,7 @@ fn validate_supported_endpoint_extensions( context: &str, endpoint: &Endpoint, ) -> Result<(), UnsupportedFeature> { - if !endpoint.allowed_ips.is_empty() - || !matches!(endpoint.tls.as_str(), "" | "terminate" | "passthrough") + if !matches!(endpoint.tls.as_str(), "" | "terminate" | "passthrough") || endpoint.allow_encoded_slash || endpoint.websocket_credential_rewrite || endpoint.request_body_credential_rewrite @@ -1496,6 +1604,11 @@ fn validate_supported_endpoint_extensions( { return unsupported_endpoint_extension(context); } + if let Some(reason) = ip::unsupported_endpoint(endpoint) { + return Err(UnsupportedFeature::policy_shape(format!( + "{context} {reason}" + ))); + } validate_supported_graphql(context, endpoint)?; validate_supported_credentials(context, endpoint)?; validate_supported_json_rpc(context, endpoint)?; @@ -1636,33 +1749,83 @@ fn validate_supported_rest(context: &str, endpoint: &Endpoint) -> Result<(), Uns Ok(()) } -#[derive(Default)] -struct ProtocolAuthorityIndex { - all: BTreeSet, - wildcards: BTreeSet, - exact: BTreeMap>, +struct AttributeSummary { + first: Option, + mixed: bool, +} + +impl AttributeSummary { + fn conflicts(&self, value: T) -> bool { + self.mixed || self.first.is_some_and(|first| first != value) + } + + fn insert(&mut self, value: T) { + if let Some(first) = self.first { + self.mixed |= first != value; + } else { + self.first = Some(value); + } + } +} + +impl Default for AttributeSummary { + fn default() -> Self { + Self { + first: None, + mixed: false, + } + } +} + +struct AuthorityAttributeIndex { + all: BTreeMap>, + wildcards: BTreeMap>, + exact: BTreeMap>>, } -impl ProtocolAuthorityIndex { - fn overlaps(&self, host: &str, ports: &[u16]) -> bool { +impl Default for AuthorityAttributeIndex { + fn default() -> Self { + Self { + all: BTreeMap::new(), + wildcards: BTreeMap::new(), + exact: BTreeMap::new(), + } + } +} + +impl AuthorityAttributeIndex { + fn overlaps_with_different(&self, host: &str, ports: &[u16], value: T) -> bool { ports.iter().any(|port| { - self.wildcards.contains(port) - || if host.contains('*') { - self.all.contains(port) - } else { - self.exact + if host.contains('*') { + self.all + .get(port) + .is_some_and(|summary| summary.conflicts(value)) + } else { + self.wildcards + .get(port) + .is_some_and(|summary| summary.conflicts(value)) + || self + .exact .get(host) - .is_some_and(|ports_for_host| ports_for_host.contains(port)) - } + .and_then(|ports_for_host| ports_for_host.get(port)) + .is_some_and(|summary| summary.conflicts(value)) + } }) } - fn insert(&mut self, host: &str, ports: &[u16]) { - self.all.extend(ports); - if host.contains('*') { - self.wildcards.extend(ports); - } else { - self.exact.entry(host.to_owned()).or_default().extend(ports); + fn insert(&mut self, host: &str, ports: &[u16], value: T) { + for port in ports { + self.all.entry(*port).or_default().insert(value); + if host.contains('*') { + self.wildcards.entry(*port).or_default().insert(value); + } else { + self.exact + .entry(host.to_owned()) + .or_default() + .entry(*port) + .or_default() + .insert(value); + } } } } @@ -1671,8 +1834,13 @@ fn validate_no_cross_protocol_overlap( policy: &ContainmentPolicy, cancelled: Option<&AtomicBool>, ) -> Result<(), PolicyValidationError> { - let mut l4 = ProtocolAuthorityIndex::default(); - let mut rest = ProtocolAuthorityIndex::default(); + let mut protocols = AuthorityAttributeIndex::default(); + let mut allowed_ips = AuthorityAttributeIndex::default(); + let mut allowed_ip_values: BTreeMap<&[String], usize> = BTreeMap::new(); + let mut implicit_modes = AuthorityAttributeIndex::default(); + let mut different_allowed_ips_overlap = false; + let mut different_implicit_ip_modes_overlap = false; + let mut different_protocols_overlap = false; for endpoint in policy .network_policies .values() @@ -1683,17 +1851,41 @@ fn validate_no_cross_protocol_overlap( } let host = endpoint.host.to_ascii_lowercase(); let ports = endpoint.effective_ports(); - let (current, other) = match endpoint.protocol_kind() { - Protocol::L4 => (&mut l4, &rest), - Protocol::Rest => (&mut rest, &l4), - }; - if other.overlaps(&host, &ports) { - return Err(UnsupportedFeature::policy_shape( - "contains overlapping L4 and REST endpoints whose inspection selection is not modeled", - ) - .into()); + let protocol = endpoint.protocol_kind(); + let endpoint_allowed_ips = endpoint.allowed_ips.as_slice(); + let next_allowed_ip_id = allowed_ip_values.len(); + let allowed_ip_id = *allowed_ip_values + .entry(endpoint_allowed_ips) + .or_insert(next_allowed_ip_id); + different_allowed_ips_overlap |= + allowed_ips.overlaps_with_different(&host, &ports, allowed_ip_id); + different_protocols_overlap |= protocols.overlaps_with_different(&host, &ports, protocol); + if endpoint.allowed_ips.is_empty() { + let wildcard = endpoint.host.contains('*'); + different_implicit_ip_modes_overlap |= + implicit_modes.overlaps_with_different(&host, &ports, wildcard); + implicit_modes.insert(&host, &ports, wildcard); } - current.insert(&host, &ports); + allowed_ips.insert(&host, &ports, allowed_ip_id); + protocols.insert(&host, &ports, protocol); + } + if different_allowed_ips_overlap { + return Err(UnsupportedFeature::policy_shape( + "has overlapping endpoints with different allowed_ips; runtime first-endpoint selection is not modeled", + ) + .into()); + } + if different_implicit_ip_modes_overlap { + return Err(UnsupportedFeature::policy_shape( + "has overlapping exact and wildcard endpoints with different implicit destination IP modes", + ) + .into()); + } + if different_protocols_overlap { + return Err(UnsupportedFeature::policy_shape( + "contains overlapping L4 and REST endpoints whose inspection selection is not modeled", + ) + .into()); } Ok(()) } @@ -1749,6 +1941,7 @@ fn resource_limit_reason( let mut port_entry_count = 0_usize; let mut l7_count = 0_usize; + let mut ip_range_count = 0_usize; let mut total_pattern_bytes = 0_usize; for policy in policies { for path in policy @@ -1788,11 +1981,25 @@ fn resource_limit_reason( return Some(resource_limit_detail("l7_rules", l7_count, MAX_L7_RULES)); } + ip_range_count = ip_range_count.saturating_add(endpoint.allowed_ips.len()); + if ip_range_count > MAX_IP_RANGES { + return Some(resource_limit_detail( + "ip_ranges", + ip_range_count, + MAX_IP_RANGES, + )); + } + for value in [&endpoint.host, &endpoint.path] { if let Some(reason) = account_pattern_bytes(value, &mut total_pattern_bytes) { return Some(reason); } } + for range in &endpoint.allowed_ips { + if let Some(reason) = account_pattern_bytes(range, &mut total_pattern_bytes) { + return Some(reason); + } + } for rule in &endpoint.rules { for value in [&rule.allow.path, &rule.allow.method] { if let Some(reason) = account_pattern_bytes(value, &mut total_pattern_bytes) @@ -2022,6 +2229,20 @@ mod tests { CheckOptions::new(Duration::from_secs(10)) } + // Keep address permissions identical when testing hostname/binary logic: + // an exact declaration without allowed_ips permits private addresses, + // whereas a wildcard declaration without allowed_ips does not. + fn fixed_test_ips(mut policy: ContainmentPolicy) -> ContainmentPolicy { + for endpoint in policy + .network_policies + .values_mut() + .flat_map(|rule| &mut rule.endpoints) + { + endpoint.allowed_ips = vec!["8.8.8.0/24".to_owned()]; + } + policy + } + #[test] fn filesystem_containment_and_counterexample() { let boundary = @@ -2140,6 +2361,8 @@ mod tests { let candidate = parse( "version: 1\nnetwork_policies:\n candidate:\n endpoints: [{ host: api_internal.example.com, port: 443 }]\n binaries: []\n", ); + let boundary = fixed_test_ips(boundary); + let candidate = fixed_test_ips(candidate); assert!(matches!( check_within_boundary(&boundary, &candidate, options()), CheckResult::Within(_) @@ -2261,7 +2484,7 @@ mod tests { } #[test] - fn host_wildcard_zero_length_suffix_preserves_exact_deny() { + fn overlapping_exact_deny_and_wildcard_is_unsupported() { let boundary = parse( "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: 'api*.example.com', port: 443, protocol: rest, enforcement: enforce, access: full }\n binaries: [{ path: /usr/bin/curl }]\n deny:\n endpoints:\n - host: api.example.com\n port: 443\n protocol: rest\n enforcement: enforce\n access: full\n deny_rules: [{ method: GET, path: '/**' }]\n binaries: [{ path: /usr/bin/curl }]\n", ); @@ -2269,14 +2492,14 @@ mod tests { "version: 1\nnetwork_policies:\n allow:\n endpoints:\n - { host: 'api*.example.com', port: 443, protocol: rest, enforcement: enforce, access: full }\n binaries: [{ path: /usr/bin/curl }]\n", ); let result = check_within_boundary(&boundary, &candidate, options()); - assert!(matches!( - result, - CheckResult::Exceeds(ref evidence) - if matches!( - evidence.counterexample(), - Counterexample::Network { host, .. } if host == "api.example.com" - ) - )); + assert!( + matches!( + result, + CheckResult::Unsupported(ref evidence) + if evidence.reason().contains("different implicit destination IP modes") + ), + "{result:?}" + ); } #[test] @@ -2535,6 +2758,8 @@ mod tests { let candidate = parse( "version: 1\nnetwork_policies:\n shared:\n endpoints: [{ host: '*.example.com', port: 443 }]\n binaries: [{ path: '/usr/bin/*' }]\n exact:\n endpoints: [{ host: api.example.com, port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", ); + let boundary = fixed_test_ips(boundary); + let candidate = fixed_test_ips(candidate); assert!(matches!( check_within_boundary(&boundary, &candidate, options()), CheckResult::Unsupported(ref evidence) @@ -2857,6 +3082,32 @@ network_policies: } } + #[test] + fn overlap_index_interns_exact_limit_allowed_ips_across_ports() { + let empty = parse("version: 1\n"); + let mut policy = parse( + "version: 1 +network_policies: + api: + endpoints: [{ host: api.example.com, port: 443 }] +", + ); + let endpoint = &mut policy.network_policies.get_mut("api").unwrap().endpoints[0]; + endpoint.port = 0; + endpoint.ports = (1..=32_768).collect(); + endpoint.allowed_ips = vec!["10.0.0.0/8".to_owned(); MAX_IP_RANGES / 2]; + let second = endpoint.clone(); + policy + .network_policies + .get_mut("api") + .unwrap() + .endpoints + .push(second); + + assert_eq!(resource_limit_reason(&empty, &policy), None); + assert!(validate_supported_policy(&policy, None).is_ok()); + } + #[test] fn excessive_model_size_is_inconclusive() { let boundary = parse("version: 1\n"); @@ -2961,6 +3212,8 @@ network_policies: let recursive = parse( "version: 1\nnetwork_policies:\n n:\n endpoints: [{ host: '**.example.com', port: 443 }]\n binaries: [{ path: /usr/bin/curl }]\n", ); + let recursive = fixed_test_ips(recursive); + let nested = fixed_test_ips(nested); assert!(matches!( check_within_boundary(&recursive, &nested, options()), CheckResult::Within(_) diff --git a/crates/openshell-prover/src/containment/execution.rs b/crates/openshell-prover/src/containment/execution.rs new file mode 100644 index 0000000000..6c9eedbb01 --- /dev/null +++ b/crates/openshell-prover/src/containment/execution.rs @@ -0,0 +1,194 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Configuration containment, assuming the same image identity resolution and +//! execution environment. This does not attest successful Landlock installation. + +use super::{ + CheckResult, ContainmentPolicy, Counterexample, ExceedsEvidence, ReasonCode, unsupported, +}; +use openshell_policy_schema::LandlockCompatibility; + +pub(super) fn unsupported_reason(policy: &ContainmentPolicy) -> Option { + if let Some(process) = &policy.process { + for identity in [&process.run_as_user, &process.run_as_group] { + // Omission remains unresolved: Docker/Podman may use OCI Config.User. + // Only runtime-supported sandbox identities plus root (to diagnose + // escalation) are understood; arbitrary account names are not. + if !identity.is_empty() + && !matches!(identity.as_str(), "sandbox" | "root" | "0") + && !identity + .parse::() + .is_ok_and(|id| (1..u32::MAX).contains(&id)) + { + return Some(format!("uses unsupported process identity '{identity}'")); + } + } + } + None +} + +pub(super) fn check( + boundary: &ContainmentPolicy, + candidate: &ContainmentPolicy, +) -> Option { + let boundary_user = boundary + .process + .as_ref() + .map_or("", |process| process.run_as_user.as_str()); + let candidate_user = candidate + .process + .as_ref() + .map_or("", |process| process.run_as_user.as_str()); + let boundary_group = boundary + .process + .as_ref() + .map_or("", |process| process.run_as_group.as_str()); + let candidate_group = candidate + .process + .as_ref() + .map_or("", |process| process.run_as_group.as_str()); + let mut unresolved_change = None; + for (field, boundary, candidate) in [ + ("run_as_user", boundary_user, candidate_user), + ("run_as_group", boundary_group, candidate_group), + ] { + if boundary == candidate { + continue; + } + let root = |identity: &str| matches!(identity, "root" | "0"); + if root(boundary) && root(candidate) { + continue; + } + if !boundary.is_empty() && !root(boundary) && root(candidate) { + return Some(CheckResult::Exceeds(ExceedsEvidence( + Counterexample::Process { + field, + boundary: boundary.to_owned(), + candidate: candidate.to_owned(), + }, + ))); + } + unresolved_change.get_or_insert_with(|| { + unsupported( + ReasonCode::UnsupportedPolicyShape, + format!( + "process {field} changes from '{boundary}' to '{candidate}'; identity resolution and ordering require execution-environment evidence" + ), + ) + }); + } + if boundary + .landlock + .as_ref() + .is_some_and(|policy| policy.compatibility == LandlockCompatibility::HardRequirement) + && !candidate + .landlock + .as_ref() + .is_some_and(|policy| policy.compatibility == LandlockCompatibility::HardRequirement) + { + return Some(CheckResult::Exceeds(ExceedsEvidence( + Counterexample::Landlock { + boundary: "hard_requirement".to_owned(), + candidate: "best_effort".to_owned(), + }, + ))); + } + unresolved_change +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::containment::{CheckOptions, check_within_boundary, parse_policy_str}; + + fn result(boundary: &str, candidate: &str) -> CheckResult { + check_within_boundary( + &parse_policy_str(&format!("version: 1\n{boundary}")).unwrap(), + &parse_policy_str(&format!("version: 1\n{candidate}")).unwrap(), + CheckOptions { + timeout: std::time::Duration::from_secs(10), + }, + ) + } + + #[test] + fn process_matches_and_root_escalations() { + let sandbox = "process: {run_as_user: sandbox, run_as_group: sandbox}"; + assert!(matches!(result(sandbox, sandbox), CheckResult::Within(_))); + for candidate in [ + "process: {run_as_user: root, run_as_group: sandbox}", + "process: {run_as_user: sandbox, run_as_group: '0'}", + ] { + assert!(matches!( + result(sandbox, candidate), + CheckResult::Exceeds(_) + )); + } + for candidate in [ + "process: {run_as_user: '1001', run_as_group: sandbox}", + "process: {}", + "", + ] { + assert!(matches!( + result(sandbox, candidate), + CheckResult::Unsupported(_) + )); + } + assert!(matches!(result("", sandbox), CheckResult::Unsupported(_))); + } + + #[test] + fn landlock_compatibility_and_defaults() { + let hard = "landlock: {compatibility: hard_requirement}"; + for soft in ["", "landlock: {}", "landlock: {compatibility: best_effort}"] { + assert!(matches!(result(soft, hard), CheckResult::Within(_))); + assert!(matches!(result(hard, soft), CheckResult::Exceeds(_))); + assert!(matches!(result(soft, soft), CheckResult::Within(_))); + } + assert!(matches!(result(hard, hard), CheckResult::Within(_))); + } + + #[test] + fn unresolved_identity_changes_do_not_mask_definitive_execution_violations() { + let boundary = "process: {run_as_user: sandbox, run_as_group: sandbox}\nlandlock: {compatibility: hard_requirement}"; + let root_group = "process: {run_as_user: '1001', run_as_group: root}\nlandlock: {compatibility: hard_requirement}"; + assert!(matches!( + result(boundary, root_group), + CheckResult::Exceeds(ref evidence) + if matches!(evidence.counterexample(), Counterexample::Process { field: "run_as_group", .. }) + )); + + let weaker_landlock = "process: {run_as_user: '1001', run_as_group: sandbox}\nlandlock: {compatibility: best_effort}"; + assert!(matches!( + result(boundary, weaker_landlock), + CheckResult::Exceeds(ref evidence) + if matches!(evidence.counterexample(), Counterexample::Landlock { .. }) + )); + } + + #[test] + fn unresolved_identity_change_does_not_mask_filesystem_expansion() { + let boundary = + "process: {run_as_user: sandbox, run_as_group: sandbox}\nfilesystem_policy: {}"; + let candidate = "process: {run_as_user: '1001', run_as_group: sandbox}\nfilesystem_policy: {read_write: [/tmp]}"; + assert!(matches!( + result(boundary, candidate), + CheckResult::Exceeds(ref evidence) + if matches!(evidence.counterexample(), Counterexample::Filesystem { .. }) + )); + } + + #[test] + fn unknown_fields_and_identities_fail_closed() { + for policy in ["process: {capabilities: all}", "landlock: {disabled: true}"] { + assert!(parse_policy_str(&format!("version: 1\n{policy}")).is_err()); + } + let unsupported_identity = "process: {run_as_user: nobody}"; + assert!(matches!( + result(unsupported_identity, unsupported_identity), + CheckResult::Unsupported(_) + )); + assert!(parse_policy_str("version: 1\nlandlock: {compatibility: disabled}").is_err()); + } +} diff --git a/crates/openshell-prover/src/containment/ip.rs b/crates/openshell-prover/src/containment/ip.rs new file mode 100644 index 0000000000..2274846548 --- /dev/null +++ b/crates/openshell-prover/src/containment/ip.rs @@ -0,0 +1,528 @@ +// SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved. +// SPDX-License-Identifier: Apache-2.0 + +//! Destination-address predicates for the explicit proxy. DNS answers and the +//! trusted gateway binding are universally quantified, not resolved by the CLI. + +use super::{ + ContainmentPolicy, Endpoint, SymbolicAction, binaries_match, bool_or, + endpoint_matches_connection, str_eq_any, +}; +use std::net::{IpAddr, Ipv4Addr, Ipv6Addr}; +use z3::ast::{Ast, BV, Bool}; +use z3::{Model, Solver}; + +const HARD_V4: &[&str] = &["127.0.0.0/8", "169.254.0.0/16", "0.0.0.0/32"]; +const HARD_V6: &[&str] = &["::/128", "::1/128", "fe80::/10"]; +const INTERNAL_V4: &[&str] = &[ + "10.0.0.0/8", + "172.16.0.0/12", + "192.168.0.0/16", + "192.0.2.0/24", + "198.51.100.0/24", + "203.0.113.0/24", + "255.255.255.255/32", + "100.64.0.0/10", + "192.0.0.0/24", + "198.18.0.0/15", +]; + +pub(super) struct SymbolicIp { + bits: BV, + v6: Bool, +} + +impl SymbolicIp { + pub(super) fn new(name: &str) -> Self { + Self { + bits: BV::new_const(format!("{name}_destination_ip"), 128), + v6: Bool::new_const(format!("{name}_ipv6")), + } + } + + pub(super) fn concrete(ip: IpAddr) -> Self { + let net = Network::from_ip(ip); + Self { + bits: bits(net.address), + v6: Bool::from_bool(net.v6), + } + } + + pub(super) fn assert_domain(&self, solver: &Solver) { + solver.assert( + self.v6 + .not() + .implies(self.bits.extract(127, 32).eq(BV::from_u64(0, 96))), + ); + } + + pub(super) fn decode(&self, model: &Model) -> Option { + let high = model.eval(&self.bits.extract(127, 64), true)?.as_u64()?; + let low = model.eval(&self.bits.extract(63, 0), true)?.as_u64()?; + Some(if model.eval(&self.v6, true)?.as_bool()? { + IpAddr::V6(Ipv6Addr::from((u128::from(high) << 64) | u128::from(low))) + } else { + IpAddr::V4(Ipv4Addr::from(u32::try_from(low).ok()?)) + }) + } + + fn matches(&self, net: Network) -> Bool { + Bool::and(&[ + self.v6.eq(Bool::from_bool(net.v6)), + self.bits + .bvand(bits(net.mask())) + .eq(bits(net.address & net.mask())), + ]) + } + + fn ranges(&self, ranges: &[&str]) -> Bool { + bool_or( + ranges + .iter() + .map(|range| self.matches(Network::parse(range).unwrap())), + ) + } + + fn mapped_v4_ranges(&self, ranges: &[&str]) -> Bool { + bool_or(ranges.iter().map(|range| { + let v4 = Network::parse(range).unwrap(); + self.matches(Network { + v6: true, + address: (0xffff_u128 << 32) | v4.address, + prefix: 96 + v4.prefix, + }) + })) + } + + fn hard_blocked(&self) -> Bool { + Bool::or(&[ + self.ranges(HARD_V4), + self.ranges(HARD_V6), + self.mapped_v4_ranges(HARD_V4), + ]) + } + + fn internal(&self) -> Bool { + Bool::or(&[ + self.hard_blocked(), + self.ranges(INTERNAL_V4), + self.mapped_v4_ranges(INTERNAL_V4), + self.ranges(&["fc00::/7"]), + ]) + } +} + +fn bits(value: u128) -> BV { + let high = u64::try_from(value >> 64).expect("high 64 bits"); + let low = u64::try_from(value & u128::from(u64::MAX)).expect("low 64 bits"); + BV::from_u64(high, 64).concat(BV::from_u64(low, 64)) +} + +#[derive(Clone, Copy)] +struct Network { + address: u128, + prefix: u32, + v6: bool, +} + +impl Network { + fn from_ip(ip: IpAddr) -> Self { + match ip { + IpAddr::V4(ip) => Self { + address: u128::from(u32::from(ip)), + prefix: 32, + v6: false, + }, + IpAddr::V6(ip) => Self { + address: u128::from(ip), + prefix: 128, + v6: true, + }, + } + } + + fn parse(value: &str) -> Option { + let (address, prefix) = value + .split_once('/') + .map_or((value, None), |(a, p)| (a, Some(p))); + let mut network = Self::from_ip(address.parse().ok()?); + if let Some(prefix) = prefix { + let prefix = prefix.parse().ok()?; + if prefix > network.prefix { + return None; + } + network.prefix = prefix; + } + Some(network) + } + + fn mask(self) -> u128 { + let width = if self.v6 { 128 } else { 32 }; + if self.prefix == 0 { + 0 + } else { + u128::MAX << (width - self.prefix) + } + } + + fn overlaps(self, other: Self) -> bool { + self.v6 == other.v6 + && (self.address & self.mask() & other.mask()) + == (other.address & self.mask() & other.mask()) + } +} + +pub(super) fn unsupported_endpoint(endpoint: &Endpoint) -> Option { + // Numeric wildcard hosts can match IP literals, whose implicit allowlist + // depends on the input string. Keep that unresolved rather than treating + // them as ordinary DNS names. + if endpoint.host.contains('*') + && endpoint + .host + .bytes() + .all(|b| b.is_ascii_digit() || matches!(b, b'.' | b'*')) + { + return Some( + "uses an IP-literal wildcard whose address resolution is not modeled".to_owned(), + ); + } + for raw in &endpoint.allowed_ips { + let Some(net) = Network::parse(raw) else { + return Some(format!("has invalid allowed_ips entry '{raw}'")); + }; + let blocked = HARD_V4 + .iter() + .chain(HARD_V6) + .map(|range| Network::parse(range).unwrap()); + let mut blocked = blocked.chain(HARD_V4.iter().map(|range| { + let v4 = Network::parse(range).unwrap(); + Network { + v6: true, + address: (0xffff_u128 << 32) | v4.address, + prefix: 96 + v4.prefix, + } + })); + if blocked.any(|blocked| net.overlaps(blocked)) { + return Some(format!( + "has allowed_ips entry '{raw}' overlapping a runtime always-blocked range" + )); + } + } + None +} + +pub(super) fn sample_addresses(endpoint: &Endpoint) -> Vec { + let mut addresses = vec!["8.8.8.8".parse().unwrap(), "10.0.0.1".parse().unwrap()]; + if let Some(net) = endpoint + .allowed_ips + .first() + .and_then(|raw| Network::parse(raw)) + { + let address = net.address & net.mask(); + addresses.push(if net.v6 { + IpAddr::V6(Ipv6Addr::from(address)) + } else { + IpAddr::V4(Ipv4Addr::from( + u32::try_from(address).expect("IPv4 network"), + )) + }); + } + addresses +} + +pub(super) fn policy_allows( + policy: &ContainmentPolicy, + action: &SymbolicAction, + binary_identity_required: bool, +) -> Bool { + bool_or(policy.network_policies.values().flat_map(|rule| { + rule.endpoints.iter().map(move |endpoint| { + let selected = Bool::and(&[ + binaries_match(rule, action, binary_identity_required), + endpoint_matches_connection(endpoint, action), + ]); + let exact = !endpoint.host.contains('*'); + let control_port = + bool_or([2379_u64, 2380, 6443, 10250, 10255].map(|port| action.port.eq(port))); + let ordinary = if endpoint.allowed_ips.is_empty() { + endpoint.host.parse::().map_or_else( + |_| { + if exact { + Bool::and(&[!action.ip.hard_blocked(), !control_port.clone()]) + } else { + !action.ip.internal() + } + }, + |ip| { + Bool::and(&[ + action.ip.matches(Network::from_ip(ip)), + !action.ip.hard_blocked(), + !control_port.clone(), + ]) + }, + ) + } else { + Bool::and(&[ + bool_or(endpoint.allowed_ips.iter().map(|raw| { + action + .ip + .matches(Network::parse(raw).expect("validated CIDR")) + })), + !action.ip.hard_blocked(), + !control_port.clone(), + ]) + }; + let alias = str_eq_any( + &action.host, + &[ + "host.openshell.internal", + "host.containers.internal", + "host.docker.internal", + ], + ); + let trusted = Bool::and(&[alias, action.trusted_gateway.clone()]); + let gateway = Bool::and(&[ + Bool::or(&[ + action.ip.ranges(&["169.254.0.0/16", "fe80::/10"]), + action.ip.mapped_v4_ranges(&["169.254.0.0/16"]), + ]), + !action.ip.ranges(&["169.254.169.254/32"]), + !action.ip.mapped_v4_ranges(&["169.254.169.254/32"]), + !control_port, + ]); + let can_match_gateway = [ + "host.openshell.internal", + "host.containers.internal", + "host.docker.internal", + ] + .iter() + .any(|alias| { + z3::ast::String::from(*alias) + .regex_matches(&super::glob_regex(&endpoint.host.to_ascii_lowercase(), ".")) + .simplify() + .as_bool() + != Some(false) + }); + let address = if can_match_gateway { + trusted.ite(&gateway, &ordinary) + } else { + ordinary + }; + // A literal destination cannot resolve to another address even + // when the explicit CIDR covers that other address. + let literal = endpoint.host.parse::().map_or_else( + |_| Bool::from_bool(true), + |ip| action.ip.matches(Network::from_ip(ip)), + ); + Bool::and(&[selected, address, literal]) + }) + })) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::containment::{ + CheckOptions, CheckResult, Counterexample, check_within_boundary, parse_policy_str, + }; + + fn policy(host: &str, ips: &str) -> ContainmentPolicy { + parse_policy_str(&format!("version: 1\nnetwork_policies:\n api:\n endpoints: [{{host: '{host}', port: 443, allowed_ips: [{ips}]}}]\n binaries: [{{path: /usr/bin/curl}}]\n")).unwrap() + } + + fn check(host: &str, boundary: &str, candidate: &str) -> CheckResult { + check_within_boundary(&policy(host, boundary), &policy(host, candidate), options()) + } + + fn options() -> CheckOptions { + CheckOptions { + timeout: std::time::Duration::from_secs(10), + } + } + + #[test] + fn ipv4_ipv6_and_cidr_union_containment() { + for (maximum, candidate) in [ + ("10.0.0.0/8", "10.2.0.0/16"), + ("2001:db8::/32", "2001:db8:1234::/48"), + ("10.0.0.0/9, 10.128.0.0/9", "10.0.0.0/8"), + ("10.2.3.4", "10.2.3.4/32"), + ] { + let result = check("api.example.com", maximum, candidate); + assert!( + matches!(result, CheckResult::Within(_)), + "{maximum} -> {candidate}: {result:?}" + ); + } + for (maximum, candidate) in [ + ("10.2.0.0/16", "10.0.0.0/8"), + ("2001:db8:1234::/48", "2001:db8::/32"), + ("10.0.0.0/8", "2001:db8::/32"), + ] { + let result = check("api.example.com", maximum, candidate); + assert!(matches!(result, CheckResult::Exceeds(_)), "{result:?}"); + if let CheckResult::Exceeds(evidence) = result { + assert!(matches!( + evidence.counterexample(), + Counterexample::Network { .. } + )); + } + } + } + + #[test] + fn defaults_and_aliases_use_runtime_modes() { + assert!(matches!( + check("api.example.com", "", "10.2.0.0/16"), + CheckResult::Within(_) + )); + assert!(matches!( + check("api.example.com", "10.2.0.0/16", ""), + CheckResult::Exceeds(_) + )); + let private_expansion = check("*.example.com", "", "10.2.0.0/16"); + assert!( + matches!(private_expansion, CheckResult::Exceeds(_)), + "{private_expansion:?}" + ); + assert!(matches!( + check("host.openshell.internal", "10.0.0.0/8", "10.2.0.0/16"), + CheckResult::Within(_) + )); + assert!(matches!( + check("host.openshell.internal", "10.2.0.0/16", "10.0.0.0/8"), + CheckResult::Exceeds(_) + )); + let result = check_within_boundary( + &policy("*.example.com", ""), + &policy("api.example.com", ""), + options(), + ); + assert!( + matches!(result, CheckResult::Exceeds(_)), + "exact declarations permit private addresses unlike wildcard defaults: {result:?}" + ); + } + + #[test] + fn exact_and_wildcard_overlap_with_implicit_ip_modes_is_unsupported() { + let boundary = parse_policy_str( + "version: 1\nnetwork_policies:\n api:\n endpoints:\n - { host: '*.example.com', port: 6443 }\n - { host: api.example.com, port: 6443 }\n binaries: [{ path: /usr/bin/curl }]\n", + ) + .unwrap(); + let candidate = parse_policy_str( + "version: 1\nnetwork_policies:\n api:\n endpoints:\n - { host: '*.example.com', port: 6443 }\n binaries: [{ path: /usr/bin/curl }]\n", + ) + .unwrap(); + + let result = check_within_boundary(&boundary, &candidate, options()); + assert!( + matches!( + result, + CheckResult::Unsupported(ref evidence) + if evidence.reason().contains("different implicit destination IP modes") + ), + "{result:?}" + ); + } + + #[test] + fn split_rule_exact_and_wildcard_overlap_with_implicit_ip_modes_is_unsupported() { + let boundary = parse_policy_str( + "version: 1\nnetwork_policies:\n wildcard:\n endpoints:\n - { host: '*.example.com', port: 6443 }\n binaries: [{ path: /usr/bin/curl }]\n exact:\n endpoints:\n - { host: api.example.com, port: 6443 }\n binaries: [{ path: /usr/bin/curl }]\n", + ) + .unwrap(); + let candidate = parse_policy_str( + "version: 1\nnetwork_policies:\n api:\n endpoints:\n - { host: '*.example.com', port: 6443 }\n binaries: [{ path: /usr/bin/curl }]\n", + ) + .unwrap(); + + let result = check_within_boundary(&boundary, &candidate, options()); + assert!( + matches!( + result, + CheckResult::Unsupported(ref evidence) + if evidence.reason().contains("different implicit destination IP modes") + ), + "{result:?}" + ); + } + + #[test] + fn malformed_blocked_and_order_dependent_inputs_are_unsupported() { + for ips in [ + "not-an-ip", + "10.0.0.1/99", + "127.0.0.0/8", + "::ffff:127.0.0.1", + "0.0.0.0/0", + "::/0", + ] { + assert!( + matches!( + check("api.example.com", ips, ips), + CheckResult::Unsupported(_) + ), + "{ips}" + ); + } + let mut ambiguous = policy("api.example.com", "10.0.0.0/8"); + let mut second = ambiguous.network_policies["api"].endpoints[0].clone(); + second.allowed_ips = vec!["10.1.0.0/16".to_owned()]; + ambiguous + .network_policies + .get_mut("api") + .unwrap() + .endpoints + .push(second); + assert!(matches!( + check_within_boundary(&ambiguous, &ambiguous, options()), + CheckResult::Unsupported(_) + )); + } + + #[test] + fn address_classification_matches_runtime() { + for raw in [ + "8.8.8.8", + "10.1.2.3", + "127.0.0.1", + "169.254.1.1", + "0.0.0.0", + "192.0.2.1", + "100.64.0.1", + "198.18.0.1", + "::", + "::1", + "fe80::1", + "fc00::1", + "2001:db8::1", + "::ffff:127.0.0.1", + "::ffff:10.2.3.4", + "::ffff:8.8.8.8", + ] { + let ip: IpAddr = raw.parse().unwrap(); + let symbolic = SymbolicIp::concrete(ip); + assert_eq!( + symbolic.hard_blocked().simplify().as_bool(), + Some(openshell_core::net::is_always_blocked_ip(ip)), + "{raw}" + ); + assert_eq!( + symbolic.internal().simplify().as_bool(), + Some(openshell_core::net::is_internal_ip(ip)), + "{raw}" + ); + } + } + + #[test] + fn excessive_ip_ranges_fail_before_constructing_the_model() { + let mut huge = policy("api.example.com", "10.0.0.0/8"); + huge.network_policies.get_mut("api").unwrap().endpoints[0].allowed_ips = + vec!["10.0.0.0/8".to_owned(); 4097]; + assert!( + matches!(check_within_boundary(&huge, &huge, options()), CheckResult::Inconclusive(ref reason) if reason.reason_code() == super::super::ReasonCode::ResourceLimit) + ); + } +} diff --git a/crates/openshell-prover/tests/containment_api.rs b/crates/openshell-prover/tests/containment_api.rs index a3ac2d7465..47c8383292 100644 --- a/crates/openshell-prover/tests/containment_api.rs +++ b/crates/openshell-prover/tests/containment_api.rs @@ -6,7 +6,7 @@ use std::time::Duration; use openshell_prover::containment::{ - CheckDomain, CheckOptions, CheckResult, Counterexample, Protocol, ReasonCode, + CheckCoverage, CheckDomain, CheckOptions, CheckResult, Counterexample, Protocol, ReasonCode, check_within_boundary, parse_policy_str, }; @@ -38,10 +38,19 @@ fn domain_name(domain: CheckDomain) -> &'static str { CheckDomain::Filesystem => "filesystem", CheckDomain::NetworkL4 => "network_l4", CheckDomain::NetworkRest => "network_rest", + CheckDomain::Process => "process", + CheckDomain::Landlock => "landlock", _ => "unknown", } } +fn covers(coverage: &CheckCoverage, expected: &str) -> bool { + coverage + .domains + .iter() + .any(|domain| domain_name(*domain) == expected) +} + #[test] fn external_callers_use_extensible_construction_and_matching_patterns() { let boundary = parse_policy_str( @@ -63,14 +72,7 @@ fn external_callers_use_extensible_construction_and_matching_patterns() { let CheckResult::Exceeds(evidence) = &result else { panic!("expected filesystem violation, got {result:?}"); }; - assert_eq!(evidence.scope().model_version, "boundary-v1"); - assert!( - evidence - .scope() - .domains - .iter() - .any(|domain| domain_name(*domain) == "filesystem") - ); + assert!(covers(evidence.coverage(), "filesystem")); match evidence.counterexample() { Counterexample::Filesystem { access, path, .. } => { assert_eq!(access.as_str(), "write"); @@ -104,5 +106,5 @@ fn external_callers_read_reason_evidence_and_authorize_only_within() { ReasonCode::SolverTimeout => {} _ => panic!("unexpected reason code"), } - assert_eq!(evidence.scope().policy_version, 1); + assert!(covers(evidence.coverage(), "landlock")); } diff --git a/crates/openshell-prover/tests/runtime_parity.rs b/crates/openshell-prover/tests/runtime_parity.rs index f124e82623..198198bdae 100644 --- a/crates/openshell-prover/tests/runtime_parity.rs +++ b/crates/openshell-prover/tests/runtime_parity.rs @@ -314,10 +314,15 @@ network_policies: &input, "data.openshell.sandbox.allow_request" )); - assert!(matches!( - check(boundary, candidate), - CheckResult::Exceeds(_) - )); + let result = check(boundary, candidate); + assert!( + matches!( + result, + CheckResult::Unsupported(ref evidence) + if evidence.reason().contains("different implicit destination IP modes") + ), + "{result:?}" + ); } #[test] diff --git a/docs/reference/policy-prover.mdx b/docs/reference/policy-prover.mdx index 4e251adc3e..f34106c83a 100644 --- a/docs/reference/policy-prover.mdx +++ b/docs/reference/policy-prover.mdx @@ -100,12 +100,13 @@ openshell-prover check candidate.yaml \ --output json ``` -The JSON object includes the result, exit code, input paths, prover version, -model version, checked policy version, and modeled domains. The documented -semantics and environmental conditions for that scope are tied to its model -version. An exceeding result also includes a filesystem or network -counterexample. Automation should use `result` and `reason_code` instead of -parsing the human-readable explanation. +The JSON object includes the result, exit code, input paths, schema version, +prover version, and modeled domains. `schema_version` versions the JSON contract, +`prover_version` identifies the implementation that produced the result, and +`coverage.domains` is the machine-readable declaration of modeled policy +domains. An exceeding result also includes a typed counterexample. Automation +should use `result` and `reason_code` instead of parsing the human-readable +explanation. | Field | When populated | |---|---| @@ -113,6 +114,21 @@ parsing the human-readable explanation. | `reason_code` | A stable identifier for an emitted `error`, `unsupported`, or `inconclusive` result; otherwise `null`. | | `reason` | A human-readable explanation paired with `reason_code`; otherwise `null`. | +The `counterexample.domain` field selects one of these objects: + +| Domain | Fields | +|---|---| +| `filesystem` | `access` (`read` or `write`) and `path`. | +| `process` | `field` (`run_as_user` or `run_as_group`), `boundary`, and `candidate`. | +| `landlock` | `boundary` and `candidate` compatibility modes. | +| `network` | `binary`, `ancestor_binary`, `binary_identity_required`, `host`, `destination_ip`, `trusted_gateway`, `port`, `protocol`, `method`, and `path`. | + +Network `binary` and `ancestor_binary` values are `null` when binary identity +enforcement is disabled. `method` and `path` are `null` for L4 witnesses. +`trusted_gateway: true` means the witness uses a recognized host-gateway alias +with a runtime-provided trusted gateway binding; `false` uses ordinary +destination validation. + The stable reason codes are `invalid_input`, `unsupported_policy_shape`, `unresolved_workdir`, `unresolved_binary_path`, `unresolved_filesystem_path`, `solver_timeout`, `solver_unknown`, @@ -132,7 +148,7 @@ openshell-prover check candidate.yaml \ | Exit | Result | Meaning | |---|---|---| -| `0` | `within_boundary` | Containment was established for the reported model scope. | +| `0` | `within_boundary` | Containment was established for the reported modeled domains. | | `1` | `exceeds_boundary` | The candidate exceeds the boundary; inspect the counterexample. | | `2` | `error` | Arguments, input files, policy syntax, or command execution prevented a valid check. | | `3` | `unsupported` or `inconclusive` | The model cannot soundly cover the policy shape, or the solver did not reach a determination. | @@ -143,10 +159,11 @@ inconclusive results as failures in CI. ## Interpretation and Limits -The initial containment model covers filesystem paths, L4 network authority, -and enforced REST method and path authority, including explicit REST denies. -The result object reports the domains used for each check. Policies that use -recognized authority outside that model return `unsupported` rather than +The containment check covers filesystem paths, process identity settings, +Landlock compatibility requirements, L4 destination authority, and enforced +REST method and path authority, including explicit REST denies. The result +object reports the policy domains modeled by each check. Policies that use +recognized authority outside that coverage return `unsupported` rather than silently ignoring it. Both inputs use the same bounded YAML/JSON parser and authored policy schema as @@ -157,12 +174,50 @@ containment model return `unsupported` and exit `3`. The prover applies aggregate limits across the candidate and boundary before semantic shape validation: 1,024 network rules, 4,096 endpoints, 4,096 binary -selectors, 65,536 authored port entries, 16,384 REST rules, 4 KiB per modeled -pattern, and 1 MiB of modeled pattern text. Exceeding any limit returns -`inconclusive` with `reason_code: resource_limit`. A cancellation already -requested at preflight takes precedence over that result; otherwise a resource -limit takes precedence over unsupported policy-shape diagnostics. This ordering -keeps validation work bounded for checked-in CI inputs. +selectors, 65,536 authored port entries, 4,096 `allowed_ips` entries, 16,384 +REST rules, 4 KiB per modeled pattern, and 1 MiB of modeled pattern text. +Exceeding any limit returns `inconclusive` with `reason_code: resource_limit`. +A cancellation already requested at preflight takes precedence over that +result; otherwise a resource limit takes precedence over unsupported +policy-shape diagnostics. This ordering keeps validation work bounded for +checked-in CI inputs. + +### Process and Landlock settings + +Matching supported `run_as_user` and `run_as_group` values do not expand the +configuration. Changing an explicit non-root identity to `root` or `0` returns +`exceeds_boundary` with the field and both values. Other identity changes return +`unsupported`; the command does not resolve accounts from a sandbox image. +These comparisons assume consistent identity resolution and execution settings. +They do not prove permission relationships between arbitrary Linux accounts. + +Landlock `hard_requirement` may not become `best_effort`. That change returns +`exceeds_boundary`. Keeping the same mode or strengthening it to +`hard_requirement` passes this part of the check. This compares the requested +requirement, not whether a target kernel successfully installed Landlock +restrictions. + +### Destination IP restrictions + +The network action includes an IPv4 or IPv6 destination address. CIDR entries +in `allowed_ips` are modeled together with host, port, executable, and REST +restrictions; network counterexamples include `destination_ip`. An empty IP +list follows the runtime's destination rules and is not a universal allowlist. +The check does not resolve DNS on the host running the CLI. + +Policies whose potentially overlapping endpoints select different destination +restrictions remain unsupported because the runtime uses the selected +endpoint's address filter. The prover conservatively treats wildcard host +selectors on a shared port as potentially overlapping, including when their +literal suffixes differ. CIDR unions within a supported endpoint are checked by +the solver. Unsupported IP-literal wildcard selectors and ranges rejected by +the runtime also cannot produce a successful proof. + +Consumers must inspect `coverage.domains` and require every domain relevant to +their authorization decision. A successful result applies only to those +reported domains and the documented assumptions. + +### Remaining limits Network binary selectors, endpoint host and path selectors, and REST allow and deny method and path selectors must use ASCII literals in both the candidate and @@ -212,5 +267,5 @@ state. In particular: returns `exceeds_boundary`. Use the [Policy Schema Reference](/reference/policy-schema) for the full policy -language. A successful prover result covers only the scope reported in its -evidence. +language. A successful prover result covers only the policy domains reported in +its evidence.