Network-wide Configuration Synthesis

1 Introduction

• Operators must manually configure devices so distributed protocols compute forwarding states that satisfy network-wide requirements, a complex task that can lead to severe downtime.The introduction cites a widespread outage lasting about an hour as an example.Source: §1 · p. 1
• The paper frames network-wide configuration synthesis as finding a configuration that makes routers converge to a forwarding state compatible with operator requirements.The operator supplies high-level requirements; the configuration is obtained automatically.Source: §1 · p. 2
• Synthesis must account for protocol diversity, dependencies between protocols, and the massive configuration search space.For example, OSPF supports shortest-path multipath routing, while BGP can direct traffic along non-shortest paths and depends on intra-domain configuration.Source: §1 · p. 2
• The approach encodes router protocols and their dependencies in stratified Datalog, then seeks inputs whose program fixed point satisfies the requirements.The resulting input identifies the desired network-wide configuration.Source: §1 · pp. 2–3
• The contributions include a stratified-Datalog input-synthesis algorithm and SyNET, an implementation supporting interacting protocols and static routes.The algorithm is presented as applicable beyond networks; the system evaluation covers multiple interacting widely used protocols.Source: §1 · p. 3
• Networks with more than 50 routers and multiple traffic classes are within SyNET’s demonstrated synthesis scope.The evaluation also tests generated configurations in an emulated network environment.Source: §1 · p. 3

2.1 Motivating Example

• OSPF alone cannot enforce the example’s two internal path requirements, but static routing at A combined with selected OSPF weights and route preferences can.The static entry steers N1 through B, while OSPF supplies the path for N2.Source: §2.1 · p. 5
• BGP and OSPF can interact: equal BGP preferences let OSPF path costs select the egress point for external traffic.In the example, link weights make the required paths to C and B lowest-cost from A and D, respectively.Source: §2.1 · p. 5
• The network is modeled as a stratified Datalog program that derives forwarding entries, while requirements are expressed as constraints over those entries.Fwd(TC, Router, NextHop) records the next hop for a router and traffic class.Source: §2.1 · p. 6
• The synthesis task is to find a Datalog input whose program fixed point satisfies the routing requirements.The input represents a network-wide configuration, and the resulting router configurations are derived from it.Source: Figure 1 · p. 4, §2.1 · p. 6
• The proposed iterative algorithm partitions a stratified program into strata, synthesizes an input for each stratum, and constructs the program input from them.The section notes that input synthesis is generally undecidable, but becomes decidable when inputs are bounded to a finite value set.Source: §2.1 · p. 6

3 Background: Stratified Datalog

• A program is well-formed when every variable in a rule head also occurs in that rule’s body.Rules, literals, and terms are written as comma-separated sequences.Source: §3 · p. 6
• Stratification places rules into ordered strata so positive dependencies may refer to the same or lower strata, while negative dependencies must refer to lower strata.This ensures predicates used negatively are fully defined before they are needed.Source: §3 · pp. 6–7
• The presentation extends stratified Datalog with aggregate functions such as min and max.The passage states this is possible because stratified Datalog is equally expressive to Datalog with stratified aggregate functions.Source: §3 · p. 7
• For an input of ground atoms, a program’s model is the fixed point computed through its strata, beginning with the input and successively extending the interpretation.The model is the interpretation produced by the final stratum.Source: §3 · p. 7

4.1 Specifying Networks

• Protocol rules derive a global forwarding predicate by collecting OSPF and static-route entries and selecting the entry with minimal administrative cost.Topology is also represented in Datalog, including predicates for links between router constants.Source: §4.1 · pp. 7–8

4.2 Specifying Requirements

• Routing requirements are function-free first-order constraints over forwarding state, covering path selection, traffic isolation, reachability, and loop-freeness.More complex requirements such as way pointing can be built from the core constraints.Source: §4.2 · p. 8

4.3 Network-wide Configurations

• Router protocol settings are input predicates; the example includes administrative costs, a static route, and OSPF link weights.Figure 3 depicts strata and the flow of predicates between them.Source: §4.3 · pp. 8–9, Figure 3 · p. 9

5 Input Synthesis for Stratified Datalog

• The overall algorithm applies SSemiPos to each stratum, with backtracking when synthesized inputs cannot be made compatible across strata.The three-stratum example illustrates this process, including matching lower-stratum outputs to the inputs already selected for higher strata.Source: §5 · p. 9

5.1 Input Synthesis for Semi-positive Datalog with SMT

• SSemiPos encodes synthesis as SMT satisfiability, and a satisfying model yields an input whose fixed point satisfies the constraint.The algorithm unrolls rules up to a predefined bound; it is guaranteed to return an input when a satisfying input reaches its fixed point within that bound.Source: §5.1 · pp. 9, 10, 12
• The encoding handles positive and negative requirements differently: unrolling recursive predicates is sound for positive constraints, while leaving them unrolled is sound for negative constraints.This split addresses the mismatch between Datalog fixed-point semantics and classical first-order SMT semantics.Source: §5.1 · p. 10

5.2 Iterative Input Synthesis for Stratified Datalog

• SStrat partitions the program into strata, synthesizes inputs iteratively from higher to lower strata, and combines those inputs into one program input.It aligns each stratum’s derived predicates with the inputs synthesized for higher strata.Source: §5.2 · p. 13
• When a lower stratum cannot produce predicates required by a higher stratum, SStrat backtracks and records failed inputs to avoid repeating them.A predefined bound on failed inputs controls when the algorithm backtracks rather than continuing its search.Source: §5.2 · p. 14
• If SStrat returns an input, its fixed point satisfies the constraint; the same soundness guarantee holds for SSemiPos on semi-positive programs.The guarantees establish correctness of returned inputs, not that a satisfying input will always be found.Source: §5.1 · p. 12, §5.2 · p. 14

