Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement
Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement
复制标题
DOI：
10.1007/978-3-030-25543-5_18
复制
发表时间：
2019-07
期刊：
影响因子：
--
通讯作者：
Nick Giannarakis;Ryan Beckett;Ratul Mahajan;D. Walker
中科院分区：
文献类型：
--
作者：
Nick Giannarakis;Ryan Beckett;Ratul Mahajan;D. Walker
我们展示了如何验证大型数据中心网络满足关键属性，例如在有限数量的故障下的所有对可达性。为了扩展分析，我们开发了识别网络对称性和从大型具体网络计算小型抽象网络的算法。使用反例引导的抽象细化，我们连续细化计算的抽象，直到给定的属性可以被验证。我们的方法的合理性依赖于一个新的网络近似的概念：在具体的网络中的路由路径是不精确的模拟那些在抽象的网络，但保证是“至少一样好”。我们实现我们的算法在一个工具，称为折纸，并使用它们来验证故障下的标准数据中心拓扑结构的可达性。我们发现，Origami计算抽象网络的边数少了1-3个数量级，这使得验证现有技术无法实现的大型网络成为可能。
We show how to verify that large data center networks satisfy key properties such as all-pairs reachability under a bounded number of faults. To scale the analysis, we develop algorithms that identify network symmetries and compute small abstract networks from large concrete ones. Using counter-example guided abstraction refinement, we successively refine the computed abstractions until the given property may be verified. The soundness of our approach relies on a novel notion of network approximation: routing paths in the concrete network are not precisely simulated by those in the abstract network but are guaranteed to be “at least as good.” We implement our algorithms in a tool called Origami and use them to verify reachability under faults for standard data center topologies. We find that Origami computes abstract networks with 1–3 orders of magnitude fewer edges, which makes it possible to verify large networks that are out of reach of existing techniques.