NV: an intermediate language for verification of network control planes
NV: an intermediate language for verification of network control planes
复制标题
NV：用于验证网络控制平面的中间语言
DOI：
10.1145/3385412.3386019
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Walker, David
中科院分区：
文献类型：
--
作者：
Giannarakis, Nick;Loehr, Devon;Beckett, Ryan;Walker, David
在过去的十年中，网络配置错误导致了大量引人注目的中断，促使研究人员开发各种网络分析和验证工具。不幸的是，由于网络配置语言的复杂性，开发和维护这样的工具是一个巨大的挑战。受Boogie和Why3等验证中间语言的启发，我们开发了NV，一种用于网络控制平面验证的中间语言。NV谨慎地在表现力和易处理性之间游走，使得为真实的协议及其配置的实际子集构建模型成为可能，并且还促进了工具的快速开发，这些工具的性能优于最先进的模拟器（秒vs分钟）和验证器（通常快10倍）。此外，我们表明，它是可能的，开发新的分析，只是通过编写新的NV程序。特别是，我们实现了一种新的容错分析，可扩展到比现有工具大得多的网络。
Network misconfiguration has caused a raft of high-profile outages over the past decade, spurring researchers to develop a variety of network analysis and verification tools. Unfortunately, developing and maintaining such tools is an enormous challenge due to the complexity of network configuration languages. Inspired by work onintermediate languages for verificationsuch as Boogie and Why3, we developNV, an intermediate language for verification of network control planes. NV carefully walks the line between expressiveness and tractability, making it possible to build models for a practical subset of real protocols and their configurations, and also facilitate rapid development of tools that outperform state-of-the-art simulators (seconds vs minutes) and verifiers (often 10x faster). Furthermore, we show that it is possible to develop novel analyses just by writing new NV programs. In particular, we implement a new fault-tolerance analysis that scales to far larger networks than existing tools.
登录
查看更多内容
DOI：
10.1145/3132747.3132753
发表时间：
2017-10
期刊：
Proceedings of the 26th Symposium on Operating Systems Principles
影响因子：
--
作者：
Aaron Gember;Aditya Akella;Ratul Mahajan;H. Liu
通讯作者：
Aaron Gember;Aditya Akella;Ratul Mahajan;H. Liu
有状态网络的抽象解释
DOI：
10.1007/978-3-319-99725-4_8
发表时间：
2017
期刊：
RFC
影响因子：
--
作者：
Kalev Alpernas;R. Manevich;Aurojit Panda;Shmuel Sagiv;S. Shenker;Sharon Shoham;Yaron Velner
通讯作者：
Yaron Velner
DOI：
--
发表时间：
2016
期刊：
影响因子：
--
作者：
Konstantin Weitz;Doug Woos;Emina Torlak;Michael D. Ernst;A. Krishnamurthy
通讯作者：
A. Krishnamurthy
DOI：
10.17487/rfc7938
发表时间：
2016-08
期刊：
RFC
影响因子：
--
作者：
Petr Lapukhov;A. Premji;Jon Mitchell
通讯作者：
Petr Lapukhov;A. Premji;Jon Mitchell
影响因子：
--
作者：
Ryan Beckett;Aarti Gupta;Ratul Mahajan;D. Walker
通讯作者：
Ryan Beckett;Aarti Gupta;Ratul Mahajan;D. Walker