Developing a mathematical framework to analyze essential internet protocols

How is it that the internet works so well, with billions of users sending millions of gigabytes all together every day? That's because the foundation of the internet is solidly set up. Yet sometimes there are problems on the internet. For example, when certain systems misbehave and disrupt the routing of internet packages.

In the new Verified Reowolf project, researchers are developing a mathematical framework with which to formally analyze essential internet protocols. Hans-Dieter Hiep, affiliated with the Leiden Institute for Advanced Computer Science (LIACS), is the initiator and principal investigator of the project and explains how it works.

Why does the internet work so well, anyway?

"Almost everyone uses the internet every day. People make video calls, stream media, send emails and make digital payments. Already in 2016, global annual internet traffic reached 1 zettabyte or 1 trillion gigabytes."

Hiep explains that the internet is made up of a number of public protocols. "A protocol is an agreement between computer devices that allows connected machines to communicate with each other in a certain way," he says. He gives the internet Protocol (IP) as an example. This is the basic unit of communication on the internet: the package, named after the material postal package.

Hiep explains: "Postal packages go all over the world: people collect them in depots for further shipment and there are various ways to move them between depots, for example by truck, train, ship or plane. In the same way, internet packages are sent around the world. The virtual version of depots are routers, and there are various ways for packages to travel between routers. This can be done via wireless radio, copper cabling or fiber optics."

When a package travels through a network of routers, how does each router along the way know where each package should go?

"Unlike postal packages, you can't always geographically link the destination of a virtual internet package to a router near the destination. Instead, one has grouped routers into so-called Autonomous Systems (ASes). For this, one uses a different protocol, namely the Border Gateway Protocol (BGP)."

Hiep says that within this BGP it is possible to exchange and update routing information between the ASes, so that the internet remains connected worldwide. "This ensures that internet packages can be sent around the world in a fast and efficient manner."

But sometimes problems occur: either by accident or with malicious intent. If certain ASes misbehave, they redirect internet packages to undesirable parts of the network. Or they even disrupt the entire routing on the internet, making service providers massively unavailable.

How is Verified Reowolf connected to these protocols and their potential problems?

"In the new Verified Reowolf project, we are researching and developing a mathematical framework in which we formally analyze essential internet protocols. We use that framework for insecurity discovery. Emerging insecurity is the concept where all individual systems behave correctly, but problems still occur on a global scale. Furthermore, we develop tools that can be used to improve and ensure the quality of computing devices that communicate according to internet protocols. This is important for the long-term stability of the internet, and thus indirectly for everything else we build on top of it in the future."