3. DADC Design
This section sketches the design of DADC tools.
3.1 Intuitive requirement specification language
DADC allows one to specify requirements or properties that a network should satisfy. It offers a Requirement Library of useful constraints. The Library contains logical structures and relationships that are typically used in network architecture diagrams. One heuristic for identifying these is by formalizing the notion of “correct configuration.” For each protocol, we ask how a group of agents executing that protocol should be configured so they accomplish a joint goal associated with that protocol. Answers to this question are encoded as constraints in the Requirement Library. Library constraints can be composed with logical operators to specify a very large class of requirements. In particular, the AND operator formalizes the superposition of logical structures in typical network architecture diagrams. For example, the entire network in Figure 2 is specified in DADC as the conjunction of requirements in Table 2. DADC specification of entire network of Figure 2:
The component requirements declare component vendors. Together they satisfy diversity requirements. The enclave requirement means there is linear IP connectivity between the client, inner gateway, outer gateway and the wan, and that all packets originating from a node are forwarded to its successor. The full mesh ipsec tunnels requirement means there is a full mesh of IPSec tunnels between the interfaces on the right, encrypting all traffic originating at the subnet of the left interfaces. Finally, the ospf domain requirement means OSPF is enabled at all interfaces of the WAN router and that all interfaces are in area 0 with default hello and dead timer values. Surprisingly, no additional routing is needed. Packets originating at clients are forwarded to inner gateways, encrypted, forwarded to outer gateways, re-encrypted and forwarded to the WAN router. That router, using OSPF-learned routes, redirects packets to the remote interface of outer tunnels where they are decrypted, forwarded to remote interfaces of inner gateways, decrypted and forwarded to the clients.
No IP addresses, static routing, or IPSec or OSPF configurations are explicitly specified. These are all computed when the requirement is solved. Conventional configuration languages force one to specify all values of configuration variables. By contrast, DADC allows one to specify just the constraints that these variables must satisfy. DADC solves these constraints to compute the values. This transition from specifying explicit variable values to specifying the conditions that these must satisfy marks a major increase in expressive power.
The entire network is specified in a single file. This is a major simplification over current practice in which a separate configuration file has to be created for each component. This makes it much harder to enforce complex dependencies across multiple files because of the context switching between different files.
In conventional configuration languages one is often forced to write requirements in a definite order. For example, static routes or firewall rules cannot be written unless the IP addresses in their fields are determined. If these addresses change, then these routes and rules have to be manually updated with the new addresses. DADC eliminates such ordering and manual updates by allowing requirements to contain variables. When variable values are computed, the requirements are automatically updated with the new values. No special manual action needs to be taken when values change. The constraint solver automatically accomplishes the update.
Not only are the semantics of the language simple, so is the syntax. A requirement is a sequence of identifiers separated by white spaces. There are no special symbols such as commas, colons, semicolons, curly, round or square braces. Except for those in IP addresses, there are no dots either. Requirements can be split across multiple lines. Each unindented line is assumed to start a requirement. All indented lines following it are assumed to belong to that requirement. The sequence of all identifiers in these lines is accumulated and parsed. All requirements in a specification file are assumed to be composed by conjunction. Thus, one does not have to write the conjunction operator for these top-level requirements. The order in which requirements are written in a file is immaterial. DADC checks whether a requirement is syntactically correct, and if not, outputs an error message.
3.2 Configuration synthesis
DADC transforms requirements into primitive constraints in the language of an SMT solver. For example, the requirement:
is transformed into the conjunction of the following requirements:
The first is further transformed into the conjunction of primitive constraints that the IP addresses of C1 eth0 and IGW1 eth0 are distinct, are in the range 201.0.0.0/24, but are not equal to the first and last addresses in the range.
For configuration synthesis, DADC simply solves the accumulated primitive constraints using an SMT solver [17]. An excerpt from the solution for the CSfC requirements is:
3.3 Configuration repair
DADC parses configuration files of an existing network into a large constraint Current Configuration of the form x1=c1,..,xk=ck where each xi is a configuration variable in the requirement and ci is its value in one of the uploaded configuration files. If the conjunction (System Requirement ∧ Current Configuration) is unsolvable, then the solver produces an “unsat-core.” This is a typically small constraint that is itself unsatisfiable and whose unsatisfiability causes that of the conjunction.
The unsat-core can be taken to be a root-cause of the unsolvability of the conjunction. If in the unsat-core there is an equation of the form x=c that occurs in Current Configuration, then this equation represents a configuration error. This error can be repaired by deleting this equation from Current Configuration and reattempting the solution to (System Requirement ∧ Current Configuration). This step is repeated until either a solution is obtained or it is no longer possible to find an equation of the form x=c in the unsat-core. At that stage, the algorithm halts and outputs the unsat-core. That unsat-core represents a design flaw in the System Requirement itself. This flaw is best resolved by the user because the System Requirement represents his intent.
Another repair option is to use a MaxSAT solver [22]. One can associate weights with variables representing the cost of changing their values. Then, MaxSAT can find the minimum cost change to values in Current Configuration so that System Requirement becomes true. If no weights are associated, MaxSAT can find the minimum number of variables to change.
3.4 Vendor-specific adapters
From the solution produced by the constraint solver, DADC generates configuration files for all components referenced in System Requirement. When these are successfully applied to components, their joint configuration would satisfy System Requirement. For example, the Cisco configuration file in Section was automatically generated by DADC.
DADC parses configuration files of different vendors to produce Current Configuration. However, it is infeasible to base parsing on writing grammars for vendorspecific configuration languages. Instead, DADC creates a database of the configuration file and then queries it to obtain the values of configuration variables in System Requirement [23]. This approach avoids the need to model the entire language when we are only interested in a subset of it.
DADC also defines an internal, abstract, vendor-neutral information model for configuration. All of its algorithms work on this model. Adapters for configuration generation and parsing are developed for each vendor. DADC communicates with devices using SNMP for Cisco and SSH for other vendors. It applies and reads entire files rather than individual commands.
3.5 Visualization of current configuration
DADC produces visualizations of a number of logical structures latent in the current network configuration. DADC can either read the configuration directly from the components. Or, an administrator can gather the configuration files, zip them, and input them to DADC. In many cases, the latter method is preferable because of its non-invasiveness. Visualizations can provide a good conceptual understanding of the network. These can also uncover structural defects. For example, suppose that in the configuration of OGW1 in Section , we change the peer value from 20.0.0.1 to a non-existent 200.0.0.1. DADC then produces the visualizations for IPSec tunnels shown in Figure 3. The inner gateway tunnels form a fullmesh as expected. The other gateway tunnels don’t. What should have been a tunnel from OGW1 to OGW2 is now pointing to the non-existent address.
3.6 Emulation
DADC has been integrated with two network emulation systems, GNS3 [7] and CORE [3]. In addition to generating component configurations satisfying a requirement, DADC also generates a configuration file for emulation. When the appropriate emulator is started with this file, the observed behavior of the network is indistinguishable from that of a physical network satisfying the same requirement except, perhaps, for performance. The net result is that complex requirements can be specified and evaluated in minutes rather than the days or months it currently takes to compute configurations, build a physical network, configure it and run tests. Figure 4. CORE Emulation of network in Figure 2 shows the CORE emulation of the network of Figure 2. It shows that ping from C1 to C4 succeeds, as we expect. It also shows that these packets are encrypted, i.e., encapsulated inside ESP packets originating at IGW1/eth1 with address 1.0.0.1 and destined to IGW4/eth1 with address 4.0.0.1. Finally, it shows the second layer of encryption inside ESP packets originating at OGW1 eth2 with address 10.0.0.1 and destined to OGW4/eth5 with address 40.0.0.1.
