Config2Spec: Mining network specifications from network configurations

Research area: Verification and Synthesis

Published by Rüdiger Birkner on March 8, 2021

Originally written for the APNIC Blog

For several years now, the community has been dreaming of Intent-Based Networking (IBN): the idea of telling the network what to do instead of how to do it.

An operator should, for example, be able to simply state its intent of sending traffic via a waypoint, instead of having to manually configure all the network’s link weights such that the shortest path goes via the waypoint. To this end, both network operators and researchers looked at abstracting away the technical details of configuring a network, allowing them to simply specify the intended behaviour and letting the ‘network’ take care of the rest.

This vision of IBN comes from the fact that still today, configuring traditional distributed networks is extremely difficult and error-prone. Because of the indirect configuration process and the complex dependencies among the different routing protocols and features, configuration errors are not uncommon. A study from Alibaba, for example, revealed that the majority of their incidents (56%) resulted from operators updating configurations.

To assist operators and prevent such incidents, the community has been working on configuration verification and synthesis tools. Verification tools allow checking that the configuration actually behaves as intended before deploying it in the network. While synthesis tools automatically generate network-wide configurations according to the intended behaviour, to be of any use, both types of tools require the operator to specify network behaviour with their intent.

The challenges of obtaining network specifications

But, what is actually such an intent? An operator’s intent, or more formally a specification, is a precise description of the properties a system — in our case, the network — has to satisfy. These properties can take various forms. For example, they can describe the forwarding behaviour, security aspects, or control plane behaviour.

Current verification systems focus on forwarding and security specifications. The properties encompass reachability, isolation, waypointing, and load balancing policies. Alongside these properties, network operators usually have to provide a failure model which those properties must hold. For example, a specification could mandate that all nodes are reachable up to single link failures.

Unfortunately, writing down a network’s full specification by hand is difficult.

It’s easy to write down the basics and summarize the main policies such as load balancing the traffic for that one popular destination, dropping traffic from the few suspicious prefixes, or rerouting critical traffic via predefined waypoints.

However, the complete specification includes a lot more than these few specific policies. It describes the entire network’s behaviour under failure for all devices and destinations. Consequently, these specifications can be huge — the specification of Internet2 consists of several thousand policies — and are the result of years of work by a changing team of network engineers. Hence, manually writing down a network’s complete and correct specification is nearly impossible.

Without simpler ways of obtaining a network’s specification, network verification and synthesis tools are unlikely to be widely deployed. As recent research confirms, needing the network’s specification imposes a major barrier to adoption.

Config2Spec: automatically mining network specifications for the operator

That is exactly where our work, Config2Spec enters the scene: Config2Spec relieves network operators from the difficult and cumbersome task of manually writing down a network’s specification, by automatically mining it from network-wide configurations and the failure model (such as up to k failures).

Doing so is challenging as one has to find all the policies that hold within the entire failure model. Both the space of policies, as well as the space of environments in the failure model—the topologies under all possible failures—are exponential.

Config2Spec addresses this challenge by combining the strengths of two well-known techniques:

Data plane analysis, which enables us to compute the set of properties that hold for a single environment
Control plane verification, which enables us to validate that a single property holds for all environments of the failure model

The former provides an efficient way to prune properties, which it does by removing properties from consideration that are obviously violated. The latter allows us to efficiently verify the remaining properties for the entire failure model.

At a high-level, one can think of Config2Spec’s approach in two stages: First, it obtains a rough guess of the specification by computing and analyzing the data plane of a few environments. This allows it to quickly narrow down the specification guess to the policies that most likely hold. Second, it refines the guess into the true specification by validating the remaining properties one-by-one.

In practice, Config2Spec switches back and forth between these two stages, dynamically identifying the approach that provides better progress. To this end, Config2Spec relies on the feedback from past iterations and the failure model as it adapts its approach to the situation at hand.

Thanks to the combination of the two stages, Config2Spec is sound and complete: sound, as it does not include any policy that is not part of the specification due to control plane verification; and complete, as it does not miss any policy belonging to the specification due to data plane analysis.

Focusing on behaviour, not specifications

Helping network operators get started with new validation and synthesis tools is just one use-case of Config2Spec. Furthermore, the specification can be used to get a general understanding of the network and its behaviour.

Here, it is important to note that the mined specification does not represent the intent of the operator, but the actual behaviour of the network as defined by the configuration. Hence, network operators can also use the mined specification to identify problems within the network by comparing it to their intent, thus checking whether the network is behaving as expected.

In addition, Config2Spec can be used to analyze configuration updates by comparing the specifications before and after the changes, even before deploying them in production.

One piece of the puzzle

Config2Spec is one piece in the large puzzle of IBN. It helps network operators, for example, getting started with verification and synthesis tools by automatically mining their network’s specification from the network-wide configuration. Still, there is a lot of work ahead to make IBN a reality. The specification and policies supported by Config2Spec are currently only concerned with forwarding, which leaves out control plane policies like minimizing routing table size or egress preferences.

We are looking forward to hearing/reading your thoughts and ideas about Config2Spec.