From 27d24f0ab362eac2e8b70779f11f45fe66ec1da0 Mon Sep 17 00:00:00 2001 From: Evie Howard Date: Wed, 22 Jul 2026 12:48:26 +0100 Subject: [PATCH 1/3] refactor(prover): remove legacy unused reachability constraints Remove can_write_to_endpoint() and the solver variables and encoding methods that exist solely to support it. No active query calls this method; confirmed zero callers across the monorepo. Crate is not published externally, so no public API concern. Removed as root cause: - can_write_to_endpoint(): zero callers in the codebase Removed as direct consumers of can_write_to_endpoint(): - binary_can_write: only read inside can_write_to_endpoint() - credential_has_write: only read inside can_write_to_endpoint() Removed as directly dead (no query ever read them): - credential_has_destructive: flagged by compiler, silenced with #[allow(dead_code)] rather than removed - filesystem_readable: flagged by compiler, silenced with #[allow(dead_code)] rather than removed Removed as now-empty encoding methods: - encode_credentials(): exclusively populated credential_has_write and credential_has_destructive - encode_filesystem(): exclusively populated filesystem_readable Also removed two #[allow(dead_code)] allowances and the corresponding HashMap::new() initialisers and build() call sites. Active query behavior is unchanged. All existing prover tests pass without modification and cover all four finding categories end-to-end. No new tests added as they would duplicate existing coverage exactly. Note: removing encode_credentials() leaves write_actions_for_scopes() and destructive_actions_for_scopes() in credentials.rs with no callers. Left as a follow-up outside the scope of this change. Closes #2412 Signed-off-by: Evie Howard --- crates/openshell-prover/src/model.rs | 114 --------------------------- 1 file changed, 114 deletions(-) diff --git a/crates/openshell-prover/src/model.rs b/crates/openshell-prover/src/model.rs index bf52993d47..21d42bc82e 100644 --- a/crates/openshell-prover/src/model.rs +++ b/crates/openshell-prover/src/model.rs @@ -45,14 +45,8 @@ pub struct ReachabilityModel { l7_enforced: HashMap, l7_allows_write: HashMap, binary_bypasses_l7: HashMap, - binary_can_write: HashMap, binary_can_exfil: HashMap, binary_can_construct_http: HashMap, - credential_has_write: HashMap, - #[allow(dead_code)] - credential_has_destructive: HashMap, - #[allow(dead_code)] - filesystem_readable: HashMap, } impl ReachabilityModel { @@ -74,12 +68,8 @@ impl ReachabilityModel { l7_enforced: HashMap::new(), l7_allows_write: HashMap::new(), binary_bypasses_l7: HashMap::new(), - binary_can_write: HashMap::new(), binary_can_exfil: HashMap::new(), binary_can_construct_http: HashMap::new(), - credential_has_write: HashMap::new(), - credential_has_destructive: HashMap::new(), - filesystem_readable: HashMap::new(), }; model.build(); model @@ -91,8 +81,6 @@ impl ReachabilityModel { self.encode_policy_allows(); self.encode_l7_enforcement(); self.encode_binary_capabilities(); - self.encode_credentials(); - self.encode_filesystem(); } fn index_endpoints(&mut self) { @@ -198,14 +186,6 @@ impl ReachabilityModel { } self.binary_bypasses_l7.insert(bpath.clone(), bypass_var); - let write_var = Bool::new_const(format!("binary_can_write_{bpath}")); - if cap.can_write() { - self.solver.assert(&write_var); - } else { - self.solver.assert(&!write_var.clone()); - } - self.binary_can_write.insert(bpath.clone(), write_var); - let exfil_var = Bool::new_const(format!("binary_can_exfil_{bpath}")); if cap.can_exfiltrate { self.solver.assert(&exfil_var); @@ -225,106 +205,12 @@ impl ReachabilityModel { } } - fn encode_credentials(&mut self) { - let hosts: HashSet = self.endpoints.iter().map(|e| e.host.clone()).collect(); - - for host in &hosts { - let creds = self.credentials.credentials_for_host(host); - let api = self.credentials.api_for_host(host); - - let mut has_write = false; - let mut has_destructive = false; - - for cred in &creds { - if let Some(api) = api { - if !api.write_actions_for_scopes(&cred.scopes).is_empty() { - has_write = true; - } - if !api.destructive_actions_for_scopes(&cred.scopes).is_empty() { - has_destructive = true; - } - } else if !cred.scopes.is_empty() { - has_write = true; - } - } - - let cw_var = Bool::new_const(format!("credential_has_write_{host}")); - if has_write { - self.solver.assert(&cw_var); - } else { - self.solver.assert(&!cw_var.clone()); - } - self.credential_has_write.insert(host.clone(), cw_var); - - let destructive_var = Bool::new_const(format!("credential_has_destructive_{host}")); - if has_destructive { - self.solver.assert(&destructive_var); - } else { - self.solver.assert(&!destructive_var.clone()); - } - self.credential_has_destructive - .insert(host.clone(), destructive_var); - } - } - - fn encode_filesystem(&mut self) { - for path in self.policy.filesystem_policy.readable_paths() { - let var = Bool::new_const(format!("fs_readable_{path}")); - self.solver.assert(&var); - self.filesystem_readable.insert(path, var); - } - } - // --- Query helpers --- fn false_val() -> Bool { Bool::from_bool(false) } - /// 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 has_access = match self.policy_allows.get(&access_key) { - Some(v) => v.clone(), - None => return Self::false_val(), - }; - - let bypass = self - .binary_bypasses_l7 - .get(bpath) - .cloned() - .unwrap_or_else(Self::false_val); - let l7_enforced = self - .l7_enforced - .get(&ek) - .cloned() - .unwrap_or_else(Self::false_val); - let l7_write = self - .l7_allows_write - .get(&ek) - .cloned() - .unwrap_or_else(Self::false_val); - let binary_write = self - .binary_can_write - .get(bpath) - .cloned() - .unwrap_or_else(Self::false_val); - let cred_write = self - .credential_has_write - .get(&eid.host) - .cloned() - .unwrap_or_else(Self::false_val); - - Bool::and(&[ - has_access, - binary_write, - Bool::or(&[!l7_enforced, l7_write, bypass]), - cred_write, - ]) - } - /// 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(); From 4873bbcb88889381eae156a7370e63492993fce7 Mon Sep 17 00:00:00 2001 From: Evie Howard Date: Wed, 22 Jul 2026 16:39:44 +0100 Subject: [PATCH 2/3] refactor(prover): remove dead write-capability helpers from binary registry BinaryProtocol::can_write(), BinaryCapability::can_write(), and write_mechanisms() lost their only callers when can_write_to_endpoint() and its supporting model fields were removed. Delete the now-dead methods. write_mechanisms() had no callers prior to this series; the two can_write() methods were made dead by the preceding model.rs cleanup. Signed-off-by: Evie Howard --- crates/openshell-prover/src/registry.rs | 32 ------------------------- 1 file changed, 32 deletions(-) diff --git a/crates/openshell-prover/src/registry.rs b/crates/openshell-prover/src/registry.rs index 63a3fce3bc..f7f7c0dd11 100644 --- a/crates/openshell-prover/src/registry.rs +++ b/crates/openshell-prover/src/registry.rs @@ -100,15 +100,6 @@ pub struct BinaryProtocol { pub actions: Vec, } -impl BinaryProtocol { - /// Whether any action in this protocol is a write or destructive action. - pub fn can_write(&self) -> bool { - self.actions - .iter() - .any(|a| matches!(a.action_type, ActionType::Write | ActionType::Destructive)) - } -} - /// Capability descriptor for a single binary. #[derive(Debug, Clone)] pub struct BinaryCapability { @@ -126,29 +117,6 @@ impl BinaryCapability { pub fn bypasses_l7(&self) -> bool { self.protocols.iter().any(|p| p.bypasses_l7) } - - /// Whether the binary can perform write actions. - pub fn can_write(&self) -> bool { - self.protocols.iter().any(BinaryProtocol::can_write) || self.can_construct_http - } - - /// Short mechanisms by which this binary can write. - pub fn write_mechanisms(&self) -> Vec { - let mut mechanisms = Vec::new(); - for p in &self.protocols { - if p.can_write() { - for a in &p.actions { - if matches!(a.action_type, ActionType::Write | ActionType::Destructive) { - mechanisms.push(format!("{}: {}", p.name, a.name)); - } - } - } - } - if self.can_construct_http { - mechanisms.push("arbitrary HTTP request construction".to_owned()); - } - mechanisms - } } /// Registry of binary capability descriptors. From 0009e7cf783e80bf964a1d0a57574add2dbeb609 Mon Sep 17 00:00:00 2001 From: Evie Howard Date: Thu, 23 Jul 2026 09:15:48 +0100 Subject: [PATCH 3/3] docs(prover): remove stale write-bypass mention from module doc comment The module doc incorrectly listed write-bypass violation detection as a prover capability. The prover only checks reachability queries; write-bypass detection was never implemented. Signed-off-by: Evie Howard --- crates/openshell-prover/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/openshell-prover/src/lib.rs b/crates/openshell-prover/src/lib.rs index 0fb8757577..98379d1c95 100644 --- a/crates/openshell-prover/src/lib.rs +++ b/crates/openshell-prover/src/lib.rs @@ -5,7 +5,7 @@ //! //! Encodes sandbox policies, binary capabilities, and credential scopes as Z3 //! SMT constraints, then checks reachability queries to detect data exfiltration -//! paths and write-bypass violations. +//! paths. pub mod accepted_risks; pub mod credentials;