Mathematical algorithms might be able to predict exactly how your network will act.


Is it possible to prove, beyond all shadow of a doubt, that your network is secure?

SecTor has talked about how security alerts are becoming more probabilistic. This week, we’re looking at an effort to do the opposite, by turning probabilistic estimates of security into deterministic, proven certainties.

This is a controversial concept. We have long accepted that there’s no such thing as 100% security in IT. Instead, it’s about risk, which is naturally fluid and difficult to estimate. It has traditionally involved doing the best job you can and expending your security efforts where they’re needed the most.

A secure network – proven mathematically

Brighten Godfrey, the CTO of Veriflow, wants to make it more binary. The US-based startup wants to predict your network’s behaviour with mathematical certainty. It is basing its product on a technique known as formal verification, which is sometimes used by software engineers to prove that software will operate correctly without any bugs.

“This is a field of computer science that develops technology to mathematically check whether a design is correct before putting it in the field,” he explained.

NASA uses formal verification to ensure that software is working properly on spacecraft, because if a program goes wrong up there, no one will be driving out with a floppy disk to fix it. Mission-critical systems from aircraft to nuclear power stations use it, too.

Practical applications for the technique have come a long way since it began, according to Jonathan Katz, director of the Maryland Cybersecurity Center and professor in the department of computer science at the University of Maryland.

“It’s hard to verify large pieces of software, and so the extent to which they were verified were very limited,” he said, adding that verification techniques have evolved over the past few years. “Now we have examples of verifiable operating systems, web browsers, and cryptographic algorithms themselves.”

Newtonian networks

This concept mimics a Newtonian view of the universe, which suggests that absolute knowledge of all forces in a system will enable you to predict its events with complete accuracy.

The problem with Newtonian mechanics is that they’re theoretical, not practical. You can’t quantify and document every force on every object in the universe. But Godfrey maintains that you can completely understand a computer network’s traffic flow if you watch it closely enough, even when that network is vast and complex.

“There’s a spectrum of complexity. There’s some software that’s small enough that a human can manually understand what that is. At the other end is arbitrary software that even for mathematic formal verification is far too complex,” he said. “Networks are in a sweet spot in the middle. This is beyond a challenge for humans to handle but we have made it feasible for automated verification to do it.”

His virtual network appliance is designed to prove that the network will operate in a way that managers’ policies dictate, and Veriflow also provides a library of its own policies that a network can be assessed against. It discovers and analyzes all of the devices on it that operate through layers one through four of the OSI networking stack (that’s everything up to switches and routers). Then, its algorithms analyse the traffic and the behaviour of devices on the network.

The idea is to have a complete understanding of the entire, network-wide behaviour on the network, he said, to the point where the software can predict what any packet from any given network device will do, at any point.
There are probably more combinations of packets and routes on your network than there are atoms in the universe, he said, so that’s a big ask. But he believes the firms’ algorithms will do it, gathering the information into a network-wide predictive data flow model.

A deep gaze, but not a broad one

Does this mean that your company’s cyber security can be mathematically proven? Sadly, it isn’t that easy. Cyber security has its own stack, ranging from the network all the way through to the people that use it, with everything in between. That includes the computers connected to the network and the applications they run.

Katz is the first to point out that you can’t verify all of that stuff. “The challenge is that you really do want to analyze the entire system,” he said. “Being able to prove security in one component of a system means that you’ve locked down that component, but then the attacker of course will just look at the other components and see where they can break in.”

That weak link may be a Windows box, which is far too complex to formally verify, or a receptionist who was a little too lax with her account details. That, too, goes beyond the realms of rational verification. Veriflow makes no claim to predict how they may operate.

Nevertheless, the firm does claim to prove that the traffic flow in a large, complex network is configured and segregated according to policies created by management, he claimed. That’s important, because a segmentation loophole may go unnoticed by your engineers, but could be spotted by an attacker who could use it to jump from one area of the network to another.

“Exactly that case of network segmentation comes up in the majority of customers, so this is a key use case,” he continued.

Other use cases include supporting customers during live incidents, where an ongoing compromise has been spotted. “As the machine gets compromised, you need that segmentation in place,” he said, arguing that companies may do that manually today, logging into individual boxes and poking around on devices to determine their status.

“That might take four hours,” he warned, arguing that his tool would prove what was segmented with 100% certainty. “What we provide is faster incident response.”

So no, it isn’t possible to verify an entire organization’s cybersecurity with math. Most of it will still be down to good old fashioned risk analysis and best practices. But if Godfrey’s claims are accurate, it does seem that we can drive determinism and complete predictability into at least one part of it. Every little helps, right?

Are you interested in finding out more about network security? Check out the registration page for the SecTor security conference in downtown Toronto, October 17-19th 2016. 


Bookmark and Share