Build a Z3 expression for whether a binary can write to an endpoint.
(&self, bpath: &str, eid: &EndpointId)
| 283 | |
| 284 | /// Build a Z3 expression for whether a binary can write to an endpoint. |
| 285 | pub fn can_write_to_endpoint(&self, bpath: &str, eid: &EndpointId) -> Bool { |
| 286 | let ek = eid.key(); |
| 287 | let access_key = format!("{bpath}:{ek}"); |
| 288 | |
| 289 | let has_access = match self.policy_allows.get(&access_key) { |
| 290 | Some(v) => v.clone(), |
| 291 | None => return Self::false_val(), |
| 292 | }; |
| 293 | |
| 294 | let bypass = self |
| 295 | .binary_bypasses_l7 |
| 296 | .get(bpath) |
| 297 | .cloned() |
| 298 | .unwrap_or_else(Self::false_val); |
| 299 | let l7_enforced = self |
| 300 | .l7_enforced |
| 301 | .get(&ek) |
| 302 | .cloned() |
| 303 | .unwrap_or_else(Self::false_val); |
| 304 | let l7_write = self |
| 305 | .l7_allows_write |
| 306 | .get(&ek) |
| 307 | .cloned() |
| 308 | .unwrap_or_else(Self::false_val); |
| 309 | let binary_write = self |
| 310 | .binary_can_write |
| 311 | .get(bpath) |
| 312 | .cloned() |
| 313 | .unwrap_or_else(Self::false_val); |
| 314 | let cred_write = self |
| 315 | .credential_has_write |
| 316 | .get(&eid.host) |
| 317 | .cloned() |
| 318 | .unwrap_or_else(Self::false_val); |
| 319 | |
| 320 | Bool::and(&[ |
| 321 | has_access, |
| 322 | binary_write, |
| 323 | Bool::or(&[!l7_enforced, l7_write, bypass]), |
| 324 | cred_write, |
| 325 | ]) |
| 326 | } |
| 327 | |
| 328 | /// Build a Z3 expression for whether data can be exfiltrated via this path. |
| 329 | pub fn can_exfil_via_endpoint(&self, bpath: &str, eid: &EndpointId) -> Bool { |