Configuration is the glue for logically integrating network components to satisfy end-to-end requirements on security and functionality. Every component has a finite number of configuration variables that are set to definite values. It is well-documented that configuration errors are responsible for 50%-80% of network vulnerabilities and downtime and it can take months to set up and adapt networks. This is because the large conceptual gap between requirement and configuration is manually bridged. This paper presents a Science of Configuration to automatically bridge this gap. It contains tools for requirement specification, configuration synthesis, repair, vendor-specific adaptation, visualization, emulation, verification, distributed configuration, in-band configuration, reconfiguration planning and moving-target defense. The Science leverages modern SMT solvers that can solve a million constraints in a million variables in seconds, and group communication protocols that provide total-ordering message delivery guarantees. The Science is motivated by the same problems that Software-Defined Networking is, but unlike SDN, exploits the full power of conventional networking devices that don’t separate the control and data planes. Applications of the Science are sketched to cyber defense exercises and network planning.
Configuration is the glue for logically integrating network components to satisfy end-to-end requirements on security and functionality. Every component has a finite number of configuration variables that are set to definite values. It is well-documented that configuration errors are responsible for 50%-80% of network vulnerabilities and downtime and it can take months to set up new networks or adapt them to changing requirements and state. This is because the large conceptual gap between requirements and configuration is manually bridged. Requirements induce complex dependencies or constraints between configurations within and across components at and across multiple protocols. The number of requirements, components, configuration variables and possible values is large, so the spaces over which one must search for a satisfying configuration are astronomical. Manual search through these spaces is infeasible.
This paper presents a Science of Configuration to automatically bridge the above gap. It leverages modern SMT solvers [10, 28] that can solve a million constraints in a million variables in seconds, and thus efficiently search through the above spaces. The Science also leverages group communication protocols that provide total-ordering message delivery guarantees [11, 9]. The Distributed Assured and Dynamic Configuration System is an implementation of this Science. In its simplest form a DADC system consists of a single controller as shown in Figure 1. DADC offers the following tools:
- Intuitive requirement specification language. This allows one to precisely specify requirements in about the same time it takes to visually depict these. It contains a catalog of fundamental logical structures and relationships at and across multiple protocol layers. These can be composed to specify a very large class of requirements. A visual version of this language is under development.
- Configuration synthesis. This computes configurations satisfying requirements and thus eliminates errors due to manual computation. Thus, it automates a central intellectual task that, currently, is manually accomplished.
- Configuration repair. This identifies configurations that are non-compliant with requirements and calculates the minimum-cost configuration changes to bring these into compliance.
- Vendor-specific adapters. These parse configuration files of components from different vendors into an abstract, vendor-neutral information model, generate these files from abstract configurations, and apply (download) files to components.
- Visualization. This provides a conceptual understanding of the network via visualizations of a large number of logical structures and relationships latent in the current configuration. It makes visible the presence or absence of structural defects.
- Emulation. This allows a network planner to evaluate complex architectural concepts in a Cisco or Linux network in minutes rather than the days or months it takes with physica`l networks. Emulation is not simulation. It reproduces the behavior of physical networks with perfect fidelity, except possibly for performance behavior.
- Verification. This evaluates the correctness of requirements and the inclusion and equivalence of access-control policies. This also evaluates the propagation of an adversary’s influence through a network with an algorithm for path finding in the presence of access-control lists and path constraints.
- Distributed configuration. This enforces global configuration consistency in the absence of a centralized configuration authority.
- In-band configuration. This removes the need to create an outof- band network for configuration management.
- Reconfiguration planning. This computes the order in which to reconfigure components without violating safety requirements during transition.
- Moving-target defense. This periodically changes network configuration in such a way that legitimate users continue to obtain service yet the adversary is confused about what configurations are new and old. This technique is called configurationspace randomization. Configuration is a network’s “DNA,” so its knowledge can allow an adversary to identify high-value targets such as single points of failure. Configuration-space randomization makes it harder for an adversary to gain such knowledge.
At present, DADC supports Cisco IOS and ASA, Linux, Juniper, Vyatta and Palo Alto for IP, IPv6 IPSec, RIP, OSPF, static routing, HSRP, VLAN, GRE, mGRE, QoS and access-control lists.
Section 2 illustrates the large gap between requirement and configuration and why it is hard to manually bridge. Section 3 sketches the design of DADC tools in the context of this example. Section 4 shows that the performance of DADC is adequate for networks of realistic size and complexity. Section 5 outlines applications of DADC to network planning and cyber defense exercises. Section 6 outlines the relationship of DADC to current work, especially, Software-Defined Networking. Section 7 contains an overview of SAT and SMT solvers and is followed by references.
2. The gap between requirement and configuration
Figure 2 shows a network architecture for securely transmitting information between hosts C1-C4. The architecture is inspired by the Commercial Solutions for Classified standard  permitting the use of commercial equipment and public networks for such transmission. The requirements that the network needs to satisfy are as follows:
- There are four enclaves
- Each enclave has a client, an inner gateway and an outer gateway
- In each enclave, inner and outer gateways are from different vendors
- Outer gateways are connected to the WAN router
- There is a full-mesh of IPSec tunnels between the inner gateways
- There is another full-mesh of IPSec tunnels between the outer gateways
- Static routes are used to forward all traffic from clients to inner gateways, from inner gateways to outer gateways, and from outer gateways to the WAN
- Dynamic (OSPF) routing is used in the WAN router
Even for this small example, it is quite hard for a human to translate the requirements into concrete configurations. He cannot choose values of configuration variables independently of each other. In fact, he needs to satisfy 503 constraints over 237 configuration variables across the 13 components. Examples of constraints are: keys, encryption and hash algorithms should be the same at both ends of every IPSec tunnel; IPSec tunnel local addresses should be equal to the IP addresses of originating interfaces, tunnel peer values should be symmetric and static routes should direct traffic into IPSec tunnels. The total number of configuration commands is 2239 with Linux hosts, Juniper inner gateways and Cisco outer gateways and WAN. The Cisco configuration file for OGW1 is listed in Table 1. Cisco configuration file for single router OGW1 in Figure 2. It lists values of IPSec configurations (peers, keys, encryption and hash algorithms) for the three outer tunnels, interface configurations (addresses, masks and originating tunnels), and static routing configuration.
The next section outlines how DADC automatically bridges the gap between requirements and configurations.