Programming Languages Meets Programmable Networks

Computer networks do not simply connect machines but run several applications on network devices, such as load balancers, intrusion detection systems, authentication portals, and more. Historically, these applications were black-boxes running on proprietary hardware, but software-defined networking (SDN) now allows anyone to write their programs using open networking protocols (e.g., OpenFlow).  So, what are the right abstractions for programming networks? This talk will try to address this question in three ways.First, we present a syntactic theory of network forwarding called NetKAT, which supports equational reasoning about network-wide behavior. Using NetKAT, programmers can ask and answer questions like, “Can A communicate with B?”, “Does all traffic traverse my intrusion detection system?”, “Is there a loop in my network?”, And so on. Second, we present a fast and efficient compiler for NetKAT. Although several network compilers already exist, they are unusable on even moderately sized networks. Using new data structures and compilation algorithms, our new compiler is two orders of magnitudes faster than prior work and scales to large datacenter networks.Finally, we consider the problem of building a reliable runtime system for NetKAT. NetKAT abstracts away several low-level details of networking hardware. Although this is a boon for the network programmer, the burden now shifts to us to engineer abstractions correctly. We present a Coq-certified runtime system that is proven correct concerning a detailed operational model software-defined networks.

Bio:

Arjun Guha is an assistant professor of Computer Science at UMass Amherst. He enjoys tackling problems in systems using the tools and principles of programming languages. Apart from network programming, he has worked on Web
security and system configuration languages. He received a Ph.D. in Computer Science from Brown University in 2012 and a BA in Computer Science from Grinnell College in 2006.