feat(prover): check process, Landlock, and destination IP containment

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)

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.

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<ScopeJson<'a>>,
+    coverage: Option<CoverageJson<'a>>,
     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,18 +317,20 @@ fn render_cancelled(output: OutputFormat, inputs: InputsJson) -> Result<u8, Stri
 }
 
 fn result_envelope(result: &CheckResult, inputs: InputsJson) -> Result<Envelope<'_>, 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())?),
             None,
             None,
         ),
         CheckResult::Unsupported(evidence) => (
-            evidence.scope(),
+            evidence.coverage(),
             "unsupported",
             3,
             None,
@@ -334,7 +345,7 @@ fn result_envelope(result: &CheckResult, inputs: InputsJson) -> Result<Envelope<
                     3
                 };
             (
-                evidence.scope(),
+                evidence.coverage(),
                 "inconclusive",
                 exit_code,
                 None,
@@ -347,7 +358,7 @@ fn result_envelope(result: &CheckResult, inputs: InputsJson) -> Result<Envelope<
         schema_version: 1,
         prover_version: env!("CARGO_PKG_VERSION"),
         check: "boundary",
-        scope: Some(scope_json(scope)),
+        coverage: Some(coverage_json(coverage)),
         result: result_name,
         exit_code,
         inputs,
@@ -357,16 +368,36 @@ fn result_envelope(result: &CheckResult, inputs: InputsJson) -> Result<Envelope<
     })
 }
 
-fn scope_json(scope: &CheckScope) -> 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<CounterexampleJson<'_>, 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<Counterexample
             ancestor_binary,
             binary_identity_required,
             host,
+            destination_ip,
+            trusted_gateway,
             port,
             protocol,
             method,
@@ -386,6 +419,8 @@ fn counterexample_json(counterexample: &Counterexample) -> Result<Counterexample
             ancestor_binary: ancestor_binary.as_deref(),
             binary_identity_required: *binary_identity_required,
             host,
+            destination_ip: destination_ip.to_string(),
+            trusted_gateway: *trusted_gateway,
             port: *port,
             protocol: protocol.as_str(),
             method: method.as_deref(),
@@ -412,18 +447,14 @@ fn render(output: OutputFormat, envelope: &Envelope<'_>) -> 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 {

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(),

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