Startup Veriflow, which emerged from stealth this April, has an ambitious goal: to eliminate the human configuration and change errors that lead to outages and breaches.
It claims to accomplish this goal by verifying changes against a near-real-time network state model that can validate network flow behavior to ensure changes and updates won’t cause problems.
The Big Idea
The startup applies the concept of formal verification, which uses algorithms to assert the correctness of system based on operator-defined specifications, to the networking domain.
“Industries like aerospace use formal verification—it’s how they model a new aircraft,” says Brighten Godfrey, Veriflow co-founder and CTO in an interview. “They mathematically eliminate error so that when they go to fabrication, there’s no errors.”
He and his co-founders decided to take that methodology and develop algorithms that apply to network infrastructure. “We mathematically validate all possible network flow behavior before it happens,” he says.
Veriflow’s product has three components: a Data Plane Collector, a Verification Engine, and a Policy Explorer UI.
The Data Plane Collector can be installed directly on network devices or it can access devices remotely. The collector pulls out the CAM tables and ACL tables from routers, switches, firewalls, and load balancers (including physical and virtual versions) that define the behavior of the network at in the data plane.
The Collector can use a device’s API if available, or will log in to the device via SSH to read device state.
Collected data is then loaded into the Verification Engine, which runs as a virtual appliance on the customer premises or in the cloud. The engine synthesizes the data into a network model, which can be used to predict the behavior of packets and flows moving through the network.
The third component is the Policy Explorer UI, which provides a real-time view of security and network policies as instantiated in the network, and can alert on policy violations.
“We have the reality of the network, and we can show that to the network or security operator,” said Godfrey. For example, the UI could show how an attacker might be able to move laterally through the network.
The P-Word (Policy)
The product serves as a near-real-time repository of network policy—not stated policy, but actually how packets and flows move through the network. That’s a powerful distinction, because what’s written in the policy binder isn’t necessarily the same as what’s configured on the network.
The product can be used to model configuration changes before the change is made to see if the change will violate a policy, or cause an unwanted outcome such as an outage. Godfrey says the startup is working with a customer that has a software-defined infrastructure. Before a controller reconfigures a switch, the change is modeled in software first.
“You hit our API, model the change, and it verifies network-wide whether a policy is violated,” says Godfrey. “Only after it’s verified do the switches get touched.”
Veriflow also positions its product as way to reduce the complexity of firewall rules and ACLs. With these rules often numbering in the thouands, it’s hard for operators to make changes because they can’t grasp the potential implications.
Godfrey says operators can query the system to understand the consequences of adding a rule, or removing rules. For instance, if an organization is trying to prune firewall rules, it could query the system and ask “What is the maximum set of rules I can remove that still meets all specified network policies?”
I had several questions for Veriflow during the briefing. Here’s a selection, with responses from CTO Godfrey.
How long does it take to run a formal verification?
It depends on the scale of the network, but the goal is minutes to seconds when it’s used in human automation. If we’re in an SDN controller, then we’re at milliseconds. The way it happens is that we do incremental verification. The algorithm can figure out what needs to be re-verified incrementally between changes.
How often is state data updated?
It’s configurable. Typical use is a periodic data pull, on an hour time scale. The bottleneck is in the APIs to get data off the device; some older devices don’t have good APIs and they become the bottleneck.
Is there an impact on the network device when you poll it for data?
No. It’s about a megabyte of data for a complete snapshot. Switches and routers have separated the management from the data traffic so it doesn’t affect the flow of data. We aren’t tapping in and reading every data packet.
What about drift between what you’ve got in your model and the actual state of the network?
At any moment, something can happen on a device, and we will take notifications to take data off, like via SNMP, when there’s a change, so we can trigger data collection. But you still want to do some periodic, full-data collection for maximum confidence.
How do customers handle remediation overload when trying to address policy violations?
Having a network-wide understanding helps with prioritization. We can see a vulnerability, [such as] is it allowing access or movement from the public Internet? So you can look at these metrics and others to figure out the top priorities. You could combine it with an awareness of assets in the network, what assets are most critical.
How do you express policies in your system?
In our library there are configuration policies that can be broadly applied. And our API allows expression of a kind of data flow behavior programatically, and you can query us like a database to say “Can this happen?” “Yes, this can happen, and here’s how”
It’s a REST API so every language can work with it. We use Python most often with customers.
Does the product do any kind of network discovery?
Users can specify which devices to monitor. Automated network discovery is an option as well.
Veriflow offering subscription pricing based on the number of devices. There are no fees or other prices based on users or queries.
Veriflow was founded in 2013. It has raised $2.9 million from New Enterprise Associates (NEA), the National Science Foundation, and the Department of Defense.
The company’s co-founders are CTO Brighten Godfrey; CSO Matthew Caesar and Principal Engineer Ahmed Khurshid. All three hold Ph.Ds. in Computer Science: Godfrey and Caesar from U.C. Berkeley, and Khurshid from the University of Illinois at Urbana-Champaign.
CEO and President James Brear has long experience in the networking industry, including roles at Cisco Systems, Force10 Networks and Tasman Networks. Before joining Veriflow, he was CEO of Procera, which was acquired in 2015.
Scott Shenker, Professor in the Electrical Engineering and Computer Sciences Department at UC Berkeley, and a co-founder of Nicira—which was acquired by VMware—is an advisor to Veriflow.
More Startup Coverage