Build a Z3 expression for whether data can be exfiltrated via this path.
(&self, bpath: &str, eid: &EndpointId)
| 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 { |
| 330 | let ek = eid.key(); |
| 331 | let access_key = format!("{bpath}:{ek}"); |
| 332 | |
| 333 | let has_access = match self.policy_allows.get(&access_key) { |
| 334 | Some(v) => v.clone(), |
| 335 | None => return Self::false_val(), |
| 336 | }; |
| 337 | |
| 338 | let exfil = self |
| 339 | .binary_can_exfil |
| 340 | .get(bpath) |
| 341 | .cloned() |
| 342 | .unwrap_or_else(Self::false_val); |
| 343 | let bypass = self |
| 344 | .binary_bypasses_l7 |
| 345 | .get(bpath) |
| 346 | .cloned() |
| 347 | .unwrap_or_else(Self::false_val); |
| 348 | let l7_enforced = self |
| 349 | .l7_enforced |
| 350 | .get(&ek) |
| 351 | .cloned() |
| 352 | .unwrap_or_else(Self::false_val); |
| 353 | let l7_write = self |
| 354 | .l7_allows_write |
| 355 | .get(&ek) |
| 356 | .cloned() |
| 357 | .unwrap_or_else(Self::false_val); |
| 358 | let http = self |
| 359 | .binary_can_construct_http |
| 360 | .get(bpath) |
| 361 | .cloned() |
| 362 | .unwrap_or_else(Self::false_val); |
| 363 | |
| 364 | Bool::and(&[ |
| 365 | has_access, |
| 366 | exfil, |
| 367 | Bool::or(&[ |
| 368 | Bool::and(&[!l7_enforced, http.clone()]), |
| 369 | Bool::and(&[l7_write, http]), |
| 370 | bypass, |
| 371 | ]), |
| 372 | ]) |
| 373 | } |
| 374 | |
| 375 | /// Check satisfiability of an expression against the base constraints. |
| 376 | pub fn check_sat(&self, expr: &Bool) -> SatResult { |
no test coverage detected