6.1 Implementation

• SyNET encodes LogicBlox stratified Datalog as SMT-LIB constraints and uses Z3; it supports OSPF, BGP, and static routes with natural protocol splitting.The implementation partitions rules into eight strata, uses a bound of 20 for most topologies and requirements, and converts synthesized inputs to Cisco configurations for testing.Source: §6.1 · pp. 14–15
• Partial evaluation removes rules with known predicate values, while reusable generic and protocol-specific constraints reduce variables and encode properties independent of topology or requirements.One example constraint prevents forwarding packets out of a router when their destination network is directly connected.Source: §6.1 · p. 15

6.2 Experiments

• All synthesized configurations were run in an emulated Cisco-router environment, where computed forwarding paths were verified against each experiment’s requirements.Source: §6.2 · p. 15
• Experiments cover 4–64-router topologies, including Internet2 and grids, 1, 5, or 10 traffic classes, and three combinations of static routes, OSPF, and BGP.For multiple traffic classes, external networks are announced by two randomly selected routers, and local BGP preferences are fixed while SyNET synthesizes OSPF costs.Source: §6.2 · pp. 15–16
• For 64 routers and 10 traffic classes, synthesis takes less than 1 hour with static routes, less than 22 hours with OSPF and static routes, and times out after 24 hours with OSPF, BGP, and static routes on the largest topologies.With OSPF, BGP, and static routes, all topologies finish within 8 hours for 1 and 5 traffic classes.Source: Table 1 · p. 16, §6.2 · pp. 16–17
• A study of production networks found 56% have fewer than 32 routers, for which SyNET would synthesize configurations within one hour; large networks typically have fewer than 15 traffic classes.The traffic-class estimate is based on a study of real-world enterprise and WAN networks.Source: §6.2 · p. 17

7 Related Work

• Existing Datalog analysis tools compute a fixed point and check a property for a supplied input, whereas this approach discovers an input yielding a fixed point that satisfies the property.Source: §7 · p. 17
• The algorithm in [35] handles non-monotone stratified Datalog only indirectly and supports negative properties, while FORMULA supports non-recursive programs rather than recursive rules with stratified negation.The paper notes that virtually all network specifications require recursive rules.Source: §7 · p. 17
• Unlike symbolic execution, which unrolls loops to find inputs violating assertions, SyNET synthesizes inputs for a given program; unlike typical counter-example-guided synthesis, it uses a sequence of oracles.The paper distinguishes its setting, techniques, and algorithms from standard symbolic execution.Source: §7 · p. 18
• Propane supports BGP and Genesis supports static routes; both support failure-resilience requirements, while SyNET can be extended with additional protocols specified in stratified Datalog.Directly quantifying over links for failure-resilience requirements would make synthesis more expensive.Source: §7 · p. 18
• ConfigAssure cannot capture routing-protocol fixed-point computation and therefore cannot synthesize protocol configurations for networks.Source: §7 · p. 18

8 Conclusion

• The network-wide configuration problem is formulated as finding inputs to a Datalog program, and a new algorithm solves the resulting input-synthesis task.Source: §8 · p. 18
• The algorithm decomposes Datalog rules into strata and iteratively synthesizes inputs for individual strata using off-the-shelf SMT solvers.Source: §8 · p. 18
• SyNET scales to realistic network sizes using combinations of OSPF, BGP, and static routes.Source: §8 · p. 18

A Formalizing OSPF

• BestOSPFRoute represents a router’s selected route to a network by its next hop and minimum cost.Source: A Formalizing OSPF · p. 21
• The second rule aggregates over possible OSPF routes to derive the minimum-cost route for each router and destination network.Source: A Formalizing OSPF · p. 21
• The last two rules encode shortest-path routing: one derives neighbor forwarding with link cost, and the other computes multi-hop paths by summing route costs.Source: A Formalizing OSPF · p. 21

• inp(P, J) denotes the set of ground atoms in interpretation J that use edb predicate symbols of program P.Source: B Proofs · p. 21
• The definition selects atoms that are both contained in J and constructed with predicates from edb(P).Source: B Proofs · p. 21
• Formally, inp(J, P) is the set of p(t) such that p belongs to edb(P).Source: B Proofs · p. 21

• For semi-positive programs, the model is the least fixed point of the consequence operator and can be computed iteratively.Source: §B.1 · p. 21
• An interpretation satisfying [P]k over-approximates the atoms derived by P for its extracted input inp(P, J).Source: §B.1 · p. 22
• For negative constraints, SSemiPos returns only inputs whose fixed points do not derive the prohibited atom.Source: §B.1 · p. 22
• The positive-constraint proof shows that an atom marked at iteration k in an interpretation satisfying [P]k is derived by P for the extracted input.Source: §B.1 · p. 22
• For positive constraints, SSemiPos returns inputs whose fixed points derive the required atom.Source: §B.1 · p. 23
• If SSemiPos returns an input for a constraint, the program’s fixed point under that input satisfies the constraint.Source: §B.1 · pp. 23–24

• If SStrat returns an input for a constraint over the final stratum, the full stratified program’s fixed point satisfies that constraint.Source: §B.2 · p. 24
• At the base case, SStrat applies SSemiPos to the final stratum, whose input satisfies the constraint by Theorem 1.Source: §B.2 · p. 24
• The proof inducts over strata, using each constructed constraint to ensure derived atoms match the corresponding input atoms for later strata.Source: §B.2 · p. 24