Seeing the Future with Mathematical Network Verification

Knowing how a network will react in a given situation is critical. Hidden policy violations can lead to disaster. According to a report by Symantec, a single API bucket misconfiguration led to over 70 million leaked records in 2018 alone. Accounting for how every single change will affect a network is time-consuming and cost-ineffective. However, organizations are gambling with their data and IT if they implement a change and wait to see what happens.

This is where mathematical model-based network verification steps in. It paints an accurate picture of how different configurations will affect a network. This includes how it will forward packets, where security policies and application requirements are violating protocol, and so on.

Math in, Math Out

Network verification is the process of exhaustively analysing a network’s design and seeing if it adheres to its intended function and an administrator’s policies. Don’t confuse it with traffic monitoring; instead, it looks at the mechanisms behind traffic and packet routing. It points out design flaws and configuration issues that would cause outages, bottlenecks, or policy violations.

Mathematical verification takes this a step further by creating an intelligent, automated process to isolate issues within the network. It is a predictive model, meant for network operators to glimpse into the possibilities of what their network might do when they change it.

It’s also an accurate way to verify the current status of a network, says Peyman Kazemian, co-founder of Forward Networks and one of the developers of Forward’s mathematical models for their network assurance product. 

Kazemian developed Forward’s model while he was studying for his PhD at Stanford University in 2013, finding that modern networks, while complex, still operate by the basic principles of bitwise match and action. The key is developing the correct formula to account for the variables within the network, which is done by identifying the key pieces of network functionality within each device in the network and mapping them to the correct set of matches and actions.

“Once we’ve done that, then voila: You can track the changes to the header spaces of packets as those packets go through network devices,” Kazemian said. “The validation platform provides an accurate mathematical model of how a network is processing and forwarding packets.”

The principle is fairly simple. Networks are built on mathematical formulas in order to forward packets. The heart of the issue is finding what variables change those formulas, and applying them in the same way to a projected set of models. 

“The first step in making tools for network verification and debugging is to create a simple model for the forwarding functionality of the network that abstracts away the complexities of understanding the forwarding state,” Kazemian wrote in his 2013 thesis. “One observation is that packet headers, despite carrying multiple protocols, are just sequences of bits. Networking boxes, despite all their complexities, simply rewrite and forward packet headers.”

While the models that Kazemian developed have since changed as networks have evolved, the principle remains the same: Math in, math out.

Predicting the Unpredictable

Operators need to evaluate networks on the whole. Looking at individual parts, Kazemian said, and modeling how they operate in a vacuum isn’t enough.

“A network is definitely more than the sum of its parts,” he said. “As you add more nodes, there’s cross-product interaction between these networking elements, and you have to model that. You need algorithms that do not blow up when you go from a hundred nodes to 2,000 to 10,000 nodes. That’s because these things do not scale linearly.”

While network verification and assurance is a moving target for many organizations, having a mathematical model can paint the most accurate picture of a network when applied, Kazemian said, and is one of the most reliable ways to ensure that new changes won’t pose a risk. 

This is especially true now, as organizations are learning the consequences of being underprepared. IT scaling has been a major issue with the shift to remote work in wake of COVID-19. While it’s not something most organizations could have predicted, the issue of scaling is something a mathematical model could have. 

Network assurance is more important than ever, as networks are rapidly and constantly changing. With new pressures from remote working and new application developments and requirements, it’s key to be able to quickly glean the impact of a new configuration in the network. Even if this is done remotely, it can increase the network agility and reduce the risk of outages, errors, and policy violations.

“You have a completely different sort of access model to your infrastructure,” Kazemian said.  “Network operators that are operating these pieces are no longer in the same physical location, so providing a singular view so that they can quickly understand where the very particular problem is, is [critical.]”

Read the latest about Forward on our blog

crossmenu linkedin facebook pinterest youtube rss twitter instagram facebook-blank rss-blank linkedin-blank pinterest youtube twitter instagram