A (Co)algebraic Approach to Programming and Verifying Computer Networks

316 pagesAs computer networks have grown into some of the most complex and critical computing systems today, the means of configuring them have not kept up: they remain manual, low-level, and ad-hoc. This makes network operations expensive and network outages due to misconfigurations commonplace. The thesis of this dissertation is that high-level programming languages and formal methods can make network configuration dramatically easier and more reliable. The dissertation consists of three parts. In the first part, we develop algorithms for compiling a network programming language with high-level abstractions to low-level network configurations, and introduce a symbolic data structure that makes compilation efficient in practice. In the second part, we develop foundations for a probabilistic network programming language using measure and domain theory, showing that continuity can be exploited to approximate (statistics of) packet distributions algorithmically. Based on this foundation and the theory of Markov chains, we then design a network verification tool that can reason about fault-tolerance and other probabilistic properties, scaling to data-center-size networks. In the third part, we introduce a general-purpose (co)algebraic framework for designing and reasoning about programming languages, and show that it permits an almost linear-time decision procedure for program equivalence. We hope that the framework will serve as a foundation for efficient verification tools, for networks and beyond, in the future