Firewall policy management is challenging and error-prone. While ample research has led to tools for policy specification, correctness analysis, and optimization, few researchers have paid attention to firewall policy deployment: the process where a management tool edits a firewall's configuration to make it run the policies specified in the tool. In this paper, we provide the first formal definition and theoretical analysis of safety in firewall policy deployment. We show that naive deployment approaches can easily create a temporary security hole by permitting illegal traffic, or interrupt service by rejecting legal traffic during the deployment. We define safe and most-efficient deployments, and introduce the shuffling theorem as a formal basis for constructing deployment algorithms and proving their safety. We present efficient algorithms for constructing most-efficient deployments in popular policy editing languages. We show that in certain widely- installed policy editing languages, a safe deployment is not always possible. We also show how to leverage existing diff algorithms to guarantee a safe, most- efficient, and monotonic deployment in other editing languages.

This paper introduces the PeerAccess framework for reasoning about authorization in open distributed systems, and shows how a parameterization of the framework can be used to reason about access to computational resources in a grid environment. The PeerAccess framework supports a declarative description of the behavior of peers that selectively push and/or pull information from certain other peers. PeerAccess local knowledge bases encode the basic knowledge of each peer (e.g., Alice's group memberships), its policies governing the release of each possible piece of information to other peers, and information that guides and limits its search process when trying to obtain particular pieces of information from other peers. PeerAccess proofs of authorization are verifiable and nonrepudiable, and their construction relies only on the local information possessed by peers and their parameterized behavior with respect to query answering, information push/pull, and information release policies (i.e., no omniscient viewpoint is required). We present the PeerAccess language and peer knowledge base structure, the associated formal semantics and proof theory, and examples of the use of PeerAccess in constructing proofs of authorization to access computational resources.