Description
NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion
---
打轴：Whisper v3-large-turbo + 剪映
翻译：Gemini 2.0 Flash Thinking Experimental 01-21
校对 & 后期：我
---
### 场景
人工配置网络耗时且容易出错，所以近两年（2017-2018）提出用机器合成配置，也就是意图驱动配置生成。
### 挑战
以往工作的合成的配置存在可解释性、连续性、可部署性不好的问题。
- 可解释性差：以往工作合成的配置没法按照网络管理员的意图进行修改，管理员们往往不信任生成的配置；或者生成的配置风格和人工生成的差异很大，难以理解和调试
- 连续性：稍微修改一点点意图，生成的配置可能就截然不同。
- 可部署性：一个网络团队并没有修改整个网络配置的权限，更有可能的情况是，一个团队只能修改一小部分的配置。所以基于整个网络进行配置更新的工作的实用性很差。
本工作的主要贡献是提出了基于自动补全草图的配置合成方式，使用 SMT 但是显著提高了 SMT 在大规模网络中的求解速度
### 方法
本工作用草图（Configuration Sketches）的方式约束配置生成的内容，只保留一些“空”，比如说 OSPF 的权重值等参数值交给 Solver 求解
这允许人工设定配置的格式，所以可解释性较好；同时也避免了“为了新增一个功能而重写整个网络配置”的问题。
Solver 的求解方式是 SMT。大规模网络直接按照上述方法使用 SMT 会由于合成时间而不具有实际价值。所以，本工作提出了多种方法对搜索方式和搜索空间进行优化：
- **部分评估 (Partial Evaluation):** 用于加速 BGP 合成，通过传播符号化宣告，提前消除许多变量。
- **基于反例引导的归纳合成 (Counter-Example Guided Inductive Synthesis, CEGIS):** 用于 OSPF 合成，显著提升了 OSPF 权重合成的效率。
- **特定于领域的启发式方法:** 结合网络领域的知识和启发式方法来引导搜索空间。
数据集是 Topology Zoo，网络规模从 32-200；输入给 Solver 需求和草图为程序随机生成。
SMT 保证正确性，所以论文主要评估的是合成速度。主要对比的工作是 SyNET，合成时间相比 SyNET 减少了多个数量级（>100x）。