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

点击翻译按钮获取中文摘要

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.