A key issue in network security management is how to define a formal security policy. A good policy specification should be easy to get right and relatively stable, even in a dynamically changing network. Much work has been done in automating network security management. But the policy languages used are usually operational and do not explicitly express the underlying security goal.

We propose an approach where policy is defined as statements of desired security properties, whose compliance can be checked automatically by analyzing the configuration of the network. We use a simple policy model, the data access- control list (DACL) to demonstrate this idea. We present a framework and corresponding algorithms for checking that low-level configurations altogether uphold the high-level DACL policy, taking into consideration potential software vulnerabilities.