3.7 Verification
Given a requirement, DADC guarantees that any solution it generates satisfies System Requirement. However, the requirement itself may be incorrect. Incorrectness can take several forms.
3.7.1 Unsatisfiable requirement
One form of incorrectness is that S y s t e m Requirement itself is unsatisfiable. Then, DADC produces an unsat-core. For example, if to the requirement of Section we add the constraint ip address IGW1 eth0 = 1.1.1.1, DADC produces the unsat-core below stating that it is not possible for the address of IGW1/eth0 to be 1.1.1.1 and yet belong to the range 201.0.0.0/24.
DADC does not attempt to repair such a requirement as it represents a design error that is best addressed by the designer.
3.7.2 Requirement does not satisfy intent
Another form of incorrectness is that while System Requirement is correct, it does not satisfy a design intent. One way of checking if it does is to express a simpler form of intent and check if the requirement implies the simpler form. This can be accomplished by checking that the requirement and the negation of the simpler form is unsatisfiable. In other words, any configuration that satisfies the requirement also satisfies the simpler form.
3.7.3 Firewall verification
DADC allows one to check the inclusion and equivalence between firewall policies. Policy P1 is included in a policy P2 provided every packet permitted by P1 is permitted by P2. P1 and P2 are equivalent if each is included in the other. We assume that policies are evaluated on five fields of a packet header: source address, source port, destination address, destination port and protocol. The brute-force approach to solving this problem by enumerating all packet headers and checking whether it is permitted (or not) by each policy is computationally infeasible. There are 2^104 packet headers to enumerate with 32 bit source and destination addresses, 16 bit source and destination ports and 8 bit protocol. DADC solves the inclusion (and equivalence) problem by converting a policy into a constraint on a generic packet header consisting of five variables one for each field. For given values of these variables, the constraint is true iff the packet header is permitted by the policy. Now, P1 is included in P2 if the constraint for P1 and the negation of the constraint for P2 is unsatisfiable. In other words, it is not possible to find a packet header that is permitted by P1 but not by P2. More details can be found in [21, 23].
3.7.4 Path planning
The problem of finding a path between a source and destination in a graph can be solved in time linear in the size of the graph. However, the problem is much harder if the graph contains firewalls or routers with access-control lists or we allow the placement of additional constraints on paths. The straightforward approach of enumerating all paths and finding one that satisfies constraints is infeasible. The number of paths in a graph can be exponential in the size of the graph. DADC converts this problem into a constraint satisfaction one and thus improves our chances of solving it. It models a path as a constraint on the generic packet header fields, and labels on nodes and edges indicating if they are on the path. The constraint is derived from the topology of the network, from access-control lists on the path, and other user-supplied constraints on the packet and path. The constraint generation algorithm makes use of the one outlined above for representing a firewall policy as a constraint. The path-finding algorithm is inspired by [5].
If a node is compromised then we can use this algorithm to find a new path between a source and destination such that path that avoids this node, and all access-control lists along the path permit the client-server flow. The algorithm can also be used to verify that there are no paths between a compromised node and a sensitive server that permit a given flow. We would check that the solver returns an unsat-core for the requirement that there be such a path.
3.8 Distributed configuration
DADC was originally designed as a centralized system that communicated with network components over an out-of-band network. The distributed version of it [14] removes both of these assumptions. As shown in Figure 5: Distributed ADC system architecture, the set of network components is partitioned into enclaves each controlled by a DADC controller. Each controller has the full functionality of a centralized DADC controller. Controllers communicate with each other over a Configuration Agreement Protocol (CAP) bus. Also communicating over this bus are Enterprise Management Systems and Intrusion Detection and Response Systems that provide information about the dynamic state of components: up, down, compromised.
CAP guarantees that messages are delivered to all controllers in the same order. Therefore, it presents to each controller an identical view of the dynamic state of all components. Each controller also has the identical System Requirement governing the whole network. Upon receipt of a message, each controller solves the System Requirement in the context of the current dynamic state. Since SAT or SMT solvers that we use are deterministic, each controller arrives at identical conclusions about the new configurations of all components, not just its own. Each controller then applies configurations relevant to its enclave to the enclave components, and the entire network converges to a new configuration satisfying System Requirement.
3.9 In-band configuration
The simplest way for a DADC controller to configure network components is over an out-of-band network. If using such a network is infeasible then the controller can try to use the data network itself, i.e., configure inband. The central challenge of in-band configuration is computing the order in which to reconfigure components. The controller should never be locked out of reaching a component before it has been reconfigured. Routing can be affected not just because routing protocol configurations can redirect traffic but also because access-control lists can block traffic. An algorithm for in-band configuration has been described in [30] where only static routing is assumed. A much more general algorithm (e.g., in the presence of dynamic routing) is possible if the network is assumed to be purely IPv4. Then, we can enable IPv6 at all interfaces of all components and let the controller communicate over the IPv6 network. No additional physical resources are required. All modern components support IPv4 and IPv6. The controller can change IPv4 configurations in any order since IPv6 reachability is unaffected by these changes. Since DADC also supports IPv6, the logical out-of-band control network configurations can also be automatically generated!
3.10 Visual specification language
While DADC’s specification language is semantically and syntactically simple, a new visual interface simplifies specification even further. One can drag and drop network and relationship objects onto a canvas and specify their attributes. At the click of a button, the text version of the requirement is generated. At the click of another button, the requirement is solved, configurations are generated and an emulation of the network is started up. Thus, one can draw a network concept in DADC and then test it under emulation in a few seconds. For example, a network of outer gateways connected to a WAN router and a full-mesh of IPSec tunnels between them is drawn in Figure 6. Visual specification of IP connectivity and a full-mesh of IPSec tunnels. Clicking the Full Mesh icon highlights the four outer gateways in the full mesh with red circles, but not the WAN router. Clicking on Generate Specification button shows the equivalent text specification. Clicking on “Run CORE Emulation” (not shown) starts up the emulation similar to that in Figure 4. CORE Emulation of network in Figure 2.
3.11 Reconfiguration planning
Once component configurations have been computed, the problem still remains: in what order should these be applied to the components so that an invariant is never violated during the transition? For example, in the network of Figure 2, we may want to apply IPSec configurations before the static routing ones so that when packets flow, they are encrypted. The reconfiguration planning algorithm allows one to specify an invariant as a requirement and transforms it into a constraint on the times at which the invariant variables should change so that the invariant remains true at all times. This constraint is then solved to compute a safe schedule of changes to the variables. Details are available in [20].
3.12 Moving-target defense
Moving-target defense is accomplished by finding a new solution to System Requirement subject to the additional constraint that values of some critical variables be different than those in the Current Configuration. A set of values is critical if their knowledge would enable an adversary to plan an effective attack. Periodically, DADC selects a critical variable x, generates the constraint not(x=c) where c is the current value of x, strengthens System Requirement with it, and reattempts a solution [26].