发表机构
ETH Zürich（苏黎世联邦理工学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出一种自动演进的网络验证器，通过编码智能体与可信预言机的反例引导循环，让基于SMT的验证器自主学习新网络功能，解决手动维护模型的难题。
AI 中文摘要
符号网络验证器可对路由输入和故障的广阔空间进行正确性推理，但仅适用于专家手动编码的协议和功能。创建并维护控制平面的忠实模型既困难又永无止境，因为没有书面源能完美指定网络的实际行为：厂商实现与 RFC 存在偏差，且行为会随版本更新而变化。持续维护的负担最终使许多需要验证的网络无法应用该技术。我们认为模型应自动演进以忠实捕捉网络实际行为。为实现这一点，我们利用唯一能明确指定网络行为的来源：路由器软件本身。在反例引导的循环中，编码智能体提出对验证器符号编码的扩展，而可信预言机（如仿真路由器）提供真实路由状态。智能体通过每次与预言机的分歧迭代优化网络模型。作为初步证据，该系统的一个原型向一个基于 SMT 的 3000 行验证器传授了三个其不支持的功能：OSPF 区域、BGP 路由反射以及 EVPN 上的 L3VPN，自主收敛到与预言机匹配的模型，甚至注意到厂商特定行为。模型增长自动化将难题从编写验证系统转变为系统测试它们；我们提出了一项研究议程，用于信任和利用自动演进的验证器。
英文摘要
Symbolic network verifiers can reason about correctness across vast spaces of routing inputs and failures, but only for the protocols and features an expert has encoded by hand. Creating and maintaining a faithful model of the control plane is both difficult and never-ending, since no written source specifies perfectly what a network does: vendor implementations deviate from the RFCs, and behaviour shifts with releases. The burden of constant upkeep ultimately keeps verification out of many networks that need it. We argue that the model should instead evolve automatically to faithfully capture the actual network behaviour. To achieve that, we leverage the only source that specifies it unambiguously: the router software itself. In a counterexample-guided loop, a coding agent proposes extensions to the verifier's symbolic encoding, while a trusted oracle (e.g., emulated routers) supplies the ground-truth routing state. The agent iteratively refines the network model using each disagreement with the oracle. As early evidence, a prototype of this system taught a 3,000-line SMT-based verifier three features it did not support: OSPF areas, BGP route reflection, and L3VPN over EVPN, converging autonomously on models that match the oracle, even noticing vendor-specific behaviour. Automating model growth shifts the hard problem from writing verification systems to systematically testing them; we propose a research agenda for trusting and harnessing automatically evolved verifiers.
Comments8 pages, 5 figures
