NeTS: Medium: Collaborative Research: DEFIND: DEclarative Formal Interactive Network Design

NeTS：媒介：协作研究：DEFIND：声明式形式交互网络设计

• 批准号: 1513961
• 负责人: Limin Jia
• 金额: $ 40万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-10-01 至 2021-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1513961&HistoricalAwards=false
• 关键词: NeTS; Medium; Collaborative; Research; DEFIND

Networks are complex systems that unfortunately are ridden with errors, which may lead to disruption of services with grave consequences. One approach to eliminating errors is to construct a formal model of the network and verify the correctness properties. However, extracting models from existing networks is often beyond what network operators can do. To lower the complexity of network design and verification, an alternative approach is to use high-level abstract domain specific languages (DSLs) to define networks. For instance, in the context of Software Defined Networks (SDN), researchers have developed Frenetic, Pyretic, NetKAT network programming languages. These DSLs are often backed by formal semantics, which provide some correctness guarantees of programs (networks) written in them. However, DSLs have yet to make inroads into practical network deployments. One key barrier to adoption is that these languages tend to be used in silos, decoupled from the process of designing, implementing, and deploying the networks. To address these challenges, this research proposes DEFIND, a platform that enables iterative network design and unifies the entire toolchain of specifying, implementing, deploying, verifying and debugging networks.The proposed research includes the following three tightly connected tasks that comprise DEFIND. All three tasks use the Network Datalog declarative networking language, as the unified intermediary language. The first research task develops static analysis techniques to analyze the correctness properties of network protocols. When properties do not hold, DEFIND provides meaningful feedback to aid program debugging. The second research task leverages dynamic provenance tracking to generate counter-examples and suggest potential fixes when static analysis in the first research task cannot provide conclusive results. The final task provides a new API for programming networks, whereby a network operator specifies the desired functionality of the network using example behavior. DEFIND aims to automatically generate network specifications from these examples. Results from the first two tasks are applied to refine examples and generate correct network specifications.The broader impact of this proposal lies in the development of a unifying framework that combines both formal analysis and implementation of network protocols during design, analysis, and implementation phase. DEFIND aims to enable network operators, even if they are not trained in programming, to directly design and configure new network protocols. The PIs will co-teach a research seminar that investigates the application of formal methods and programming techniques in the domain of network protocol design.

网络是复杂的系统，不幸的是被错误驱逐出境，这可能导致服务的破坏，并带来严重后果。消除错误的一种方法是构建网络的形式模型并验证正确性属性。但是，从现有网络中提取模型通常超出了网络运营商可以做什么。 为了降低网络设计和验证的复杂性，另一种方法是使用高级抽象域特定语言（DSL）来定义网络。例如，在软件定义的网络（SDN）的背景下，研究人员开发了疯狂的，发热的，Netkat网络编程语言。 这些DSL通常得到正式语义的支持，这些语义提供了一些编写的程序（网络）的正确性保证。 但是，DSL尚未进入实际网络部署。 采用的一个关键障碍是，这些语言倾向于在筒仓中使用，与设计，实施和部署网络的过程脱钩。 为了应对这些挑战，这项研究提出了Defind，该平台可以使迭代网络设计并统一指定，实施，部署，验证和调试网络的整个工具链。拟议的研究包括以下三个紧密连接的任务，这些任务构成了Fafind。这三个任务都使用网络数据索语声明网络语言作为统一的中介语言。第一个研究任务开发了静态分析技术来分析网络协议的正确性属性。当属性不存在时，Defind提供有意义的反馈来帮助计划调试。 第二项研究任务利用动态的出处跟踪来生成反例，并建议在第一个研究任务中的静态分析无法提供结论性结果时进行潜在修复。 最终任务为编程网络提供了新的API，通过示例行为，网络运营商指定网络的所需功能。 Defind的目的是从这些示例中自动生成网络规格。前两个任务的结果用于完善示例并生成正确的网络规格。该提案的更广泛影响在于开发一个统一框架，该框架在设计，分析和实施阶段期间将正式分析和网络协议的实施结合起来。 Defind的目的是使网络运营商（即使未经编程中的培训）可以直接设计和配置新的网络协议。 PI将共同讲授一个研究研讨会，该研讨会研究正式方法和编程技术在网络协议设计领域中的应用。