Free Trial

Safari Books Online is a digital library providing on-demand subscription access to thousands of learning resources.

CHAPTER 24 Formal Analysis of Policy-Based Security Configurations in Enterprise Networks 623 interpolicy shadowing exists if the following con- dition is true: Equation 24-9 u d u d (S discard ¬S discard ) (S protect ¬S protect ) = false. This expression represents the filtering condition that results in shadowing some traffic by D u . The first term represents the traffic discarded by D u but permitted by D d , whereas the second term represents the traffic that requires protection by D u but is not protected by D d . In this case, SA negotiation fails and the traffic is discarded at the upstream device. Rule 2 in SG A and rule 2 in SG B show an example of interpolicy shadow- ing. Shadowing is considered a conflict because it prevents the traffic desired by some nodes from flowing to the end destination. Interpolicy Spuriousness. Traffic is spurious if the upstream policy S u permits some traffic blocked by the downstream policy S d . Formally, that do not satisfy one of the conflict conditions are combinations where the upstream device and the downstream device perform the same action. To discover these conflicts, we construct the BDD for each of the conflict conditions defined above. On using the upstream outbound access pol- icy and the downstream inbound access policy. 2 Each rule in the upstream policy is checked if it intersects with any of the conflict conditions. If an intersection is found, we look for the corre- sponding rule in the downstream policy. Again, we match every rule in the downstream pol- icy against the conflict condition until we find an intersecting rule. If the downstream rule also matches the upstream rule, then the discovered conflict is reported along with the involved rules. Interpolicy Overlapping-Session Conflicts. IPSec allows applying nested sessions on the same traffic at different points on the traffic path to multiple remote peers. Similar to the intrapol-