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