This article was published on January 9, 2018

Formal verification: From spaceships to the corporate network


Formal verification: From spaceships to the corporate network

According to IDC, by the end of 2017 two-thirds of the CEOs of Global 2000 companies will have digital transformation at the center of their corporate strategies. The agile and resilient business is going to be built on the agile and resilient network; and the network of the future certainly extends beyond an enterprise’s own local data centers and into the cloud.

Surprisingly, unlike storage and compute which has been virtualized for a decade, only recently have we seen significant innovation in networking technology. The innovation makes networks easier to manage as well as faster, more intelligent and now, capable of identifying issues before they emerge. Network functions virtualization (NFV) and software-defined networks (SDN) are enabling a new level of programmability, but networks are still a lagging part of infrastructure when it comes to operational flexibility.

The latest breakthrough to address this is formal verification, which enables proactive assurance that the network and business are online and secure. This is a game changer for a part of the infrastructure that traditionally has not always moved as quickly as other technologies.

What is formal verification?

Formal verification uses mathematics to verify the correctness of an underlying system in relation to its specification. In networking, this means network personnel can use formal verification to verify if the network is going to behave as intended. With a dynamic map of the entire network, they can evaluate everything that can possibly go wrong and prevent disasters BEFORE they actually happen.

Sound like science fiction? It’s science, but it’s hardly fiction: NASA has used formal verification in its Mars rovers before launch to mathematically verify all possibilities of what could go wrong on the Martian landscape. This verification allowed the rover’s creators to proactively identify issues and figure out technical workarounds before any catastrophe could happen millions of miles away.

Today, in addition to NASA, organizations such as IBMMentor, and Intel have employed formal verification in everything from space exploration to defense systems, to processor design, to other electronic devices that cannot afford to fail. Getting these products wrong in any way would scuttle the project or cost millions in rework, and there is similar risk/cost at stake with an enterprise network.

Now, formal verification is entering networking on a global scale. Among the first products taking advantage of this technology and hitting the market are Continuous Network Verification platforms whose underpinnings are akin to AI, and perform advanced automated reasoning to predict all possible behavior that can occur in the network and verify whether it meets the business goals. 

The end solution eliminates network outages and vulnerabilities that can lead to astronomical losses. When something can’t go wrong, this is technology companies need to deploy.

Formal verification and next-generation networking technologies

Few networks in use today were designed end to end to accommodate growth and next-generation technologies such as SDN and NFV. Rather, most were cobbled together to meet various needs; today, they are messy, Frankenstein-like collections of hardware and software that do not address business objectives such as ensuring compliance or securing data.

The result is networks that are difficult to manage and that provide only limited visibility into where problems are occurring. This makes it difficult to fix problems, much less prevent them in the first place.

What’s more, recent networking technologies such as virtualization, SDN and NFV, which were designed to improve operations and network performance, have made networks even more complex. Add to that cloud services and multi-vendor environments, and it’s easy to see why networks have become one of the most difficult parts of an IT infrastructure to manage effectively.

A recent survey from Dimensional Research found 97 percent of respondents admitted that human error was a factor to blame for their network outages. Complexity and change are the underlying causes. Network ops just cannot verify the entire network every time a change is made. And when an error is made that causes a network failure, there are signification financial ramifications around both the cost of repairing the damage, to the loss of customers and brand reputation. AT&T, Customs Boarder Protection, Southwest Air, and Square have all recently suffered high-profile network outages that can be attributed to human error.  

Human-induced network issues will happen more frequently as networks become even more complex due to expansions into the cloud and digital transformation. Automation can help, but even it cannot solve every complex networking problem that arises, and unchecked automation may even compound this problem.

Formal verification is connected to a larger methodology called intent-based networking (IBN). Continuously verifying that the network matches the intent of the business is a critical component of any IBN system. If the intent is not being met, the system can take corrective actions automatically, such as adding or removing capacity, or preventing changes from occurring. Although intuitive networks are on the horizon, verification is enabling business today.

Companies such as Veriflow and Intentionet are using formal verification in their intent-based networking solutions. Cisco Systems also has made product announcements in the area of intent-based networking, and Juniper Networks is now working on intent-based networking technologies.

Conclusion

Today’s dynamic business requires an infrastructure built for flexibility and agility, yet networks are often opaque and may be locked down due to operational uncertainty. Formal verification and intent-based networking are bringing operational simplicity to enterprise networks and enable organizations to remediate issues before they surface and head off problems before they happen.

Get the TNW newsletter

Get the most important tech news in your inbox each week.

Also tagged with