The internet depends on connections. From buying a friend’s birthday present online to Skyping business meetings with colleagues in Japan, every internet transaction requires that sensitive information be shunted from one place to another in cyberspace. This movement of data relies on networking, the process that controls how routers and other network-related devices, like gateways and firewalls, facilitate the flow of packets of information between destinations.
“Fast networks have been critical to enabling the growth of the internet,” says John Nathan Foster, Computer Science. “Over the last decade, the rise of new web services, cloud computing, and data centers has created new scalability challenges for networks. They need richer functionality. Routers need to be even faster and more flexible.”
A New Way of Building Faster Computer Networks
Traditionally routers were vertically integrated systems, according to Foster. Users bought the hardware, operating system, and software from the same company and were unable to change much. About 10 years ago, a few computer experts started a movement known as Software Defined Network (SDN) architecture to rethink how networks are created. SDN aimed to make the network control directly programmable by using open standards that do not require proprietary software. These open software-based controllers would take the place of the previous vendor-specific devices and protocols that made up networks. SDN also included the need for new computer languages to program the controllers. Foster was immediately interested.
“For the first time in 30 years the whole industry was trying to agree about what machine-level languages we should use for routers and what higher-level things we want to layer on top to express rich network functionality,” he says.
NetKAT, Breaking Up the Programming
Foster and his lab turned their attention to modular programming, the principle that underlies all modern software. “Software does incredibly complex things, but no one programmer has to understand the entire thing at once,” Foster says. “You find ways to break it up into small pieces and then to compose multiple pieces together so you get more complicated behaviors. Networking had rarely been like that. It was clear to me that we should write programs in a modular way, so we started to design a series of languages that offered constructs that could be used to write modular programs.”
From that work came the language known as NetKAT (Kleene Algebra with Tests). NetKAT gives human programmers a break from the tricky and tedious business of writing low-level code to tell each device in the network what to do. “It’s a high-level language for programming network behavior, for telling a network how to process packets,” Foster explains.
“NetKAT is above the level of machine code,” Foster continues. “A lot of other languages are describing things in terms of router primitives. Here, it’s much more abstract. You can say something like ‘Forward packets from here to Cornell Tech and make sure every packet goes through the firewall,’ and the system will generate all the machine-level instructions needed to do that. With high-level languages like NetKAT, the compiler can search for lots of combinations of low-level code that might do a better job than what a human would come up with. When programs get big enough, there’s too much for a human to keep in their head.”
“You can say something like ‘Forward packets from here to Cornell Tech and make sure every packet goes through the firewall,’ and the system will generate all the machine-level instructions needed to do that.”
While creating NetKAT in collaboration with colleagues at Princeton, Foster and postdoctorate Arjun Guha, now at the University of Massachusetts, were excited to discover their mathematical foundations for the language were not new. They were the same as the system Foster’s departmental colleague Dexter C. Kozen had been working on for 20 years. “That was super exciting,” Foster says. “When you’re a mathematician, you’re actually glad to discover what you’re doing is what someone else is doing under a different guise. That means there’s connections between two seemingly different areas. They’re not identical, but every theorem that holds in our system, also can hold in Kozen’s system. This paved a path towards building tools that could automatically prove theorems about programs written in NetKAT.”
Extending NetKAT as Security Checker and More
Not only can programmers use NetKAT to write code, but it can also serve as a general framework into which other existing formalisms can be encoded. This means NetKAT can be used to verify that other configurations of code running proprietary devices are secure by checking the properties of any path a packet takes as it goes through the network, such as connectivity, resilience, isolation, access control, and load balancing. “Having a mathematical system for proving things about network programs is a new idea,” says Foster. A number of companies are interested in NetKAT, with Fujitsu among the first to use the language for a product internally.
With funding from the Office of Navy Research and the National Science Foundation, Foster has been working with Kozen and fellow faculty member Robert D. Kleinberg to create an extension of NetKAT called Probabilistic NetKAT. The researchers want to use the extension to express random algorithms, which are often used for load balancing—spreading data traffic among many paths so that no one path gets overloaded. They hope to refine some of Kleinberg’s foundational theoretical work on randomized routing algorithms, implement them in Probabilistic NetKAT, and then deploy them in the real world. “We’re not there yet, but our hope is that we can explain why some of these algorithms people are using today work well,” Foster says. “When they don’t work well, we want to characterize why they don’t work, and maybe propose new, more robust algorithms instead.”
P4 for Flexible, Secure, Reliable Networks
As part of the effort to recreate networking in the SDN mode, Foster is also a member of an open-source consortium developing a low-level computer language called P4 (Programmable Packet Processing Programs). P4 is conceived as part of the architecture for a new hardware design. Foster is the technical steering committee chair for the language and the co-chair of the language design committee. “I’m trying to get engineers from the major tech companies like Cisco, Google, and Microsoft to agree on what the definition of P4 should be,” Foster says. “It’s a form of industry outreach.”
Many companies have been interested in P4, and last spring AT&T announced they were using it internally in their network. “I’m excited about this,” Foster says. “Right now, there’s no standard language used for packet processing. P4 could fill that space. The design of P4 has some nice features that could make networks more flexible, more secure, and more reliable. If it succeeds and becomes the de facto standard for expressing packet-processing behavior on the internet, it will likely be deployed on millions of devices around the world for decades to come. The chance for impact is huge.”