Facultatea de Automatica si Calculatoare
Universitatea Politehnica Bucuresti, Romania
Splaiul Independentei 313a
Bucuresti
Romania
|
Catedra de Calculatoare Facultatea de Automatica si Calculatoare Universitatea Politehnica Bucuresti, Romania |
Address Splaiul Independentei 313a Bucuresti Romania |
Welcome to the homepage of ERC Starting Grant project CORNET H2020 (Grant Number 758815). The project started in January 2018 and runs until December 2022.
The CORNET project aims to make programmable networks more robust by building verification software which can catch potential problems before the network is changed either via software updates or configuration changes. The end goal is to provide provable correctness guarantees to networks, ensuring operators that the network behaves as expected all the time.
To achieve provably correct networks without requiring verification expertise from network operators, CORNET runs the control plane as given, but intercepts the outputs (heading to the data plane). It verifies at runtime these control plane outputs, checking that the resulting network (data plane plus control plane forwarding rules) behaves according to the specification. When an error is detected, this is flagged to the network operators and optionally prevented from being inserted in the network (when this is possible) (see our HotNets 2017 paper).
The cornerstone of this approach is the ability to quickly check whether a given dataplane behaves correctly as per its specification. So far, we have focused on verifying programmable dataplanes specified in the P4 language. Vera was our first project targetting P4 verification, and one of two papers that first tackled this problem; the other project is p4v, from Cornell and Barefoot networks. Vera uses symbolic execution to verify quickly (under one second) that P4 programs behaved according to spec for small and medium-sized programs and catches both correctness and safety issues, but takes longer to test complex programs. This means it can be used at program development to find out possible bugs, but not at runtime to make sure the network is bug free, as we envisaged.
bf4 (bug-free P4 programs) is our second project on this topic (Sigcomm 2020). It uses verification techniques to generate simple conditions which must be obeyed at runtime by the controller, and these can be enforced at runtime very quickly (milliseconds). bf4 ensures that a running P4 program does not contain any of list of possible bugs arising from cases when the P4 program behaves in an undefined way. bf4 is reasonably also fast at development time, checking complex programs and generating the control-plane conditions in a few minutes.
The standard way to specify correctness properties is with formal languages such as CTL, but these are cumbersome to use. Instead, we propose using equivalence instead: an operator can specify that the real network must behave in the same way as an idealized network which is much easier to understand. netdiff is the tool we have built that automatically checks the equivalence of two network data planes given as input.
Finally, we have spent time trying to understand the potential impact of buggy dataplanes (see our SOSR paper), to see if well publicized attacks from traditional computing have a correspondent in the programmable dataplanes world. Our preliminary evaluation (SOSR 2020) suggests that P4 dataplanes can be exploited, but that the severity of the attacks is generally lower than in the traditional computing world.