关系网络验证
网络与互联网体系结构
2024-03-27 v1
摘要
关系网络验证是一种验证网络变更的新方法。与传统网络验证分析单个网络快照的规范不同，关系网络验证分析涉及两个网络快照（例如，变更前和变更后的快照）的规范，并捕获它们的相似性和差异性。关系变更规范紧凑且精确，因为它们指定了快照之间发生变化的流或路径，然后简单地要求网络的其他行为“保持不变”，而无需逐一枚举。为了获得类似的保证，单快照规范需要枚举所有预期不会发生变化的流和路径行为，以便我们能够检查是否有任何意外改变。因此，精确的单快照规范与网络规模成正比，这使得它们对于许多真实世界网络而言难以生成。为了证明关系推理的价值，我们开发了一种高级关系规范语言和一个名为 Rela 的工具来验证网络变更。Rela 首先将输入规范和网络快照表示编译为有限状态转换器。然后，它使用自动机等价性的判定过程来检查合规性。我们使用全球骨干网（超过 10^3 台路由器）复杂变更数据的实验发现，93% 的 Rela 规范需要少于 10 个术语，并且它在 20 分钟内验证了其中 80% 的变更。
引用
@article{arxiv.2403.17277,
title = {Relational Network Verification},
author = {Xieyang Xu and Yifei Yuan and Zachary Kincaid and Arvind Krishnamurthy and Ratul Mahajan and David Walker and Ennan Zhai},
journal= {arXiv preprint arXiv:2403.17277},
year = {2024}
}