(&mut self)
| 141 | } |
| 142 | |
| 143 | fn encode_l7_enforcement(&mut self) { |
| 144 | for (policy_name, rule) in &self.policy.network_policies { |
| 145 | for ep in &rule.endpoints { |
| 146 | for port in ep.effective_ports() { |
| 147 | let eid = EndpointId { |
| 148 | policy_name: policy_name.clone(), |
| 149 | host: ep.host.clone(), |
| 150 | port, |
| 151 | }; |
| 152 | let ek = eid.key(); |
| 153 | |
| 154 | // L7 enforced? |
| 155 | let l7_var = Bool::new_const(format!("l7_enforced_{ek}")); |
| 156 | if ep.is_l7_enforced() { |
| 157 | self.solver.assert(&l7_var); |
| 158 | } else { |
| 159 | self.solver.assert(&!l7_var.clone()); |
| 160 | } |
| 161 | self.l7_enforced.insert(ek.clone(), l7_var); |
| 162 | |
| 163 | // L7 allows write? |
| 164 | let allowed = ep.allowed_methods(); |
| 165 | let write_set: HashSet<&str> = WRITE_METHODS.iter().copied().collect(); |
| 166 | let has_write = if allowed.is_empty() { |
| 167 | true // L4-only: all methods pass |
| 168 | } else { |
| 169 | allowed.iter().any(|m| write_set.contains(m.as_str())) |
| 170 | }; |
| 171 | |
| 172 | let l7_write_var = Bool::new_const(format!("l7_allows_write_{ek}")); |
| 173 | if ep.is_l7_enforced() { |
| 174 | if has_write { |
| 175 | self.solver.assert(&l7_write_var); |
| 176 | } else { |
| 177 | self.solver.assert(&!l7_write_var.clone()); |
| 178 | } |
| 179 | } else { |
| 180 | // L4-only: all methods pass through |
| 181 | self.solver.assert(&l7_write_var); |
| 182 | } |
| 183 | self.l7_allows_write.insert(ek, l7_write_var); |
| 184 | } |
| 185 | } |
| 186 | } |
| 187 | } |
| 188 | |
| 189 | fn encode_binary_capabilities(&mut self) { |
| 190 | for bpath in &self.binary_paths.clone() { |
no test coverage detected