Problem Statement
PR #822 adds L7 deny rules to the network policy schema, enabling the allow-everything-except pattern. Deny rules take precedence over allow rules.
The policy prover does not yet understand deny rules. Its policy parser, Z3 constraint model, and verification queries all operate on the allow-rule-only schema. Without this update, the prover will overestimate reachability -- reporting exfiltration or write-bypass paths through endpoints where deny rules would actually block the request at runtime.
Proposed Design
policy.rs: Parse deny_rules from endpoint definitions. Each deny rule has the same shape as an allow rule: method, path, query, command.
model.rs: For each endpoint, encode deny rules as negative constraints on l7_allows_write. If all write methods are covered by deny rules, the endpoint should be treated as write-blocked even if allow rules or access: full would otherwise permit them.
queries.rs: No structural changes expected. The exfiltration and write-bypass queries already check l7_allows_write -- the fix is in the model encoding.
Agent Investigation
- crates/openshell-prover/src/policy.rs parses endpoint fields including rules and access but does not yet handle deny_rules
- crates/openshell-prover/src/model.rs encodes l7_allows_write based on allowed_methods() -- primary place to incorporate deny rule exclusions
- PR #822 adds deny_rules to NetworkEndpointDef in crates/openshell-policy/src/lib.rs
Related: #565, #699, PR #741, PR #822
Problem Statement
PR #822 adds L7 deny rules to the network policy schema, enabling the allow-everything-except pattern. Deny rules take precedence over allow rules.
The policy prover does not yet understand deny rules. Its policy parser, Z3 constraint model, and verification queries all operate on the allow-rule-only schema. Without this update, the prover will overestimate reachability -- reporting exfiltration or write-bypass paths through endpoints where deny rules would actually block the request at runtime.
Proposed Design
policy.rs: Parse deny_rules from endpoint definitions. Each deny rule has the same shape as an allow rule: method, path, query, command.
model.rs: For each endpoint, encode deny rules as negative constraints on l7_allows_write. If all write methods are covered by deny rules, the endpoint should be treated as write-blocked even if allow rules or access: full would otherwise permit them.
queries.rs: No structural changes expected. The exfiltration and write-bypass queries already check l7_allows_write -- the fix is in the model encoding.
Agent Investigation
Related: #565, #699, PR #741, PR #822