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

Jen Klostermann
The Fintech Landscape The Nitty Gritty Although the COVID-19 pandemic has highlighted its existence, most of us have been using fintech in some form or another for quite some time. It’s a big part of ...
Steve Prentice
The Era of Microlearning Becoming employable and then staying employable requires ongoing, up to date knowledge, and this can become something of a dilemma. Many of us grew up with a traditional understanding of the ...
Louis
More CISOs will have to deliver revenue growth to protect their budgets and grow their careers in 2023 and beyond, and a core part of that will be getting multicloud security right. It’s the most common infrastructure strategy for ...
David Discenza
Four Ways to Improve Cybersecurity (Updated: December 9th, 2022 ) Cyber-attacks on businesses have become common place. In fact, it’s estimated that a cyber-attack occurs every 39 seconds. Who are the targets of these attacks? ...
Cybersecurity Bootcamps To Help Build Your Career
Cybersecurity Bootcamps We've discussed the importance of training and the hiring of cybersecurity professionals many times on CloudTweaks over the past 10+ years. Now more than ever as the world enters into a dark era ...
Stacey Farrar
Modern Auth and Exchange Online Migrations Microsoft has phased out Basic Authentication (Basic Auth), replacing it with Modern Authentication (Modern Auth) to provide increased protection and user security. Through this, Microsoft has turned off Basic ...
Maxim Melamedov
Trouble is Brewing Cloud Paradise - 2023 Will Determine Company's Long-Term Plans for Cloud Use The relationship between developers and the cloud was practically love at first sight. For years, migration to the cloud in ...
Drew Firment
Stop Focusing on Cloud Adoption and Start Focusing on Cloud Maturity For the past several years, most organizations have made it their priority to shift much of their applications and data from on-premises to the ...
Disaster Plan.png
David Fletcher Blown Image
Twitbook.png
Disaster Recovery Plan.png

PLURALSITE

Pluralsight provides online courses on popular programming languages and developer tools. Other courses cover fields such as IT security best practices, server infrastructure, and virtualization. 

(ISC)²

(ISC)² provides IT training, certifications, and exams that run online, on your premises, or in classrooms. Self-study resources are available. You can also train groups of 10 or more of your employees.

CYBRARY

CYBRARY Open source Cyber Security learning. The world's largest cyber security community. Cybrary provides free IT training certificates. Courses for beginners, intermediates, and advanced users are available.