fix(prover): distinguish sibling endpoints and fail closed on solver errors

crates/openshell-prover/README.md

@@ -186,6 +186,12 @@ not form part of the authored policy schema.
 
 See `src/model.rs`. Briefly:
 
+- Endpoint facts are indexed by rule, endpoint position, and effective port.
+  Sibling endpoints retain their own grants even when their destinations overlap.
+- Query entrypoints return an error if the base constraints are inconsistent or
+  the solver cannot reach a conclusion. Callers must propagate that error; it
+  cannot be accepted as a finding or compared as an empty finding list.
+
 - Bool sorts per `(binary, endpoint)` pair encode policy reachability,
   filtered by binary capability flags (`can_exfiltrate`,
   `bypasses_l7`).

crates/openshell-prover/src/lib.rs

@@ -31,7 +31,7 @@ use report::{render_compact, render_report};
 ///
 /// - `Ok(0)` — pass (no findings, or all accepted)
 /// - `Ok(1)` — fail (one or more unaccepted findings present)
-/// - `Err(_)` — input or registry loading error
+/// - `Err(_)` — input, registry, or solver error
 ///
 /// Binary and API capability registries are embedded at compile time.
 /// Pass `registry_dir` to override with a custom filesystem registry.
@@ -59,7 +59,7 @@ pub fn prove(
     };
 
     let z3_model = build_model(policy, credential_set, binary_registry);
-    let mut findings = run_all_queries(&z3_model);
+    let mut findings = run_all_queries(&z3_model)?;
 
     if let Some(ar_path) = accepted_risks_path {
         let accepted = load_accepted_risks(Path::new(ar_path))?;
@@ -223,7 +223,7 @@ filesystem_policy:
         let bin_reg = registry::load_embedded_binary_registry().expect("load registry");
 
         let z3_model = build_model(pol, cred_set, bin_reg);
-        let findings = run_all_queries(&z3_model);
+        let findings = run_all_queries(&z3_model).expect("run queries");
 
         let categories: std::collections::HashSet<&str> =
             findings.iter().map(|f| f.query.as_str()).collect();
@@ -276,7 +276,7 @@ network_policies:
         let bin_reg = registry::load_embedded_binary_registry().expect("load registry");
 
         let z3_model = build_model(policy, cred_set, bin_reg);
-        let findings = run_all_queries(&z3_model);
+        let findings = run_all_queries(&z3_model).expect("run queries");
 
         let reach = findings
             .iter()
@@ -310,7 +310,7 @@ network_policies:
         let bin_reg = registry::load_embedded_binary_registry().expect("load registry");
 
         let z3_model = build_model(policy, credentials::CredentialSet::default(), bin_reg);
-        let findings = run_all_queries(&z3_model);
+        let findings = run_all_queries(&z3_model).expect("run queries");
 
         let link_local = findings
             .iter()
@@ -323,7 +323,104 @@ network_policies:
         )));
     }
 
