CAREER: Towards a Unified Declarative Platform for Composable Verifiable Networks

CNS-0845552 Loo，宾夕法尼亚大学Boon Thau CAREER：为可组合的可验证网络建立统一的声明性平台这项研究项目研究了一种声明性、可组合和可验证的网络基础设施--能够在现有网络之间桥接，按层堆叠，动态更改层或网桥，并允许通过新功能进行快速扩展。提议的基础设施利用声明性联网，这是一种声明性的、受数据库启发的可扩展基础设施，它使用查询语言来指定行为。这种方法提供了紧凑性、安全性、可组合性以及进行正确性检查的可能性。拟议研究的第一个贡献是探索网络组合的机制，其中现有网络的不同部分或元素通过声明性规范组合在一起，以创建具有新功能的新网络。第二个贡献利用声明性框架和基础设施提供的动态组合能力来实现可适应的混合协议，即基于不断变化的应用需求和网络条件组合几个现有协议而构建的协议。第三篇文章探索了一种验证陈述性网络及其组成的性质的正式方法。将探索三种验证技术：数据库查询语言的静态分析，利用声明性网络与逻辑程序的连接的定理证明技术，以及运行时验证。这项提议的教育目标是一个综合的研究和教学计划，强调以数据为中心和正式的方法方法来实现联网。这一建议的智力优势是开发了一个统一的声明框架，用于指定、组成、正式验证和实施网络。这一提议的更广泛影响在于能够利用虚拟化和覆盖等技术实现的网络多样性实现和创建新功能。

CNS - 0845552 Loo, Boon Thau University of PennsylvaniaCAREER: Towards a Unified Declarative Platform for ComposableVerifiable NetworksThis research project investigates a declarative, composable and verifiable network infrastructure -- one capable of bridging between existing networks, stacking them in layers, dynamically changing the layers or bridges, and allowing for rapid extensibility with new functionalities. The proposed infrastructure utilizes declarative networking, a declarative, database-inspired extensible infrastructure that uses query languages to specify behavior. This approach provides the benefits of compactness, safety, composability, and the potential for correctness checks.Intellectual Merit. The first contribution of the proposed research explores mechanisms for network composition where distinct parts or elements of existing networks are combined via declarative specifications to create a new network with new functionalities. The second contribution leverages the dynamic composition capabilities provided by the declarative framework and infrastructure to enable adaptable hybrid protocols, i.e. protocols built from combining several existing protocols based on changing application needs and network conditions. The third contribution explores a formal methodology towards verifying the properties of declarative networks and their compositions. Three verification techniques will be explored: static analysis of database query languages, theorem proving techniques that leverages declarative networking's connection to logic programs, and runtime verification.Broader Impact. The education goal of this proposal is an integrated research and teaching program that emphasizes data-centric and formal methods approaches towards networking. The intellectual merit of this proposal is the development of a unified declarative framework for specifying, composing, formally verifying, and implementing networks. The broader impact of this proposal lies in the ability to enable and create new functionalities from the network diversity that technologies such as virtualization and overlays make possible.