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 Datalog 声明性网络语言作为统一的中介语言。第一个研究任务开发静态分析技术来分析网络协议的正确性属性。当属性不成立时，DEFIND 会提供有意义的反馈来帮助程序调试。 第二个研究任务利用动态来源跟踪来生成反例，并在第一个研究任务中的静态分析无法提供结论性结果时提出潜在的修复建议。 最终任务为网络编程提供了一个新的 API，网络运营商可以使用示例行为来指定所需的网络功能。 DEFIND 旨在从这些示例中自动生成网络规范。前两项任务的结果用于完善示例并生成正确的网络规范。该提案的更广泛影响在于开发了一个统一框架，该框架在设计、分析和实现阶段将网络协议的形式分析和实现结合起来。 DEFIND 旨在使网络运营商即使没有接受过编程培训，也能够直接设计和配置新的网络协议。 PI 将共同举办一个研究研讨会，研究形式化方法和编程技术在网络协议设计领域的应用。