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）的背景下，研究人员已经开发了Frenetic，Pyretic，NetKAT网络编程语言。 这些DSL通常由形式语义支持，形式语义为用它们编写的程序（网络）提供了一些正确性保证。 然而，DSL尚未进入实际的网络部署。 采用的一个关键障碍是，这些语言往往在孤岛中使用，与设计，实现和部署网络的过程脱钩。 为了应对这些挑战，本研究提出了DEFIND，这是一个能够实现迭代网络设计并统一指定，实施，部署，验证和调试网络的整个工具链的平台。拟议的研究包括以下三个紧密相连的任务，包括DEFIND。所有这三个任务都使用Network Datasheet声明性网络语言作为统一的中间语言。第一个研究任务是发展静态分析技术来分析网络协议的正确性。当属性不成立时，DEFIND提供有意义的反馈以帮助程序调试。 第二个研究任务利用动态出处跟踪来生成反例，并在第一个研究任务中的静态分析无法提供结论性结果时提出潜在的修复建议。 最后一个任务提供了一个新的API，用于对网络进行编程，由此网络运营商使用示例行为来指定网络的期望功能。DEFIND旨在从这些示例中自动生成网络规范。前两个任务的结果被应用到细化的例子，并产生正确的网络specifications.The更广泛的影响，这个建议在于一个统一的框架，结合了正式的分析和实现的网络协议在设计，分析和实施阶段的发展。DEFIND旨在使网络运营商，即使他们没有受过编程培训，也能直接设计和配置新的网络协议。PI将共同教授一个研究研讨会，研究正式方法和编程技术在网络协议设计领域的应用。