Network Configuration Management via Model Finding
Network Configuration Management via Model Finding
复制标题
通过模型查找进行网络配置管理
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
S. Narain
中科院分区：
文献类型：
--
作者：
S. Narain
复杂的端到端网络服务是通过配置方法建立的：每个组件都有有限数量的配置参数，每个配置参数都被设置为一个确定的值。端到端的网络服务需求可以是连通性、安全性、性能和容错性。然而，在端到端需求和详细的组件配置之间存在很大的概念差距。为了弥补这一差距，创建了许多附属需求，例如，要使用的协议，以及要在不同协议层上设置的逻辑结构和相关策略。
Complex, end-to-end network services are set up via the configuration method: each component has a finite number of configuration parameters each of which is set to a definite value. End-to-end network service requirements can be on connectivity, security, performance and fault-tolerance. 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 and total cost of ownership. This paper shows how to formalize and automate such reasoning using a new logical system called Alloy.
Alloy is based on the concept of model finding. Given a first-order logic formula and a domain of interpretation, Alloy tries to find whether the formula is satisfiable in that domain, i.e., whether it has a model. Alloy is used to build a Requirement Solver that takes as input a set of network components and requirements upon their configurations and determines component configurations satisfying those requirements.
This Solver is used in different ways to accomplish the above reasoning tasks. The Solver is illustrated in depth by carrying out a variety of these tasks in the context of a realistic fault-tolerant virtual private network with remote access. Alloy uses modern satisfiability solvers that solve millions of constraints in millions of variables in seconds. However, poor requirements can easily nullify such speeds. The paper outlines approaches for writing efficient requirements. Finally, it outlines directions for future research.