A Path-Based Network Policy Language

Network policies are traffic regulations for the networks which make up the Internet. These are necessary for managing the flow of data, for access control to the network, and for managing the network to achieve other types of quality of service goals. However, with the myriad of different policies and networks, all with varying needs, conflicts can arise between network policies. Detecting and correcting these conflicts can be quite difficult for human administrators. Thus, there is a need for a theoretically sound method for specifying policy and for automatically detecting policy conflicts. This dissertation presents a path-based policy language that is more comprehensive than earlier languages for describing network policy. The Path-based Policy Language PPL is a formal language for constructing models of Internet service and access control. This path-based language is extensible and allows for an unambiguous representation of network policies based on both the static and dynamic attributes of todays networks. To support this language, both a compiler and policy conflict tester were developed. These tools accept network policies specified in PPL, translate them into formal logic, and using a theorem prover to test for policy conflicts. PPL allows for the efficient representation of large networks with its abbreviated path format. This path format allows multiple paths to be represented with one statement.