Formal verification: what it is and why you need it in your network infrastructure

Formal Verification: Confidence in complicated systems

Formal verification

When you step on a 777 to your next business trip or vacation, has a flash of impending doom ever crossed your mind? While it is always good to call your loved ones, rest assured: the odds of your plane crashing are only 1 in 4 million. You have a better chance of being struck by lightning (1 in 3 million) or spending $300 and winning the $656 Million Powerball jackpot (1 in 2 million).

So given how complex airplanes are – hundreds of buttons and handlers in the cockpit controlling tens of thousands mechanical components, plus the complicated and dynamic nature of flight control, both software and operators – why are they so reliable? As engineers, we all know complicated software applications are bound to have bugs: the industry average is 15-50 bugs per 1000 lines of code in software (according to Steve McConnell,  Code Complete).  But autopilot software simply can’t afford to fail, no matter how complex or demanding the situation. Since spot tests with a handful of pre-defined inputs hold no chance to entirely eliminate bugs, aerospace engineers and researchers turn to a dramatically more powerful method, formal verification, to boost the reliability of mission-critical software to near perfection.

Formal verification builds a mathematical model of an application’s behavior and deduces whether certain properties of the software will always hold with an astronomical set of possible input and execution paths—and it does so, amazingly, before the software is actually executed. Returning to the flight control software example, formal verification is capable of answering questions like “is there any possible execution path of the flight control software where the target altitude of autopilot module is incorrectly overwritten (leading to a crash)? ”. Bottom line: formal verification gives you confidence in life-depending and mission-critical systems and software, from airplane safety to Mars rovers to supercomputer chips to life-support medical equipment.

Ramifications for your enterprise network

In the past 15 years, enterprise networks have evolved from the realm of your in-house Geek Squad to the cardiovascular system of your entire business. The performance and reliability of your network is no longer a technical issue—it’s a bottom-line concern. And while enterprise networks have never been more business-critical, they’ve also never been more complex:  it’s now common to see multi-site enterprise networks with tens of thousands of routers and switches with a private data center and campus network on each site, and an MPLS network from different providers stitching all of them together with a galaxy of configuration features in use: VLAN, spanning tree, OSPF, BGP, multicast, MPLS, ACLs, stateful firewalls, load balancers, network virtualization (NSX, ACI or others), VRFs, RIP, and OpenFlow. Worst of all, the configurations and interactions of these components are constantly changing. The odds of human error in this environment becomes not a question of if, but of when, and of how often.

At Veriflow, we share your concern for the mission-critical enterprise network infrastructure. We understand the pressures that these intricacies and complexities place on your network architects and operators. We believe the answer lies in our advanced patented network verification technology. We look at your network’s data plane – in a sense, the “compiled software” of a network – and mathematically verify security and reliability policies against the trillions of possible packets combining complicated behaviors of different protocols.  The result: your network is as reliable as an airplane or a NASA Mars rover.

For more information about the Veriflow solution, please read our white paper.