-    // 7. Empty policy produces no findings.
+    #[test]
+    fn sibling_endpoints_preserve_findings_and_method_identity() {
+        use finding::{FindingPath, category};
+
+        // Exercise both conflicting write facts and agreeing write facts with
+        // different methods, in either endpoint order and on overlapping ports.
+        for (first_method, second_method) in [("GET", "*"), ("POST", "DELETE")] {
+            for reverse in [false, true] {
+                let mut policy = policy::parse_policy_str(&format!(
+                    r#"
+version: 1
+network_policies:
+  github:
+    endpoints:
+      - host: api.github.com
+        ports: [443, 8443]
+        protocol: rest
+        rules:
+          - allow: {{method: "{first_method}", path: "/**"}}
+      - host: api.github.com
+        port: 443
+        protocol: rest
+        rules:
+          - allow: {{method: "{second_method}", path: "/**"}}
+    binaries:
+      - path: /usr/bin/curl
+  metadata:
+    endpoints:
+      - host: 169.254.169.254
+        port: 80
+    binaries:
+      - path: /usr/bin/curl
+"#
+                ))
+                .unwrap();
+                if reverse {
+                    policy
+                        .network_policies
+                        .get_mut("github")
+                        .unwrap()
+                        .endpoints
+                        .reverse();
+                }
+                let credentials = credentials::load_credential_set_embedded(
+                    &testdata_dir().join("credentials.yaml"),
+                )
+                .unwrap();
+                let registry = registry::load_embedded_binary_registry().unwrap();
+                let model = build_model(policy, credentials, registry);
+                let findings = run_all_queries(&model).unwrap();
+                assert!(
+                    findings
+                        .iter()
+                        .any(|f| f.query == category::LINK_LOCAL_REACH)
+                );
+                assert!(
+                    findings
+                        .iter()
+                        .any(|f| f.query == category::CREDENTIAL_REACH_EXPANSION)
+                );
+                let methods = &findings
+                    .iter()
+                    .find(|f| f.query == category::CAPABILITY_EXPANSION)
+                    .unwrap()
+                    .paths;
+                assert!(methods.iter().any(|p| matches!(p, FindingPath::Exfil(p) if p.method == "DELETE" && p.endpoint_port == 443)));
+                assert!(!methods.iter().any(|p| matches!(p, FindingPath::Exfil(p) if p.method == "DELETE" && p.endpoint_port == 8443)));
+            }
+        }
+    }
+
+    #[test]
+    fn sibling_l4_and_l7_endpoints_preserve_reach() {
+        let policy = policy::parse_policy_str(
+            r"
+version: 1
+network_policies:
+  metadata:
+    endpoints:
+      - host: 169.254.169.254
+        port: 80
+        protocol: rest
+        access: read-only
+      - host: 169.254.169.254
+        port: 80
+    binaries:
+      - path: /usr/bin/curl
+",
+        )
+        .unwrap();
+        let registry = registry::load_embedded_binary_registry().unwrap();
+        let model = build_model(policy, credentials::CredentialSet::default(), registry);
+        let findings = run_all_queries(&model).unwrap();
+        assert_eq!(findings.len(), 1);
+        assert_eq!(findings[0].query, finding::category::LINK_LOCAL_REACH);
+    }
+
+    // Empty policy produces no findings.
     #[test]
     fn test_empty_policy_no_findings() {
         let policy_path = testdata_dir().join("empty-policy.yaml");
@@ -334,7 +431,7 @@ network_policies:
         let bin_reg = registry::load_embedded_binary_registry().expect("load registry");
 
         let z3_model = build_model(pol, cred_set, bin_reg);
-        let findings = run_all_queries(&z3_model);
+        let findings = run_all_queries(&z3_model).expect("run queries");
 
         assert!(
             findings.is_empty(),

crates/openshell-prover/src/model.rs

@@ -16,14 +16,23 @@ use crate::registry::BinaryRegistry;
 #[derive(Debug, Clone, Hash, PartialEq, Eq)]
 pub struct EndpointId {
     pub policy_name: String,
+    /// Position within the policy rule's endpoint list.
+    pub endpoint_index: usize,
     pub host: String,
     pub port: u16,
 }
 
 impl EndpointId {
     /// Stable string key used for Z3 variable naming.
     pub fn key(&self) -> String {
-        format!("{}:{}:{}", self.policy_name, self.host, self.port)
+        // Length-prefix the authored name so delimiters cannot alias another rule.
+        format!(
+            "{}:{}:{}:{}",
+            self.policy_name.len(),
+            self.policy_name,
+            self.endpoint_index,
+            self.port
+        )
     }
 }
 
@@ -97,10 +106,11 @@ impl ReachabilityModel {
 
     fn index_endpoints(&mut self) {
         for (policy_name, rule) in &self.policy.network_policies {
-            for ep in &rule.endpoints {
+            for (endpoint_index, ep) in rule.endpoints.iter().enumerate() {
                 for port in ep.effective_ports() {
                     self.endpoints.push(EndpointId {
                         policy_name: policy_name.clone(),
+                        endpoint_index,
                         host: ep.host.clone(),
                         port,
                     });
@@ -122,15 +132,16 @@ impl ReachabilityModel {
 
     fn encode_policy_allows(&mut self) {
         for (policy_name, rule) in &self.policy.network_policies {
-            for ep in &rule.endpoints {
+            for (endpoint_index, ep) in rule.endpoints.iter().enumerate() {
                 for port in ep.effective_ports() {
                     let eid = EndpointId {
                         policy_name: policy_name.clone(),
+                        endpoint_index,
                         host: ep.host.clone(),
                         port,
                     };
                     for b in &rule.binaries {
-                        let key = format!("{}:{}", b.path, eid.key());
+                        let key = format!("{}:{}:{}", b.path.len(), b.path, eid.key());
                         let var = Bool::new_const(format!("policy_allows_{key}"));
                         self.solver.assert(&var);
                         self.policy_allows.insert(key, var);
@@ -142,10 +153,11 @@ impl ReachabilityModel {
 
     fn encode_l7_enforcement(&mut self) {
         for (policy_name, rule) in &self.policy.network_policies {
-            for ep in &rule.endpoints {
+            for (endpoint_index, ep) in rule.endpoints.iter().enumerate() {
                 for port in ep.effective_ports() {
                     let eid = EndpointId {
                         policy_name: policy_name.clone(),
+                        endpoint_index,
                         host: ep.host.clone(),
                         port,
                     };
@@ -284,7 +296,7 @@ impl ReachabilityModel {
     /// Build a Z3 expression for whether a binary can write to an endpoint.
     pub fn can_write_to_endpoint(&self, bpath: &str, eid: &EndpointId) -> Bool {
         let ek = eid.key();
-        let access_key = format!("{bpath}:{ek}");
+        let access_key = format!("{}:{bpath}:{ek}", bpath.len());
 
         let has_access = match self.policy_allows.get(&access_key) {
             Some(v) => v.clone(),
@@ -328,7 +340,7 @@ impl ReachabilityModel {
     /// Build a Z3 expression for whether data can be exfiltrated via this path.
     pub fn can_exfil_via_endpoint(&self, bpath: &str, eid: &EndpointId) -> Bool {
         let ek = eid.key();
-        let access_key = format!("{bpath}:{ek}");
+        let access_key = format!("{}:{bpath}:{ek}", bpath.len());
 
         let has_access = match self.policy_allows.get(&access_key) {
             Some(v) => v.clone(),
@@ -372,6 +384,15 @@ impl ReachabilityModel {
         ])
     }
 
+    /// Reject inconsistent or inconclusive base constraints before querying them.
+    pub fn validate(&self) -> miette::Result<()> {
+        match self.solver.check() {
+            SatResult::Sat => Ok(()),
+            SatResult::Unsat => miette::bail!("inconsistent reachability model"),
+            SatResult::Unknown => miette::bail!("reachability model validation inconclusive"),
+        }
+    }
+
     /// Check satisfiability of an expression against the base constraints.
     pub fn check_sat(&self, expr: &Bool) -> SatResult {
         self.solver.push();
@@ -392,3 +413,52 @@ pub fn build_model(
     let _ctx = Context::thread_local();
     ReachabilityModel::new(policy, credentials, binary_registry)
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::queries::{check_credential_safety, run_all_queries};
+
+    #[test]
+    fn inconsistent_base_model_is_an_error_even_without_query_paths() {
+        let model = build_model(
+            PolicyModel::default(),
+            CredentialSet::default(),
+            crate::registry::load_embedded_binary_registry().unwrap(),
+        );
+        model.solver.assert(Bool::from_bool(false));
+        assert!(check_credential_safety(&model).is_err());
+        assert!(run_all_queries(&model).is_err());
+    }
+
+    #[test]
+    fn inconclusive_base_model_is_an_error() {
+        let model = build_model(
+            PolicyModel::default(),
+            CredentialSet::default(),
+            crate::registry::load_embedded_binary_registry().unwrap(),
+        );
+        model.solver.assert(Bool::new_const("resource_limited"));
+        let mut params = z3::Params::new();
+        params.set_u32("rlimit", 1);
+        model.solver.set_params(&params);
+        assert_eq!(model.solver.check(), SatResult::Unknown);
+        assert!(run_all_queries(&model).is_err());
+    }
+
+    #[test]
+    fn endpoint_keys_distinguish_rule_names_with_delimiters() {
+        let left = EndpointId {
+            policy_name: "rule:2001".to_string(),
+            endpoint_index: 0,
+            host: "db8::1".to_string(),
+            port: 443,
+        };
+        let right = EndpointId {
+            policy_name: "rule".to_string(),
+            host: "2001:db8::1".to_string(),
+            ..left
+        };
+        assert_ne!(left.key(), right.key());
+    }
+}