research
My research centers around designing and building manageable (network) systems by borrowing elegant ideas from formal methods, databases, knowledge representation and reasoning, logic-based artificial intelligence, and more.
enabling agile network management with logic programming
The networking community is currently undergoing an exciting transition from guess-work protocols to disciplined software: Most research efforts involve adapting formal methods, often assuming a clean-slate, stand-alone, closed system architecture, for networking, utilizing highly optimized programming and reasoning tools tailored for specific problems. To tackle challenges that do not readily fit into these techniques, this project proposes rapid prototyping by a general logic programming platform. The key observation is that most ``unconventional’’ problems in networks arise from uncertain and asynchronous events, multiple stakeholders and non-expert users, and diverse requirements that are ad-hoc and ever-changing. Many of these issues mirror those extensively studied in logic programming and its many fruitful application domains. As a first step to materialize this insight and to show the feasibility of using logic programming as a rapid prototyping tool, we develop (1) a general model for networks under uncertain and asynchronous events by extending the relation structures, addressing a challenge in existing network verification; and (2) a general network transformation system by exploiting the meta-logical feature of logic programming, subsuming earlier specialized network tools.
We emphasize that while a complete and final solution to formally managed networks is beyond the scope of this paper, we hope rapid prototyping with logic programming can pave the way to accelerate the migration from guesswork to formally managed networks.
- Structural Semantics Management: an Application of the Chase in Networking MASCOTS23 [paper] [slides]
- Faure: A Partial Approach to Network Analysis, HotNets 2021 [paper] [slides]
- Internet Routing and Non-monotonic Reasoning LPNMR 2019 [paper] [slides]
database-defined networking
Software-defined networking (SDN) provides an unprecedented opportunity to exercise computing principles in simplifying networking practice. Indeed, many salient SDN features — central control and programming interfaces — are enabled by principles from the fields of programming language, operating systems, and distributed systems. While these principles have produced a variety of programming abstractions that drastically improve networking practice, reducing the complex distributed protocols to simpler centralized programs, there is little consensus on what are the right abstractions. Moreover, network architects today need to combine heterogeneous data sources — network forwarding rules, data flow and QoS metrics, host intrusion alerts, and so on — to produce a cohesive view of the network and investigate problems. To tackle the challenging network abstraction and integration problem, this project will explore the computing principle — a principle blessed with decades of fruitful theories and commercial success, yet surprisingly under-investigated in SDN — of database.
ravel: a realization
- Ravel is now open source, http://download.ravel-net.org
- companion site, http://ravel-net.org
- github organization, https://github.com/ravel-net
publications
- position paper [SOSR’16]
- abstraction and orchestration: [SOSR’15 position paper] [SOSR’15 poster] (keynote) [overview]
- concurrency control: [ONS’14 position paper]
networking and automated reasoning
synthesizing dynamic network controller
The few existing synthesis work on network control today are about translating a static snapshot of high-level control policy into the actual control configurations that process traffic. However, networks are dynamic and the policies are by nature reactive: the policies are reacting to the constantly changing network (its configurations states and the live traffic being processed). To accommodate such dynamic policies, we formulate network control as a two-player temporal game: the controller and the dynamic network become two players engaging in a game, the goal is to find a winning strategy for the controller player such that no matter what moves the dynamic network take, the controller ends up in a winnning state defined by some temporal properties.