Hi everyone, my name is Rüdiger Birkner and
today I'm going to talk about Config2Spec,
a tool to facilitate intent-based networking or
at least a tool to take some steps towards
it.
For quite some years, intent-based networking or
short IBN has been on everyone's mind.
And the idea of it sounds great.
You specify your intent and the network just
behaves accordingly.
No more cumbersome configurations.
You need intent and you're done.
Unfortunately, we're not there yet.
Actually there's still quite some ground to be
covered, but at least there's progress.
All major vendors have somewhat intent-based
networking product or solution.
And also in academia, a lot of work has gone into
it.
For example, there are network configuration
synthesis tools that allow operators to
automatically
produce network configurations according to their
intent.
And there are many configuration validation and
verification tools that allow to check
whether your configuration satisfies your intent
or not.
Some of these tools made it even and are
commercially available now.
So imagine you have just heard about these tools
and you want to try them out for yourselves.
For example, you're about to deploy some
configuration change and you want to make sure
that the
change really only does what you intended to do
and doesn't break anything.
So you start looking around and you find that
today several network validation and verification
tools are available.
You check them out and you realize that they more
or less all follow the same recipe.
First of all, you get the config, you apply your
changes and you provide it to the tool.
Second, you need to specify your intent.
Third, you need to run the tool, you wait for the
results.
And finally, you check the results and maybe you
need to adapt something in your configurations
or you're good to go.
So it's quite a straightforward process, no?
But hold on, most of these steps are clear.
Get the configurations, run the tool, act upon it.
But what is actually this intent?
What is a specification?
Let's look at that a bit closer.
So in general, a specification simply describes
the behavior of a system.
So as the name says, it specifies how the system
should behave.
Hence in our case, in a network, a specification
simply consists of all the policies that should
hold in your network.
So in this project, we consider policies from a
policy language and we support four predicates,
reachability, isolation, waypointing and load
balancing.
These are the most common policies in the network
validation and verification literature.
So for example, our specification could consist
of the following policies for the given network.
But what does it actually mean these policies
should hold?
The network can be in different states, routers
and links can fail and the network's behavior
will change.
For sure, the policies will all hold when all the
links are up.
But what if router R1 or some link fails?
Or what if all the link fails?
Do the policies still have to hold?
So clearly just having a set of policies is not
enough.
We also need a context, a context under which
these policies have to hold.
So we can just extend our definition of the
specification by not only requiring the set
of policies, but also by requiring that the set
of policies have to hold under a given
failure model.
Now this failure model provides the missing
context.
An operator can specify all the concrete
environments.
So all the states of the network for which the
policies should hold.
So one concrete environment is basically one
state of the network where simply every link
is assigned to be either up or down.
For example, the operator could specify the
following five environments and in a realistic
setting with a larger topology, specifying
manually all these concrete environments is
cumbersome and also not desired.
So therefore you can actually capture such a
failure model in two parts, with a symbolic
environment and the failure bound.
The symbolic environment is basically the network
topology in which every link is assigned
one of three states, up, down or symbolic.
And symbolic simply means that the link can be
either up or down.
And the second part of failure bound simply
provides a bound on the maximum number of
links that can or are expected to be down at the
same time.
So together the set of policies and the failure
model make up the network specification.
And this definition of the specification is
actually widely used in today's network
verification
literature.
So now that we know what the network
specification is, we can come back to the recipe
and we
should be all set to use the network validator to
check our configuration change.
Unfortunately, this is not the case.
While the definition of a specification is
actually quite simple, writing down a complete
specification is actually extremely difficult.
And this is not just in networking the case, but
in general, as this tweet of a well-known
researcher shows.
The need for specification often prevents people
from using verification tools.
This is also what a paper from HotNets 2019 by
Ryan Beckett and Ratul Mahajan noted.
So they basically said that outside of a handful
of large cloud computing providers, the use
of network verification tools is still sparse.
And they even argued that the next frontier for
network verification is to enable easy
and effective use for the average network
engineer.
And actually, we also have our own anecdotal
experience with that.
A while ago, we were discussing with a network
operator that mentioned to us that they were
about to also try to deploy such a network
verification tools.
But in the end, the adoption of this tool fell
through just because the tool required
a specification.
You might still wonder and ask yourself, is it
really that hard to write down how you
want your network to behave?
Well, just take Internet2 as an example.
As part of this project, we analyzed the publicly
available configuration from 2015 and found
that its specification is made up of almost 4,000
policy predicates.
Now imagine writing this specification by hand
and doing this without mistake.
Or if you are a network operator, would you know
all the policies of your network?
Or could you fully describe its behavior?
I would really be curious to discuss this with
you and hear what you have to say.
But in any case, don't worry.
This is exactly where Config2Spec enters the
scenes and is here to assist network operators.
So together with Dana from Technion, Martin and
Laurent from ETH Zurich, we developed
Config2Spec, a tool that automatically mines a
network specification.
So Config2Spec takes as input your network's
configuration and the failure model.
And it automatically finds your network
specification, so all the policies that your
network enforces.
In the following, we will first consider two
strong approaches that individually explore
one dimension of the problem at a time.
Then I show you how we combine these two
approaches to leverage their individual strengths.
And in the end, we'll talk about Config2Spec's
performance.
So how long it actually takes to compute such a
specification.
So let's get started with the straw man solutions.
When you think back to the specification, you
remember that we only want to have those
policies from the space of all policies that hold
for every single concrete environment
in the failure model.
So we kind of have two dimensions, or we have
kind of two search spaces.
One is the failure model, so all the concrete
environments that it contains.
And the other one are all the policies.
So it's a space of all possible policy.
Together in combination, this becomes untractable.
However, we can look at the two in isolation.
When we look at it from the perspective of the
failure model, so when we look at all
the concrete environments, we can make use of
data plane analysis.
And when we look at it from the perspective of
the policies, we can make use of control
plane verification.
So what do I mean by that?
Let's first look at data plane analysis.
At the high level, we can break down the problem
of finding the specification for a failure
model and the configuration into finding the
specification for each concrete environment
within the failure model.
And then we just combine the outputs.
So we start with one concrete environment from
the failure model, and together with
the network configuration, we compute the forwarding
state using data plane analysis.
From the forwarding state, we can easily
determine whether two nodes are reachable,
isolated,
and so on.
So below here, I show you kind of an abstract
illustration of this.
The blue area represents the space of all
possible policies.
After running data plane analysis and finding all
the policies for this one concrete environment,
we can narrow it down, and we have kind of the
set of policies that hold only for this
one environment.
So now we continue one environment after the
other.
And finally, at the end, we have the
specification for each concrete environment in
isolation.
And since the specification of the full failure
model is a set of policies that holds for
all of them, we can simply take the intersection,
and we will end up with the network specification.
So as you can see, by intersecting one by one, we
start with a very rough over-approximation
of the specification and refine it step by step.
And finally, we end up with the network
specification.
So when we now look at the problem from the
perspective of the policies, and we use control
plane verification, we have again the same
situation.
We have a large number of candidate policies.
We have the failure model and the configuration.
And with modern verification tools, we can easily
check if a single policy holds for
the entire failure model or not.
So from that space of all policies, we can select
one policy, feed it together with the
config and the failure model to the verifier, and
the verifier will tell us whether this
one policy holds for the failure model or not.
Now we can do this for every single possible
policy separately, verifying them one by one,
and ultimately obtain the full specification by
taking the union of this.
So here, we kind of under-approximate the
specification and increase it step by step
until we reach the full specification.
So to quickly recap, both techniques have their
pros and cons.
Data plane analysis can find all the policies
that hold for a single concrete environment,
whereas control plane verification can check
whether one policy holds for the entire failure
model.
So the strength of data plane analysis is
actually to quickly cut down the candidate
space, as with checking one single concrete
environment, one can already rule out a lot
of policies.
And control plane verification is very good at
verifying a small set of candidate policies
and quickly identifying which belong to the
specifications and which don't.
So the natural question, or actually I already
led to this, is why don't you combine the
two approaches?
And this is exactly what we do.
So internally, config2spec consists of multiple
modules.
First of all, of a data plane analysis module and
the control plane verification module,
and it consists of a predictor.
And this predictor dynamically decides whether to
use one or the other, always favoring faster
completion.
So let's look at this at the high level.
In the beginning, we start with the set of all
possible policies as our candidate set
for the specification.
And this I try to illustrate with the blue area
behind me.
We start with data plane analysis, pick one
concrete environment, see what policies hold
for this environment, and intersect that with the
candidate set.
We continue, pick another concrete environment,
and so on.
We quickly manage to reduce the candidate set by
a lot.
However, we continue with this until kind of not
much more progress can be made.
The size of the candidate set stabilizes.
And at this point, the predictor decides to
switch from data plane analysis to control
plane verification and starts to pick one policy
after the other and verify them.
It will check whether these policies hold for the
failure model.
Some won't, some will.
And the continuous one policy after another until
we have checked them all and config
to spec terminates and we have found the full
specification.
So to make config to spec really work, we
optimized both approaches.
Following, I will just present the intuition.
First of all, we can speed up data plane analysis
or kind of the process of narrowing down the
candidate set a lot by choosing the right
environments to analyze.
We do that based on the remaining candidate set.
So we always pick the next environment that maximally
disrupts the forwarding state with
respect to those policies.
To speed up the verification, we can kind of do
three things.
First of all, we can group policies.
So instead of checking them one by one, we check
them in small groups.
Second, we can consider dependencies.
For example, if we check a reachability between
two points and we see that it doesn't hold,
we don't need to check a waypointing policy
between those points because we know if the
reachability doesn't hold, the waypointing can't
hold either.
And as a last part, we can trim policies without
even verifying them.
So we can trim policies which cannot hold because
of topological constraints.
Just think of a failure model that allows for
tooling failures.
We have a topology that has two different paths
between a given set of nodes.
And we know that there can't be a reachability
between those nodes under tooling failures
if there are only two paths.
So there's no point in verifying this policy.
We know beforehand that it doesn't hold.
So now, finally, let's look at how config2spec
performs.
To this end, we have fully implemented config2spec
in about 5,000 lines of Python and Java code
and we rely on two state-of-the-art tools, Batfish
for data plane analysis and Minesweeper
for control plane verification.
To test config2spec, we have generated
configurations using a tool called netcomplete.
And we did this for three networks, a small, a
medium, and a large one.
Let's look at the runtime of config2spec.
Let's look at how long it takes to actually find
such a specification.
Now, in the following, I will only show you the
results for the largest topology, which
has roughly 160 routers.
For all the other topologies, the results were
similar.
Obviously, it was faster, but they were
qualitatively similar.
On the y-axis, we show the runtime in hours.
We make a difference between the BGP and the OSPF
configurations because OSPF configs are
much easier to deal with and hence faster.
In addition, we split up the time that config2spec
used into the time it used for data plane
analysis and the time it used for control plane
verification.
We ran the analysis for three different failure
models for up to one, two, and three link
failures.
Now, there are two special cases to consider.
The first special case are failure models
consisting of few environments.
Interestingly, we never use verification in cases
where we only allow up to one link
failure.
And this is due to the fact that there are only
very few concrete environments, but a
lot of candidate policies.
So the predictor decides that it is faster to
just iterate through all of the environments
instead of trying to verify the policies.
On the other hand, the other special case are
situations where we allow for a lot of
link failures.
Because then the trimming is extremely efficient
and there are actually not that many candidate
policies left that we have to check.
So it's faster to actually just go through the
policies and check them one by one instead
of going through all the environments.
The worst case is somehow in between where we
have a lot of concrete environments to
consider and we also cannot discard many policies
because of topological constraints.
In that case, it took almost 14 hours for config
to spec to find the specification.
And as you can see, most of the time is spent verifying
the policies.
Obviously, if you have a larger topology, it will
take longer.
However, note that you don't run config to spec
whenever you perform a configuration
change.
You run config to spec once or twice to learn the
specification and then you can use that
specification for verification, synthesis and so
on.
With that, we're already at the end of this talk.
So I presented to you config to spec, a system
that takes on the challenging task of
automatically
mining a specification from the configuration and
the failure model.
And after all this, you might think, great, we
have the network specification and now
what?
First of all, the learn specification is useful
for verification as explained in the
beginning.
However, it's also useful beyond verification.
For example, one can use it for what if and analyzes.
So you can compute the specifications for
different configurations and check what happens
if you do this or that.
Second, you can use it also for config streamlining,
which means you learn the specification for
an existing configuration and then you want to
synthesize a new configuration that has
the same behavior, so the same spec, but uses a
different mix of routing protocols or protocol
features.
And finally, config to spec can help you just
better understand your network's behavior.
So if I raised your interest, I really invite you
to check out our NSDI 20 paper as there
are more details to config to spec than what I
covered today.
In addition, we're still working on config to
spec, trying to improve it.
So if you have any opinion on it, if you think
this is useful, please let us know.
So please reach out to us either to my email
address or visit our website.
Thanks a lot for your attention and I'm happy to
take any questions.