PDF Basket
Faulty networks significantly affect daily life. Failures in data centres disrupt mission-critical applications, while airline network failures frequently ground planes.
Routers are an essential piece of this infrastructure, exchanging data between computer networks. Each router comprises a program known as a control plane, which organises the data’s path to its destination, and a dataplane, which processes the traffic itself. Top-end devices forward 52 terabytes of traffic every second.
“It’s a bit like a post office, with routers reading data packet ‘headers’ like addresses on envelopes, to determine the intended destination,” says Costin Raiciu from the University Politehnica of Bucharest in Romania.
Until recently, the dataplane program was written into the router’s hardware, limiting it to predetermined functions. This meant that any changes to this code required network device manufacturers – such as Cisco, Broadcom and Intel – to redesign the underlying silicon, presenting a costly barrier to upgrades.
Nowadays, the router dataplane is programmable using languages such as P4. Intel’s Tofino and Broadcom’s Trident chips are examples of routers with programmable dataplanes.
“While programmable routers offer immense flexibility, they can still end up with bugs that elude programmers and can disable networks,” explains Raiciu, the coordinator of the EU-funded SafeNet project.
Building on the preceding (CORNET) project’s research, Raiciu’s team had developed a tool called bf4 for finding bugs in P4 programs and automatically fixing them, making it easier for non-experts to use. SafeNet explored opportunities to expand the technology and make it available to interested parties.
“Our bug detecting solution is available open-source on GitHub and is, as far as we know, the only publicly available tool for this purpose,” remarks Raiciu, a co-founder of Correct Networks, the project host. “Our market study persuaded us to expand into the development of commercial software to optimise data centre networks.”
Verifying before deployment
“P4 is particularly bug-prone because it’s a low-level programming language, much like the C programming language in the software world,” adds Raiciu.
The most common P4 bugs are with inaccurate header values which cause application and/or router crashes and can render network devices vulnerable to hacking.
Many bugs can be caught if the data packets and paths are verified before deployment, but this relies on fast verification tools (minutes or less) that avoid false alarms.
The bf4 tool uses a technique called ‘verification-condition generation’, coupled with a novel inference algorithm, to detect non-sensical control plane entries, removing false positives.
On the largest P4 program (switch.p4, with 6 000 lines of code), bf4 found around 160 bugs in two minutes. When its ‘inference’ algorithm was activated, most of these bugs turned out to be false positives, reducing the number of potential bugs to 15.
“The P4 code is then either manually fixed by programmers, or bf4 can change the code automatically,” says Raiciu.
Pivoting from bug detection to optimisation
“bf4’s ability to offer offline verification of a P4 program is extraordinary and is testament to both the simplicity of the P4 language itself and progress in computer science and systems theory,” remarks Raiciu.
SafeNet’s market study with potential customers made it clear that uptake of programmable routers remains low, with few programmers using P4 in situ.
“So, we decided to make bf4 available open-source and focus on creating and commercialising software that optimises data centre network performance,” explains Raiciu. “We’ve already patented this technology and after much interest from key players such as Orange and Microsoft, now have a clear plan to bring the product to market.”