Incremental verification of computing policies

Abstract

A computing policy is a sequence of rules, where each rule consists of a predicate and an action, which can be either “accept” or “reject”. A policy P is said to accept (or reject, respectively) a request iff the action of the first rule in P, whose predicate matches the request, is “accept” (or “reject”, respectively). An accept (or reject, respectively) property of a policy P is a set of requests that should be accepted (or rejected, respectively) by P. Policy P is said to satisfy an accept (or reject, respectively) property pp iff every request that is specified by property pp is accepted (or rejected, respectively) by policy P. In this paper, we outline efficient methods for verifying whether any given policy P satisfies any given property pp, provided that policy P results from changing only one rule in another policy that is known to satisfy property pp.