Loo, Boon Thau University of Pennsylvania CAREER: Towards a Unified Declarative Platform for Composable Verifiable Networks
This 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.
