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; 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(); 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.