Symbolic router execution
Symbolic router execution
复制标题
符号路由器执行
DOI：
10.1145/3544216.3544264
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Gember-Jacobson, Aaron
中科院分区：
文献类型：
--
作者：
Zhang, Peng;Wang, Dan;Gember-Jacobson, Aaron
网络验证通常需要在不同的故障模型（确定性和/或概率）下分析跨不同空间（报头空间、故障空间或其产品）的属性。现有的验证器有效地覆盖了头部或故障空间，但不能同时覆盖两者，并且有效地对确定性或概率性故障进行推理，但不能同时覆盖两者。因此，没有单一的验证者能够支持所有需要不同空间覆盖和故障模型的分析。本文介绍了SRE (Symbolic Router Execution)，它是一种通用的、可扩展的、支持多种分析的验证引擎。SRE象征性地执行网络模型来发现我们所谓的包失败等价类（pfec），每个pfec都在报头和失败的产品空间中具有独特的转发行为。SRE在符号执行期间支持各种优化，同时保持故障模型的不可知性，因此它以通用的方式扩展到产品空间。通过使用bdd对符号头和失败进行编码，各种分析可以简化为bdd上的图形算法（例如，最短路径）。我们使用真实拓扑和合成拓扑进行的评估表明，与最先进的方法相比，SRE在检查可达性、挖掘规范等方面取得了更好或相当的性能。
Network verification often requires analyzing properties across different spaces (header space, failure space, or their product) under different failure models (deterministic and/or probabilistic). Existing verifiers efficiently cover the header or failure space, but not both, and efficiently reason about deterministic or probabilistic failures, but not both. Consequently, no single verifier can support all analyses that require different space coverage and failure models. This paper introduces Symbolic Router Execution (SRE), a general and scalable verification engine that supports various analyses. SRE symbolically executes the network model to discover what we call packet failure equivalence classes (PFECs), each of which characterises a unique forwarding behavior across the product space of headers and failures. SRE enables various optimizations during the symbolic execution, while remaining agnostic of the failure model, so it scales to the product space in a general way. By using BDDs to encode symbolic headers and failures, various analyses reduce to graph algorithms (e.g., shortest-path) on the BDDs. Our evaluation using real and synthetic topologies show SRE achieves better or comparable performance when checking reachability, mining specifications, etc. compared to state-of-the-art methods.
登录
查看更多内容
影响因子：
--
作者：
Ryan Beckett;Aarti Gupta;Ratul Mahajan;D. Walker
通讯作者：
Ryan Beckett;Aarti Gupta;Ratul Mahajan;D. Walker
ProbNV：网络控制平面的概率验证
影响因子：
--
作者：
Giannarakis, Nick;Silva, Alexandra;Walker, David
通讯作者：
Walker, David
DOI：
--
发表时间：
2020
期刊：
ACM SIGCOMM Symposium on Software Defined Networking Research
影响因子：
--
作者：
A. Kheradmand
通讯作者：
A. Kheradmand
DOI：
--
发表时间：
2020
期刊：
Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication
影响因子：
--
作者：
Samuel Steffen;Timon Gehr;Petar Tsankov;Laurent Vanbever;Martin T. Vechev
通讯作者：
Martin T. Vechev
NV：用于验证网络控制平面的中间语言
DOI：
10.1145/3385412.3386019
发表时间：
2020
期刊：
PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Giannarakis, Nick;Loehr, Devon;Beckett, Ryan;Walker, David
通讯作者：
Walker, David