How Formal Verification Can Thwart Change-Induced Network Outages

How Formal Verification Can Thwart  Breaches

Formal verification is not a new concept. In a nutshell, the process uses sophisticated math to prove or disprove whether a system achieves its desired functional specifications. It is employed by organizations that build products that absolutely cannot fail. One of the reasons NASA rovers are still roaming Mars years after their intended lifespan is because the correctness of their software was mathematically verified before deployment. Similar trusted 24/7/365 technology is embedded into mission-critical airplane flight controls, medical devices, and military defense systems that are too important to malfunction.

Recently, a team of computer science professors and Ph.D. students in the EnterpriseWorks incubator at the University of Illinois at Urbana-Champaign (UIUC) discovered how that same methodology can be applied to bulletproof today’s most complex networks to help prevent change-induced outages and breaches. Mathematical network verification is long overdue. Even if only 2% of modifications to a network’s configuration result in a change-induced outage or vulnerability, let’s put that in perspective: would you board an airplane if you knew that two out of 100 planes could fall out of the sky? Of course not. Why should we expect less from our networks? With so much sensitive data at stake, networks have to be as trustworthy as mission-critical systems and infrastructure.

Why Networks Fail

network

Four key factors have made network infrastructure particularly vulnerable to breaches and outages. First, when you factor in the cloud, virtualization, the move to software-defined networks (SDN), and mobile and IoT devices, you’ll quickly see that networks have become incredibly complex to manage. Second, every network change leaves an opening for something to possibly be misconfigured. By some estimates, operators of large enterprise or service provider networks make approximately 1,000 changes per month. Third, humans are a constant and unpredictable factor. Gartner analyst Donna Scott has noted that “80 percent of unplanned downtime is caused by people and process issues, including poor change management practices, while the remainder is caused by technology failures and disasters.”

And finally, there is poor policy management. According to the consulting firm Protiviti, one out of three enterprises and Service Providers lacks policies for IT, information security and data encryption, while 71 percent lack critical knowledge of which policies to institute to mitigate vulnerabilities and disruption. The fact is, most enterprises do not know what their network actually looks like at the deep infrastructure level, whether it is operating as it should be, and what Vulnerabilities are lurking in the network. As a result, making any change to the network – even a day-to-day modification like changing access control rules or adding a device – is a time-consuming, manual and risky process. And broad architectural changes such as moving to a hybrid cloud or deploying SDN can be daunting projects.

How Formal Verification Works

Formal verification tries to predict the future: will my design work when I deploy it in the field? Will it always work, no matter what unexpected inputs or attacks are thrown at it? For example, a software application designer might want to know that her code will never crash or that it will never execute certain functions without an authorized login. These are simple, practical questions – but answering them is computationally challenging because of the enormous number of possible ways code may be executed, depending on the inputs and environments it interacts with. Decades of research advances in formal verification algorithms have led to the ability to rigorously answer such questions for certain kinds of software and critical systems.

Can we understand the behavior of complex enterprises with the same mathematical rigor? In a network, we want to understand whether the design meets network-wide data-flow policy: Is my network correctly segmented to protect against lateral movement by attackers inside my perimeter? Will my web services be available even after a router interface failure? Today, these questions are addressed through manual spot-checks, auditing and change-review boards that might take weeks to provide answers, all of which still leave plenty of room for error. In contrast, mathematical network verification reasons automatically about the possible behaviors of the network.

Achieving that analysis required several innovations:

  • First, it required rigorous understanding of devices’ data-flow behavior, down to the data plane instructions, which are the “machine code” of the network.
  • Second, it required sophisticated, novel reasoning algorithms and compact data structures that can efficiently explore the exponentially large number of possible packets that may be injected at thousands or tens of thousands of devices and ports in the network.

Using mathematical network verification can help enterprises prevent the outages and breaches that lead to astronomical losses, both informational and financial. Unlike techniques such as penetration testing and traffic analysis, mathematical network verification performs exhaustive analysis of all possible data-flow behavior in the network, before it happens – before vulnerabilities can be exploited, and without waiting for users to experience outages. If there is a network policy violation, verification will find it and provide a precise identification of the vulnerability and how to fix the flaw. The underlying technology allows for millisecond-level analysis of security policies, enabling real-time alerting and policy enforcement, and can provide mathematical evidence that the network is correct, giving organizations the confidence to implement changes to their infrastructure.

