Network Configuration Management via Model Finding
Sanjai Narain, Telcordia Technologies, Inc.
narain@research.telcordia.com

Complex, end-to-end network services are set up via the configuration
method.  However, there is a large conceptual gap between end-to-end
requirements and detailed component configurations. To bridge this
gap, a number of subsidiary requirements are created that constrain,
for example, the protocols to be used, and the logical structures and
associated policies to be set up at different protocol layers. By
performing different types of reasoning with these requirements,
different configuration tasks are accomplished. These include
configuration synthesis, configuration error diagnosis, configuration
error fixing, reconfiguration as requirements or components are added
and deleted, and requirement verification. However, such reasoning is
currently ad hoc. Network requirements are not even precisely
specified hence automation of reasoning is impossible. This is a major
reason for the high cost of network management.  This paper shows how
to formalize and automate such reasoning using Alloy, in the context
of a realistic fault-tolerant virtual private network. While modern
satisfiability solvers that Alloy uses are highly efficient, poor
specifications can easily nullify their speeds. The paper outlines
approaches for writing efficient requirements. Finally, it outlines
directions for future research.