Player is loading...

Embed

Embed code

Transcriptions

Note: this content has been automatically generated.
00:00:00
um hoops before i start i uh would like to say that the
00:00:06
later or the end of the talk i will uh right
00:00:09
sure do some work that was done jointly with um a p. h. d. students essays are strong you can select the
00:00:14
idea a post doc the researcher trees but those uh and professor george kind they're all from e. p. f.
00:00:21
so this is a um traditional view i'm gonna show you of the network
00:00:27
um as we most of us learned a about it at school
00:00:32
so there is a set of and hose at the edge and then there is the network in the middle
00:00:39
and only interesting processing happens at the end of course
00:00:43
not at the network of course there are
00:00:47
um network devices right there switches and routers inside the network
00:00:51
uh doing some processing but the processing their dwayne is mostly
00:00:56
standardised and well understood so each network device would have eight data play
00:01:02
that the um whose role is to receive the packets uh look at their ethernet or i. p.
00:01:07
headers to decide where to send the packet next and then there would be a control plane
00:01:13
'cause role would be to uh run routing protocols like b. g. p. and always the f.
00:01:18
and populate the all the data structures the forwarding people's views by the data point
00:01:23
but the point is that there is this very very clear separation
00:01:27
between the and host at the edge and the network
00:01:32
uh and all the interesting processing again happens at the end holes and the network does nothing more than forwarding
00:01:38
in routing now the problem with these uh picture is that eight turned out not to be enough
00:01:45
so it turned out that a network has to do much more than forwarding in routing
00:01:50
um for instance it has to implement security functions
00:01:53
like fire walls the intrusion detection systems
00:01:56
uh traffic scrubbers it has to implement um performance optimisation functions like transparent caches
00:02:03
um load balancer is web accelerators it has to
00:02:06
implement a translation functions like network address
00:02:10
translation um or chance coders from various uh between value scheme manager video formats
00:02:16
um and also a lot of monitoring functions like for accounting or compliance monitoring
00:02:23
so tool uh satisfy all these needs a back in
00:02:27
the nineties the the research the networking research community
00:02:31
came up with a very beautiful vision of an active network so in that vision
00:02:37
of the world consists of inter connected we've network so we don't have
00:02:43
a head versus network and the idea is that these active networking owns can be
00:02:49
programmed to do not only forwarding and routing but anything we want to
00:02:54
and in fact they can execute call that is carried inside packets
00:02:59
so the idea was that a and and host would
00:03:02
start some computation story partial results inside the packet
00:03:06
send the packet out in the network where any network device could pick
00:03:10
it up and start executing you know complete the computation and soul
00:03:15
so this way we could program not only individual and host to complete individual tasks
00:03:21
but we could program the entire network as a whole to complete the task
00:03:27
so that was a very beautiful vision um
00:03:31
but it was controversial so the the research community was very very excited about it
00:03:37
but the network practitioners thought that it was scary and they thought that it provided way
00:03:42
more flexibility and programmability than what was really necessary so networks didn't really happen
00:03:50
um instead we got something completely different we got middle boxes
00:03:57
so little boxes are a little bit like active network nodes in that they are
00:04:02
sophisticated network devices located in the middle of the network that to processing um
00:04:09
but unlike um active networking owns they're not fully programmable so a um
00:04:16
traditional middle box these eight closed appliance that implements fixed functionality and
00:04:22
is located at the fix network point so if i
00:04:25
network operator wants to deploy new functionality or above a new
00:04:30
network location they need to deploy a new middle box
00:04:34
now the problem with little boxes is that they are m. s. so first of all there are tons of them
00:04:40
so a recent study show that about a third or more of network devices to date our mailboxes surprise me
00:04:47
um and it's they are really a pain to manage because of their
00:04:51
lack of programmability um so let me illustrate with an example
00:04:57
a very serious uh security fred a four networks today is the now of service
00:05:02
so in in our service at dark and a darker sense um large volume of unwanted
00:05:08
traffic and flights the network and disrupts the connectivity between the legitimate and host
00:05:13
so the way a network providers deal we've um canal service uh
00:05:18
attacks today is the use scrubbing little boxes so basic rubber
00:05:23
takes as input to the the um a flawed traffic any process it and
00:05:28
it separates the good packets from the backpack it's that's what it that's
00:05:32
now and network today typically it's offers many small denial
00:05:37
of service attacks even on a daily basis
00:05:40
and um let's say a massive denial of service attack every
00:05:44
few years or so depending on the kind of network
00:05:48
now the massive attack maybe rare but when it does happen of course it
00:05:51
has a significant cost not only because it takes time to deal with
00:05:56
but because it impacts the reputation of the network provider that's offers of everybody learns that network such and
00:06:01
such once was down for so many also for so many days and that can be very bad
00:06:06
so the first problem that network operators face is that they um that the the
00:06:13
nature of the of the denial of service traffic changes all the time
00:06:16
so they need to keep buying and learning how to use and testing and deploying new little boxes inside their networks
00:06:23
the other problem is that um well you don't know what kind of attack provision for
00:06:29
should you buy a big scrapping middle box to provision for the a rare
00:06:34
massive attack of multiple but you get bits per second that you may receive or
00:06:38
provision for you know the smaller the attacks a few megabits per second
00:06:43
and even when you make you to make that decision um it is not
00:06:47
easy to decide how to spend your security budget so should you
00:06:51
for instance by lots of smaller scrubbers and position one at each entrance into
00:06:57
your network in order to block the uh traffic as early as possible
00:07:02
or should you spend all your budget by a bigger
00:07:05
a scrubber place it somewhere central inside your network
00:07:10
these latter option is of course more flexible but at
00:07:14
the same time eight creates problems because it allows
00:07:17
the flight traffic the attack traffic to enter the network right he has to go to be
00:07:22
redirected to the central scrubber and then back to its
00:07:24
original destinations so this may introduce congestion into
00:07:28
the network and it may add latency to what the the users of the network experience
00:07:34
no latency is you know one of the key words of the they
00:07:37
kate everybody talks about latency for good or bad reasons um so
00:07:42
by the way this is not just a technical problem is very bad p. r. for network provider
00:07:48
so how to deal with all these shortcomings of middle boxes that have to do with their lack of programmability
00:07:55
a new vision for networks these emerging these days network function
00:08:00
virtually station or an f. b. so here the
00:08:04
idea is that instead of of switches and routers and
00:08:08
all different kinds of middle boxes inside the network
00:08:11
we have simply programmable network platforms sort of the network
00:08:15
operator on each of these platforms can drop
00:08:19
different network functions depending on what is necessary at that point for the network
00:08:25
for example if the network is under denial of service attack
00:08:29
uh the operator can deploy describing network function exactly at the
00:08:34
point where the attack traffic is entering the network
00:08:37
now if the attack changes so the attack traffic moves they start entering at another point
00:08:43
then very easily the operator can also move describing network function okay that's the idea
00:08:51
so this is what and if the net or function virtual decisions about um so in a way
00:08:58
um we're trying not to redirect traffic as we traditionally do traditionally
00:09:03
would we want to process certain kind of traffic in
00:09:05
a certain way we try to we directed to make it go to middle box where it can be processed
00:09:11
instead with benefit we're moving at the network functionality because we have all these network functions that are
00:09:16
floating around so we moved them to where the traffic that we need to treat he's
00:09:21
and it's called and if he virtually station sort of the net or functions are virtual
00:09:26
in the sense that they each of them is not tied to particular device begin float around the network
00:09:33
yeah
00:09:35
now many of you are thinking well but i was told that the new vision for networks is as the enter
00:09:40
softer define networking not interface so how this is the end relate to the story i am uh tell you
00:09:47
so i said earlier that in the traditional network the network devices or switches and
00:09:53
routers and they have the data plane which forwards packets and the control plane
00:09:59
which runs routing protocols in our place the data structures used by the data point
00:10:05
so that's a traditional network in the new kind of network that i'm talking about
00:10:11
we don't have all these things we have these programmable network platforms so the data
00:10:16
played of course runs whatever network function that we have dropped into it
00:10:21
but what about the control plane what is the control plane do this is what is the and tries to pass or
00:10:28
so one possible answer provided maybe as the envision is that
00:10:33
the control planes will move away from the network devices and
00:10:37
it will all be moved into this logically centralise controller
00:10:41
that would make the decisions for the entire network it will monitor the
00:10:44
state of all the the network links it will decide how routing
00:10:48
will happen throughout the network it will deploy virtual network functions as
00:10:52
needed inside the network it will configure the data structures everything
00:10:57
so what exactly how exactly the the this controller looks like it's
00:11:02
still up for debate by the research community and the practitioners
00:11:05
um but one way to think about it for those of you who
00:11:08
are into the cloud he's like a open stack neutron on steroids
00:11:14
so this is how the n. f. b. and as they envision come together
00:11:18
so and if the uh envisions programmable bigger planes were we can drop virtual
00:11:22
network functions and as the n. envisions a programmable logically centralise control plane
00:11:29
which among other things deplores network functions inside the network as needed
00:11:35
is this controversial less so than active networks work in fact
00:11:40
it is very much anticipated um by the practitioners
00:11:44
in fact the the researchers are still very excited about that or programmability and the practitioners still
00:11:50
find it scary but this time around the fee and they agree that it is necessary
00:11:56
so what is it that makes an s. v. a scary the
00:12:01
same thing that made connected networks carry two decades ago
00:12:06
it enables us to the the continues dating of network
00:12:10
functionality and continues updates necessary calm we've box
00:12:15
so imagine a network operator uh she has her network she has
00:12:19
dropped you know network functions into her programmable network platform
00:12:24
you know she drops a new network function bought this one has
00:12:28
about which means that if it receives um a specially crafted
00:12:33
back at a it crashes or you can sort flights the network
00:12:37
or he does other bad things that disrupt network connectivity
00:12:41
now crashing or hanging i mean we may be used lead as computer users right we're used
00:12:46
to our programs a crashing hanging and network operator though is a very different story
00:12:53
network operators or a notoriously conservative and for very good reasons and
00:12:59
network but can disrupt the operation of the network in effect
00:13:03
older users and that can be millions of users at the same time right which is a catastrophe for network operators
00:13:10
so they try to avoid this option is as much as possible um thing called like streets like they
00:13:16
provision backup network links they have hot standby routers
00:13:20
and switches the inside each router they have
00:13:24
hot standby supervisor engines the useful solvable line cards
00:13:29
they um most importantly evade very very rarely change the
00:13:34
functionality of the network they only do it when
00:13:36
they absolutely really really have to um and again as i said that's for very good reason
00:13:43
a few years the ago uh i i was giving a talk about better programmability um
00:13:49
to an audience of a router engineers and um none of them had any
00:13:54
objection to the technology was describing but at some point one of them
00:13:58
raise their hand and said well if this all sounds good but
00:14:02
if you open up the network like that and you make it programmable there
00:14:06
would be all these buttons and who's gonna deal with customer support
00:14:10
so the word of the the router engineers were really afraid that if they try to sell you know
00:14:15
programmable routers and programmable network devices to network operators those
00:14:19
would be very unhappy because who deal with
00:14:22
a customer support both at the network level and from the point of view of the rubber manufacturer
00:14:27
so how do we go from basic justifiably conservative culture of network operators
00:14:33
well world were virtual network functions are just floating around the network
00:14:38
what has changed since the time of active networks that makes such a move possible
00:14:46
so what has changed is that now we can call roost and
00:14:49
so there has been a lot of good progress uh
00:14:53
within the last a decade with a program analysis tools and
00:14:57
after all and network function is just a specialised program
00:15:02
so what we would like to have is a program analysis to
00:15:07
um that takes as input the code of a network function and it property that we would like to prove
00:15:14
for our network function and eats proves that these network
00:15:18
function satisfies or does not satisfy this product
00:15:22
i want all this problem arises to look like exactly depends on what our
00:15:28
network function looks like um and there are two possibilities to the
00:15:34
it could be that the network functions running on a specialist network processor in which case
00:15:39
of course it is written in that domain specific language that that process or understands
00:15:44
or it is the case that our network function rounds on in general propose the
00:15:49
c. p. u. like intel and then our network function as we can in
00:15:52
a general purpose language like c. or c. plus plus and it's typically using
00:15:57
a fast i all library like the p. d. k. or that yeah
00:16:01
so both of these options are interesting enter valley that are happening today um
00:16:08
building a a domain specific language is an art any sin double research core goal
00:16:15
but also i'm learning a studying how to write and how to underlies network functions that are returning to
00:16:22
treat complete language that people are using for all sorts of other things other than that or functions
00:16:28
is also a noble research goal and one that i personally i'm more interested in so this is what i'm i'm working on
00:16:39
network functions are a little bit special in the sense that they're always
00:16:43
read and then supper optimised for high performance hack unpredictable performance
00:16:48
you don't want one packet to take a ten times more than
00:16:52
another packet to be processed because that leads the network problems
00:16:56
so as a result of these optimisation for predictability in performance they have certain characteristics
00:17:03
um first of all relatively conceptually simple processing what does a
00:17:07
network function do well it takes as input a packet
00:17:11
um it read a couple of values from its headers and it may it would typically
00:17:17
look up these values in the data structure like a hash table or hash map
00:17:21
if anything they update some header values it may update a little bit of local state and send the packet on its way
00:17:29
so there are no or for instance no loops of undetermined duration
00:17:33
if there is any looping it is typically over packet uh headers in the worst case
00:17:37
over packet contents before doing something like encryption or uh taking a a texan
00:17:43
there is no dynamic memory allocation you know properly with the
00:17:47
network function um we typically reallocate all the memory
00:17:51
all the packet buffers that we need again to avoid
00:17:54
be unpredictable performance associated with dynamic memory management
00:17:58
and of course there's no recursion so all these characteristic uh
00:18:03
make it conceptually simpler to reason about the the
00:18:06
behaviour of the network function soul in principle network functions
00:18:10
should be good application domain for program nice it's
00:18:16
now what we write a program analysis to would develop
00:18:19
a program analysis tool there are three key aspects
00:18:24
one is the reader of the provided analysis um
00:18:28
can i use this tool to simply test my program
00:18:32
my network function with many different into packets
00:18:36
um or can i use the tool to prove that my network function will never
00:18:40
ever crash or and or an infinite loop no matter what input packet receipts
00:18:45
the other uh aspect is the nature of the properties that i'm
00:18:49
trying to prove um and my interested in low level
00:18:53
properties like crashed freedom or memory safety which are general and
00:18:57
apply to any network function no matter what it does
00:19:00
or i might also interested in higher level semantic a behavioural properties
00:19:05
that are very specific to the particular network function for example if my network function is
00:19:11
a firewall does it drop all the bad packet and does it keep overboard packets
00:19:16
and the last uh aspect is the level of human effort as rules that was saying i might pressing a
00:19:22
button and then wait for the analysis to complete or do i need to interact with the two
00:19:28
now i fully agree that interacting with the two can be you know a great experience and teaches you about your
00:19:33
program but at the same time there are scenarios as i will argue reducing this effort it does make sense
00:19:40
the only their trade offs between these three aspects for example the more readers the analysis we want and the
00:19:46
higher level the properties who want to prove the more human effort is required in order to do it
00:19:52
i'm interested in proofs nodding tests and both for a low level and
00:19:58
semantic properties and the question i'm trying to answer is um
00:20:02
what amount of human effort does it take to what extent can we would use the human effort that is necessary for these tests
00:20:11
so i will make a parenthesis here there is a lot of interesting work going on today that
00:20:16
people call network verification and i would like to relate that to the story and telling
00:20:22
and that would be very fire takes as input a a network topology
00:20:26
and configuration and a set of models for the network functions the
00:20:31
network devices so a model says how is sweet how router how
00:20:35
every single middle box that's in the network should be operating
00:20:39
and also i desired property and then it proves that
00:20:43
these network topology configuration satisfies or not this property
00:20:50
bought a network they fire relies on models of network
00:20:54
functions of network devices for its books so any
00:20:57
proof it produces easing complete unless we also prove that
00:21:02
the only involve network functions behave as intended
00:21:06
so this is one reason why i mean just improves and not tests of the behaviour
00:21:12
of network functions because it is a key piece missing from completing network verification
00:21:19
alright so these days when a non expert a program analysis try
00:21:24
their hand uh at a nice is the first call they
00:21:27
try the first thing they try is symbolic execution um which is in a way the brute force of program analysis
00:21:35
so a symbolic execution engine takes as input code
00:21:39
program code in our case the court of a network function and it has the
00:21:43
possibility that every single branching point to explore all possible outcomes so in principle
00:21:50
and symbolic execution engine can explore and get it can't analyse all
00:21:54
the possible instruction sequences that the network function may execute
00:22:00
does this doesn't require a lot of effort to choose to use a a such a simple integration angie
00:22:05
no not really you can actually press a button and wait for the analysis to complete
00:22:11
what kind of properties can we check definitely low level properties
00:22:15
like rice freedom uh absence of infinite loops but also
00:22:19
high level properties anything we can um anything we can uh
00:22:23
specify as a set of assertions on program state
00:22:28
what about a bigger so can we use symbolic execution only to test or also to prove properties
00:22:35
well i in principle we can prove with symbolic execution
00:22:39
so if i do it an exhaustive symbolic execution of my network function so
00:22:44
i explore all the possible instruction sequences and there's no infinite loop
00:22:49
well i have argued be proved that my network function ease a free of loops
00:22:54
however in product this um there is a very well known problem which is called f. explosion
00:23:00
so real problems and real network functions typically have
00:23:04
such a large number of possible uh uh instruction
00:23:08
sequences that maybe a executed that one cannot
00:23:13
explore all of them and reason about all of them in useful time so what
00:23:18
um people usually do to bypass the problem of symbolic execution is modelling
00:23:25
so when are symbolically executing a program or a network function
00:23:30
instead of executing the implementation of a certain function
00:23:34
one can replace that with a model unconnected a
00:23:38
simplified model of eight function and uh
00:23:43
this way i mean because this functions of the these these models are chosen to be very simple the entire process can
00:23:49
can finish no this is very helpful when using symbolic execution
00:23:54
especially with programs that maintains sophisticated state and network functions
00:24:00
typically do that for instance the meeting flow tables and so modelling is very useful um you also helps a lot by the way within far
00:24:07
right if you have an operating system libraries drivers uh that are your program is
00:24:11
making use of a you have to use models in or usable execution
00:24:16
um of course vase simplification comes at the cost of regard as you may be guessing so when
00:24:23
we are we placing an actual implementation of a function with a model of course where assuming
00:24:29
that the model captures all the interesting properties of the implementation that are relevant
00:24:33
to what we're trying to prove and this may not be the case
00:24:38
so to recap symbolic execution is a handy to each requires little human effort bought
00:24:44
that cam comes to get the cost of finger so using symbolic execution along
00:24:49
can not typically help to prove prove useful properties of a state full network functions
00:24:56
but of course i mean roost and spend all this time talking to us about interesting uh tools that
00:25:01
we can use for problem and i says so they're way more powerful tools out there uh
00:25:06
proof assistance that can help with anything that a human can prove about
00:25:10
a program i'm in principle and they do automatic groove checking
00:25:14
but of course here the cost is human effort like no matter how um
00:25:20
well designed the art hubble they are big do require a nontrivial amount of effort and expertise in order to use
00:25:27
so the question is of course can we have the best of both worlds can we somehow have their readers analyses
00:25:32
offered by the most powerful proof assistance combined with the little human effort uh an
00:25:39
expertise in program analysis required by something as brute force a symbolic execution
00:25:45
okay so now we'll talk a little bit about our uh approach so
00:25:53
a colleague of mine are said uh once that the only a data structure that networking
00:25:59
people need is a hash table and he's mostly right so uh if we
00:26:05
look at the network functions that we use today they all tend to uh be
00:26:09
who's a very few common data structures hash tables hash marks and sarah
00:26:14
i mean by offers a body that this if that is true then why not create a library
00:26:20
with all these common data structures and let's ask program a nice is experts to finalise them
00:26:27
using any tool they they want i if this is gonna take time of course an expertise but if we can
00:26:33
get all the or many network function developers to use this library then this cost will be calmer christ
00:26:40
and then by the network function developer can you use this library
00:26:45
and if i make sure that all the state that might network function maintains it is kept it is down
00:26:50
through this special verified library okay then um then i
00:26:55
can reason about my network function using symbolic execution
00:26:59
symbolic execution as we said does not deal well with state
00:27:03
but my network function does not handle steak directly
00:27:06
it has delegated this task to be special library that has already been finalised with more sophisticated needs
00:27:13
so the idea here is we take the network function and we a separate logically the
00:27:19
called into state focal handled by the library and state was cold so um
00:27:25
we use different techniques to uh underlies the different kinds of course all
00:27:29
state for it takes more time but that is our ties
00:27:32
the state was called it can be done more quickly and it can be done by the developer of the network function themselves
00:27:39
if we manage to pull off this combination then yes we will
00:27:43
have the best of both worlds so how can we do
00:27:47
i
00:27:49
in the first that um we are create our library of of data uh
00:27:54
structures and we're allies in particular for each library function alright formal contract
00:28:01
i'm showing an example here but the details don't matter what matters is that a formal contract
00:28:07
has preconditions impose conditions um like you being a listening to for the past hour ants
00:28:14
eat for my specifies what base library function should do how to behave um
00:28:22
the second in the second step we write the uh the network function and then
00:28:27
we we make sure to use the library to store all the state
00:28:30
uh maintain but is network function and then we underlies it in particular
00:28:36
we use uh first we replace all calls
00:28:40
to library functions with simplified models
00:28:43
and then we'd let's say an exhaustive symbolic execution of the entire network function
00:28:48
right so i'm showing here obviously a simplified example where we have replaced uh calls
00:28:55
to read and write functions these are library to read and write i'm
00:28:59
reading right uh functions to access data stored in the library data structures and
00:29:05
with we replace them with these models now the outcome of this that
00:29:09
he's a set of call traces they are all the possible um course sequences
00:29:15
of calls to library functions that this network function might execute so
00:29:20
in this particular example i'm showing their two possible a sequence uh of
00:29:25
calls or right to some data structure and read plus right
00:29:30
alright
00:29:33
a the last and uh the third and last that we finally prove
00:29:37
that the improve the the the desired property of our network function so we
00:29:44
take first of all we take every single a call trace every single call sequence
00:29:49
and then we check whether our desired property holes at the
00:29:54
end of the school sequence and if it does
00:29:58
then we go back and check whether the outcome of the model
00:30:02
the simplified model that we used for every single library function whether that
00:30:07
is consistent with what the corresponding formal contract for that function specified
00:30:13
i forgot to tell you that we uh in the first that we
00:30:17
prove that each of function implementation actually satisfies the
00:30:22
formal contract that we've written for it
00:30:25
alright so let me show you through a very simple example so let's say we have a network function that came
00:30:31
on other things eight uh it is supposed to drop
00:30:35
any packet receives that has destination port number nine
00:30:39
so the model we're using for the right function here um assumes
00:30:45
that indeed when the input the packet that alright this
00:30:48
input or network function reaches the end of the score sequence the the board can only nine this is the model
00:30:55
now the the contract uh that i'm showing next to to the model
00:31:01
does not say anything about board number nine of course what
00:31:04
it does guarantees that these particular function is not going to modify the back is not gonna do anything to change it
00:31:12
so i'll if i the the developer of the network function if
00:31:15
by this point i have done nothing to ensure that
00:31:18
packets with destination port night are dropped that might prove full
00:31:22
fail because our proof checker is going to say well
00:31:26
um if i look at what the contract says it cannot all for what the model
00:31:30
claims which is that the board will always be different on the destination point but
00:31:35
if i have done the right thing i the developer that is then the provable succeed because again what the
00:31:42
a model claims is supported by the formal contract so this is the the idea
00:31:48
so it was a beautiful idea that a us any harm and uh
00:31:53
one way to describe it is that we are not trying to
00:31:57
come up with the perfect model for every function a priori
00:32:01
because it's a very difficult tasks like my i know in advance which are all the features of a function that would be relevant
00:32:08
for particular proof and make sure that you capture them in the model so instead of trying to do that um we uh
00:32:16
we we write very simple models we write them carelessly if you will
00:32:20
but that's okay because after we use them before proves axes we
00:32:25
come back and we check was this model that we used
00:32:28
alright was it correct for the particular network function and the particular property that we were trying
00:32:33
to prove and that is much easier so this is what we call them lazy groups
00:32:40
so we use this approach um and we developed the a very fight
00:32:45
and network address translation translator that we call a big that
00:32:49
and to the best of our knowledge it's the first i'm not we can see that was formerly very fine
00:32:56
we proved using uh the technique i write outlined that it conforms to r. f. c.
00:33:01
a three zero twenty two which is the r. c. that specifies correct not behaviour
00:33:06
and very importantly we experimented with it and we found that it's performance was on par
00:33:12
so it was not significantly below the performance of a traditional and very fight to compute um
00:33:22
the good news is that it is possible to rigorously reason about
00:33:28
state for network functions with relatively little human effort if you
00:33:33
are a network function developer and you're willing to use a library
00:33:36
of data structures that has already been finalised by next
00:33:41
most importantly these does not have to come at the cost
00:33:44
of performance so when systems people hear about writing cold
00:33:48
in a way that is friendly politeness is there always scared that there will be a a performance cost
00:33:54
in other cases may be the case but with with network functions we have not found that to be the case and that's good news
00:34:02
of course there are challenges and open questions um
00:34:06
the first one is about the universality of data structures used by network functions so
00:34:12
the premise of this work is that we have many many network functions written
00:34:17
by many different developers but if it will all be using a relatively
00:34:21
small set of common data structures and we can put all these in the library right then and allies in our ties the cost um
00:34:29
will that be the case or if this vision takes off and
00:34:32
people develop even more more diverse network functions well when
00:34:37
you start optimising for performance you want to use a slightly different version of that hash map or hash table
00:34:43
and you change a bit interface you change it implementation and now the
00:34:46
very the the analysis effort needs to be done from from scratch
00:34:50
um so will this be the case or will it be the case that
00:34:53
will be able to incrementally reason about slightly different um uh data structures
00:34:58
so that's one one open question and another one is of course going
00:35:02
with further reduce the human effort required to reason about network functions
00:35:07
with lazy proves we certainly would used it a lot relative to uh the existing alternatives but um
00:35:14
very still human effort required in stitching together the results of the various analyses
00:35:19
that we do it so how much more can be reduced that
00:35:24
so if we work on these open questions and we address these open questions
00:35:30
that we are headed we were making progress toward having actually flexible network
00:35:36
now you may question whether that's necessary you may say well he's actually
00:35:40
flexible and programmable network a good idea do we want it um
00:35:45
i think so and we can debate on what particular functionality i or you would like the the the network
00:35:51
to uh to support but i don't think that's the main reason why we should want network flexibility programmability
00:35:58
so when one has these properties um that changes the way they do things and that brings about
00:36:04
a great unexpected things for instance um providers that all for all for software services to date
00:36:12
they're not conservative right they do not whenever they want to what i'm proposing your application or change uh on
00:36:18
or add features to their applications it's not like they do all these you know complicated studies and the
00:36:23
wait for years and they ask everybody do you want this new feature now they tried out the put
00:36:28
it out there like if people pick it up then that's good and everybody works and improve it
00:36:33
and that's great at least a very interesting and dynamic software world um
00:36:38
now imagine if we could have such a world um if we could
00:36:42
have such an open and dynamic culture but in the networking thank
00:36:55
i
00:37:00
questions about this great presentation uh for for some questions
00:37:10
oh yes
00:37:14
uh_huh yes yes a button which affirmative duty of the remote experience some
00:37:19
as gentle as you can imagine like to challenge a couple of
00:37:23
years some sh sh oh one that's used to it's just a
00:37:28
little bit yeah that's all that was just a recursive functions
00:37:32
well just give one example of ritual yeah that's true ritual as clients
00:37:38
which you must for itself is recursive protocol itself which use the
00:37:43
routing loop uh_huh so how to punish people for us
00:37:50
when you have rituals solutions but yes so thank you that's a great question so
00:37:56
when i i usually tend to separate you know data like function in
00:37:59
controlling functions and i know that uh we do they tend to
00:38:03
use the term via net for both of them but when i at least think about a. d. n. s. server or client
00:38:09
i don't think of that as a data plane network function so
00:38:13
that is not the kind of function where you know packet comes in you could do something to to send it out
00:38:18
i consider that a more sophisticated functions and that's not something i can reason about with the model i just described
00:38:24
so this is something for you know monitoring for accounting for weeks
00:38:28
cropping for fireballs format for transporters for these types of services
00:38:33
um because they have those very specific characteristics that i talked about like recursion now
00:38:39
that doesn't mean that's you know we shouldn't be working on you know a
00:38:42
verification environment for the kinds of things you're talking about but there
00:38:46
i just see a little bit less opportunity for the automation but i'm talking about
00:38:50
so i remember so this child or a between the human effort than
00:38:54
the level of automation and the the level of the properties
00:38:57
so i think that when it comes to this kind of services you're talking about it we
00:39:02
we we will have to strike a balance which further away from automation and more into interactive environments
00:39:07
like that was that was that was talking about you know like reasoning about impart protocol
00:39:11
what would your dream vision of individual network cable civility and such
00:39:20
rachel just ritual clinton's distributions rituals lips reasons one apostle vision loss to build you a
00:39:26
it helps you to to verify tools functions is is the majority
00:39:31
would freeze approach yet just matter is dictated we'll just yet
00:39:36
we used to have little pages will drop to voice your g. e.
00:39:41
you don't you don't you skills or when it's software engineers
00:39:45
who calls it already did the consistency should justin controller
00:39:51
well so i fully agree with you but i would like to separate the kind of vision i was talking
00:39:57
about where you can change you can drop network functions into the data plane from the one you're talking
00:40:03
about what we have you know as the n. galore out in its full version everywhere i'm i'm not
00:40:09
saying that that vision won't happen but i do agree with you that there are challenges and um
00:40:14
i think we should be working on it i don't quite see exactly the solution
00:40:17
yet so that's why i'm not going there but i'm saying something different um
00:40:22
you said that what you describe are the building blocks for making this vision come true
00:40:27
i don't think that's necessary so one can have a a lot more control
00:40:32
control environment so not the full fledged as the in control of the where
00:40:36
the research communities envisioning it but still have the ability to modify
00:40:40
the network functionality so the kind of building block some talking about our
00:40:43
for instance well my dream application is about checking forces the neutrality
00:40:49
are all the network i i believe very firmly that's you know the way we use
00:40:54
networks dates very importantly sure that people have equal access and so long right
00:40:58
so i'm having a transparent network that we can very quickly prove that is being
00:41:03
neutral it's behaving correctly to what everyone for me it's a big deal
00:41:06
these we can do if we have very fight network functions that we can drop at
00:41:11
the boundaries of network domains we do not need a full fledged as the end
00:41:16
controller that you know that's fancy things with the entire network in order to do that
00:41:20
not that we shouldn't be working on it but it's a slightly different thing
00:41:35
it's a little bit blinding yeah okay uh
00:41:39
so you're offered a question that we will be resuming the presentations it