Real-time Situational Awareness

Depending on how an organization applies mathematical network verification to its network, the technology can collect a real-time situational awareness of a network’s data-plane state (the lowest and most foundational information in a network device), develop a flow model of the entire network and perform a rigorous analysis of security policies in real time to detect vulnerabilities and policy violations.

In a world where a network intrusion can result in billion-dollar losses, brand damage and outages of critical functionality, mathematical network verification represents a significant step towards improving overall network health and preventing network outages and breaches. It is the only technology available today capable of providing rigorous, real-time analysis at the deep data-plane level of a complex network, and it produces a level of confidence not attainable by other approaches.

Mathematical network verification is a unique technology that has already demonstrated success in multiple Fortune 500 and Government networks. We will likely see quick adoption of the technology when organizations discover how quickly and dramatically it improves network security and resilience, making change-induced breaches and outages a thing of the past.

By Dr. Brighten Godfrey

New York

From Y2K To NYC Parking Meters: Have We Learned Anything About Complacency In Cybersecurity?

Cybersecurity Complacency This past January – in what seems like a different world now – a story briefly hit the headlines and was seen as more of a quirk than a threat. It was soon ...
Gary Bernstein

AWS General Release of Amplify Flutter

The AWS General Release of Amplify Flutter The Amazon Web Service has announced that the Amplify Flutter is now generally available in a way to help make flutter apps easier and more accessible. According to ...
Digitizing Contact Center to Reduce Call Volume by 30% and Improve NPS

Digitizing Contact Center to Reduce Call Volume by 30% and Improve NPS

Digitizing Contact Center With a Net Promoter Score (NPS) average of 24, telecom holds the lowest industry average according to the NPS Benchmarks Report. Operational inefficiencies in contact centers play a major role in the low ...
Jim Fagan

The Geopolitics of Subsea Connectivity

Subsea Connectivity Digital transformation and the migration of data and applications to the cloud is a global phenomenon. While we may like to think that the cloud knows no borders, the reality is that geopolitics ...
Gary Bernstein

Exposed Data From 21 Million VPN Mobile Users

Exposed Data From 21 Million VPN Mobile Users The data and credentials from 21 million mobile VPN users were found for sale last week in an internet forum. A cyber thief posted the credentials for ...

PROXY SERVICES

The CloudTweaks technology lists will include updated resources to leading services from around the globe. Examples include leading IT Monitoring Services, Bootcamps, VPNs, CDNs, Reseller Programs and much more...

  • Smartproxy

    Smartproxy

    Smartproxy is a rising star in the constantly growing proxy market. Smartproxy offers awarded customer service, impressive performance, and is serious about your anonymity (yes, cybersecurity matters). The latest features developed by Smartproxy are 30 minute long sticky sessions and Google Proxies. Rumor has it, the latter guarantee 100% success rate

  • Bright Data

    Bright Data

    Bright Data’s network is one of the most robust of its kind globally. Here are its stark advantages: Extremely stable connection for long sessions (99.99% uptime guaranteed). Free to integrate with our Proxy Manager which allows you to define custom rules for optimized results. Send unlimited concurrent requests increasing speed, cost-effectiveness, and overall efficiency.

  • Rsocks

    Rsocks

    RSocks team offers a huge amount of residential plans which were developed for plenty of tasks and, most importantly, has been proved to be quite efficient. Such variety has been created on purpose to let everyone choose a plan for a reasonable price, online, rotation and other parameters.

  • Storm Proxies

    Storm Proxies

    Storm Proxies' network is optimized for high performance and fast multi-threaded tools. You get unlimited bandwidth. No hidden costs, no limits on bandwidth. Try Storm Proxies 100% Risk Free. If you are not happy with the service email us within 24 hours of purchase and we will refund you.