AED: incrementally synthesizing policy-compliant and manageable configurations

When updating router configurations, network operators often attempt to meet a variety of management objectives (e.g., maintaining structural similarity across devices), while also ensuring all forwarding policies are correctly satisfied. Our tool, AED, automates this process. AED models configuration updates as a collection of syntax tree additions and removals, and formulates an innovative system of SMT (Satisfiability Modulo Theory) constraints that encode configurations' structure and interaction with routing algorithms. Operators express management objectives in a high-level language, and AED translates these to "soft" constraints that are maximally satisfied. Evaluations on real and synthetic network configurations show that AED can update networks with tens of routers and hundreds of policies in under a minute, and AED outperforms both hand-crafted updates and state-of-the-art tools in meeting management objectives.