Share this talk: 


Conference program

Welcome address
Andreas Mortensen, Vice President for Research, EPFL
7 June 2018 · 9:49 a.m.
Introduction
Jim Larus, Dean of IC School, EPFL
7 June 2018 · 10 a.m.
The Young Software Engineer’s Guide to Using Formal Methods
K. Rustan M. Leino, Amazon
7 June 2018 · 10:16 a.m.
Safely Disrupting Computer Networks with Software
Katerina Argyraki, EPFL
7 June 2018 · 11:25 a.m.
Short IC Research Presentation 2: Gamified Rehabilitation with Tangible Robots
Arzu Guneysu Ozgur, EPFL (CHILI)
7 June 2018 · 12:15 p.m.
Short IC Research Presentation 3: kickoff.ai
Lucas Maystre, Victor Kristof, EPFL (LCA)
7 June 2018 · 12:19 p.m.
Short IC Research Presentation 5: CleanM
Stella Giannakopoulo, EPFL (DIAS)
7 June 2018 · 12:25 p.m.
Short IC Research Presentation 6: Understanding Cities through Data
Eleni Tzirita Zacharatou, EPFL (DIAS)
7 June 2018 · 12:27 p.m.
Short IC Research Presentation 7: Datagrowth and application trends
Matthias Olma, EPFL (DIAS)
7 June 2018 · 12:31 p.m.
Short IC Research Presentation 8: Point Cloud, a new source of knowledge
Mirjana Pavlovic, EPFL (DIAS)
7 June 2018 · 12:34 p.m.
Short IC Research Presentation 9: To Click or not to Click?
Eleni Tzirita Zacharatou, EPFL (DIAS)
7 June 2018 · 12:37 p.m.
Short IC Research Presentation 10: RaaSS Reliability as a Software Service
Maaz Mohiuddlin, LCA2, IC-EPFL
7 June 2018 · 12:40 p.m.
Short IC Research Presentation 11: Adversarial Machine Learning in Byzantium
El Mahdi El Mhamdi, EPFL (LPD)
7 June 2018 · 12:43 p.m.
20s pitch 1: Cost and Energy Efficient Data Management
Utku Sirin, (DIAS)
7 June 2018 · 2:20 p.m.
20s pitch 2: Gamification of Rehabilitation
Arzu Guneysu Ozgur, EPFL (CHILI)
7 June 2018 · 2:21 p.m.
20s pitch 4: Neural Network Guided Expression Transformation
Romain Edelmann, EPFL (LARA)
7 June 2018 · 2:21 p.m.
20s pitch 5: Unified, High Performance Data Cleaning
Stella Giannakopoulo, EPFL (DIAS)
7 June 2018 · 2:21 p.m.
20s pitch 6: Interactive Exploration of Urban Data with GPUs
Eleni Tzirita Zacharatou, EPFL (DIAS)
7 June 2018 · 2:22 p.m.
20s pitch 7: Interactive Data Exploration
Matthias Olma, EPFL (DIAS)
7 June 2018 · 2:22 p.m.
20s pitch 8: Efficient Point Cloud Processing
Mirjana Pavlovic, EPFL (DIAS)
7 June 2018 · 2:23 p.m.
20s pitch 9: To Click or not to Click?
Eleni Tzirita Zacharatou, EPFL (DIAS)
7 June 2018 · 2:24 p.m.
20s pitch 10: RaaSS Reliability as a Software Service
Maaz Mohiuddlin, LCA2, IC-EPFL
7 June 2018 · 2:24 p.m.
20s pitch 11: Adversarial Machine Learning in Byzantium
El Mahdi El Mhamdi, EPFL (LPD)
7 June 2018 · 2:24 p.m.
Machine Learning: Alchemy for the Modern Computer Scientist
Erik Meijer, Facebook
7 June 2018 · 2:29 p.m.

Recommended talks

The Lognormality Principle
Réjean Plamondon, Département de Génie Électrique École Polytechnique de Montréal
21 March 2016 · 2:05 p.m.