NeTS: Medium: Collaborative Research: Network Configuration Synthesis: A Path to Practical Deployment

NeTS：媒介：协作研究：网络配置综合：实际部署之路

• 批准号: 1703493
• 负责人: David Walker
• 金额: $ 57万
• 依托单位: Princeton University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-07-01 至 2022-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1703493&HistoricalAwards=false
• 关键词: NeTS; Medium; Collaborative; Research; Network

All sectors of society depend on properly functioning computer networks. For example, every day, millions of citizens order prescription drug refills, pay their electricity bills, book hotels, shop for groceries, and participate in thousands more activities online, through the cloud. But none of these services will work if the networks that deliver information are down. Moreover, modern business, healthcare, the military and the government are just as dependent on reliable networks as everyday citizens. Many network outages are caused by operators manually (and incorrectly) programming the 'configuration files' that manage the ways that network devices forward information. While the flexibility allowed by configuration files is essential, network outages are often caused by operators using hundreds of low-level directives at each network device to create network-wide policy. Because the global consequences of making even small configuration changes is so drastic, many organizations take several weeks to audit even small changes, limiting their ability to respond effectively to traffic fluctuations, business opportunities, security threats and hardware failures. A natural solution to these problems -- analogous to the trend in programming languages for software development over the last several decades as programmers have moved from machine code to Java -- is to define more robust, higher-level programming languages for implementing network policies. However, there are technical and pragmatic hurdles to surmount before it will be possible to deploy new languages in industrial settings on a large scale. In particular, existing network-wide policy languages are not expressive enough for many desired network policies and often require wholesale migration to new networking platforms. Hence, the overarching goal of this project is to surmount the technical challenges that impede practical deployment of high-level network programming languages. The project is developing the core technology necessary to efficiently support and incrementally deploy high-level network policies. The project leverages connections to two major cloud providers as a means to test the resulting languages and systems on real industrial networks, identify pragmatic barriers to adoption, and ultimately deploy the technology where possible.The project builds on the PIs' recent work on Propane, a new network programming language that allows users to describe end-to-end paths for intra- and inter-domain routing, along with a compiler that produces configurations for the industry-standard BGP protocol. The results of this project will extend Propane in several ways to support practical deployment: First, users will be able to declare device roles (e.g., top-of-rack switch) and the connectivity invariants related to them to enable concise specifications. A new compiler will verify safety properties of policies in the presence of such declarations and generate parameterized templates that make compiler outputs more intelligible for operators. Second, users will specify financial contracts that govern transit costs using a new declarative language and the compiler will optimize routes automatically by generating refined policies that meet objectives. Third, the Butane compiler will target and exploit the benefits of heterogeneous back-end protocols and platforms. Fourth, tools will help network operators infer new high-level configurations from existing low-level configurations and to verify that new configurations are equivalent to old ones. Finally, Butane will support mixed mode (legacy- and high-level network operations) so engineers can migrate their networks slowly over time and test partial deployment on small fractions of their live traffic.

社会各阶层都依赖正常运作的计算机网络。例如，每天，数以百万计的公民通过云在网上订购处方药、支付电费、预订酒店、购买食品杂货，并参与数以千计的活动。但是，如果提供信息的网络关闭，这些服务都不会起作用。此外，现代企业、医疗保健、军队和政府与普通公民一样依赖可靠的网络。许多网络中断是由操作员手动(和错误地)对管理网络设备转发信息的方式的“配置文件”进行编程造成的。虽然配置文件所允许的灵活性至关重要，但网络中断通常是由操作员在每个网络设备上使用数百条低级指令来创建网络范围的策略造成的。由于进行微小配置更改的全球后果非常严重，许多组织甚至需要数周时间来审核即使是微小的更改，从而限制了他们有效应对流量波动、商业机会、安全威胁和硬件故障的能力。这些问题的自然解决方案--类似于过去几十年来软件开发编程语言的趋势，因为程序员已经从机器代码转向Java--是定义更健壮的、更高级的编程语言来实现网络策略。然而，在大规模在工业环境中部署新语言之前，还需要克服技术和实用方面的障碍。特别是，现有的网络范围的策略语言不足以表达许多所需的网络策略，并且通常需要大规模迁移到新的网络平台。因此，该项目的总体目标是克服阻碍高级网络编程语言实际部署的技术挑战。该项目正在开发有效支持和逐步部署高级网络策略所需的核心技术。该项目利用与两家主要云提供商的连接作为一种手段，在真实的工业网络上测试产生的语言和系统，确定采用的实用障碍，并最终在可能的情况下部署技术。该项目建立在PI最近在丙烷上的工作基础上，丙烷是一种新的网络编程语言，允许用户描述域内和域间路由的端到端路径，以及为行业标准BGP协议生成配置的编译器。该项目的成果将以多种方式扩展丙烷以支持实际部署：首先，用户将能够声明设备角色(例如架顶式交换机)和与其相关的连接不变量，以实现简洁的规范。新的编译器将在存在此类声明的情况下验证策略的安全属性，并生成使编译器输出更易于操作员理解的参数化模板。其次，用户将使用一种新的声明性语言指定管理运输成本的财务合同，编译器将通过生成满足目标的精细化策略来自动优化路线。第三，丁烷编译器将瞄准并利用异类后端协议和平台的优势。第四，工具将帮助网络运营商从现有的低级配置中推断出新的高级配置，并验证新配置是否等同于旧配置。最后，丁烷将支持混合模式(传统和高级网络运营)，因此工程师可以随着时间的推移缓慢迁移他们的网络，并在他们的实时流量的一小部分上测试部分部署。

项目成果

Campion: debugging router configuration differences

• DOI: 10.1145/3452296.3472925
• 发表时间: 2021-08
• 期刊: Proceedings of the 2021 ACM SIGCOMM 2021 Conference
• 作者: Alan Tang;S. Kakarla;Ryan Beckett;Ennan Zhai;Matt Brown;T. Millstein;Y. Tamir;G. Varghese

ProbNV: probabilistic verification of network control planes

ProbNV：网络控制平面的概率验证

• DOI: 10.1145/3473595
• 发表时间: 2021
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Giannarakis, Nick;Silva, Alexandra;Walker, David
• 通讯作者: Walker, David

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