CLOUDTWEAKS CONTRIBUTOR PROGRAM

Join the CloudTweaks thought leadership contributor program which includes a customized profile, branded identity page, newsletter marketing, social amplification and more...

The program is currently available to consultants, influencers or executive level contributors.

Brighten Godfrey

How Formal Verification Can Thwart Change-Induced Network Outages and Breaches

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.

shutterstock_131120717

(Image Source: Shutterstock)

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

Brighten Godfrey

Dr. Brighten Godfrey has conducted research in networked systems and algorithms for more than a decade; his work has led to the development of novel architectures and systems for Internet routing, data-center networking, high-performance data transport and network data-plane verification. He has also advanced the theoretical analysis of network algorithms.

In 2015, Dr. Godfrey received the ACM SIGCOMM Rising Star Award in recognition of outstanding research contributions, including contributions to network verification. Dr. Godfrey was awarded the Alfred P. Sloan Research Fellowship in 2014 and has also received the University of Illinois at Urbana-Champaign (UIUC) Dean’s Award for Excellence in Research and the National Science Foundation CAREER Award. He was a Beckman Fellow at the UIUC Center for Advanced Study in 2014-2015 and has served as program committee chair of several academic conferences.

Dr. Godfrey continues to advise young researchers in his role as associate professor of computer science at UIUC and is co-instructor of a popular Coursera course, Cloud Networking. He holds a Ph.D. in Computer Science from the University of California, Berkeley.

View Website
The Lighter Side Of The Cloud - Whoops!
The Lighter Side Of The Cloud - Microsoft Updates
The Lighter Side Of The Cloud: Intelligence
The Lighter Side Of The Cloud - Resistant
The Lighter Side Of The Cloud - Cloud Metaphor
Driving Transformation? It is possible to predict the future.

Driving Transformation? It is possible to predict the future.

Driving Transformation Previously, I wrote about the criticality of defining the Vision for your transformation - what is your real objective, how ...
A Smart Data Approach to Assurance in a Hybrid Cloud Environment

A Smart Data Approach to Assurance in a Hybrid Cloud Environment

Smart Data Microsoft and Amazon both reported significant growth in their cloud businesses recently. Revenue for Microsoft’s Azure increased by ...
Mitigating Cyberattacks: The Prevention and Handling

Mitigating Cyberattacks: The Prevention and Handling

Mitigating Cyberattacks New tools and technologies help companies in their drive to improve performance, cut costs and grow their businesses ...
Backups And Disaster Recovery Are Not The Same Thing

Backups And Disaster Recovery Are Not The Same Thing

Backups And Disaster Recovery Most business owners are aware of the consequences of losing data. Much of the value of ...
Cloud’s Mighty Role - Why Custom Development is the Next Big Thing (Again)

Cloud’s Mighty Role – Why Custom Development is the Next Big Thing (Again)

Custom Development is the Next Big Thing Today, software is playing a very important role in performing basic business processes ...
Matthew Cleaver

Dispelling the Myths of Cloud Solutions for the Small Business

Dispelling the Myths of Cloud Solutions As a business leader, migrating to the cloud can be overwhelming due to the ...
Ransomware Cyber-Attacks: Best Practices and Preventative Measures

Ransomware Cyber-Attacks: Best Practices and Preventative Measures

Ransomware Cyber-Attacks “WanaCrypt0r 2.0” or “WannaCry,” an unprecedented global ransomware cyber-attack recently hit over 200,000 banking institutions, hospitals, government agencies, ...
HTML5 Speed Test

HTML5 Speed Test

HTML5 SPEED TEST SERVICES There is no made-for-all solution when it comes to optimizing a website for speed, and while putting a cloud platform in place is a good start, every cloud startup should ensure that they have an optimization ...
Glassdoor’s 10 Highest Paying Tech Jobs Of 2018

Glassdoor’s 10 Highest Paying Tech Jobs Of 2018

Glassdoor is best known for its candid, honest reviews of employers written anonymously by employees. It is now common practice and a good idea for anyone considering a position with a new employer to check them out on Glassdoor first. With ...
20 Leading Cloud CMS Wordpress Alternatives

20 Leading Cloud CMS WordPress Alternatives

Cloud CMS Wordpress Alternatives Content management systems (CMS) have grown exponentially in recent years. Their number and features have exploded. There are now dozens of cloud CMS Wordpress alternatives for startups and small business. CMS is getting more sophisticated. Website building ...
10 Prototyping Tools To Help Build Your Startup

10 Prototyping Tools To Help Build Your Startup

Prototyping Tools We are continuing this week by focusing on startup tools, tips and tweaks that will help you build, design, manage and market your way into the cloud based business that you want to be. Last week we offered a ...
The Developer’s Guide to Azure

The Developer’s Guide to Azure

Develop on a cloud platform designed for you. In this update of the Developer’s Guide to Azure, see how the comprehensive set of Azure app platform services fits your needs. Use it to navigate the architectural approaches and most common ...
Infographic - Internet of Things (IoT) Will Be Top Technology Investment

Infographic – Internet of Things (IoT) Will Be Top Technology Investment

Internet of Things Investment Investors are jumping all over the opportunities abound when it comes to the Internet of Things and Big Data. There is simply way too much money at stake to ignore the potential that is going to truly ...