Authors:
Radu Stoenescu -- University Politehnica of Bucharest
Matei Popovici -- University Politehnica of Bucharest
Lorina Negreanu -- University Politehnica of Bucharest
Costin Raiciu -- University Politehnica of Bucharest
Presenter : Radu Stoenescu
Networks are becoming increasingly complex entities and as we have seen before, misconfigurations can lead to errors and a lot of pain. Data planes are also become more complex with much processing being shifted done to the DP. In view of this, understanding network reachability is posing real problems. The authors believe that states verification is the way to go. So they propose following a methodology that takes a data plane snapshot, creates a network model and then uses a verification engine to verify the network model against the data plane snapshot. They have created a language for modeling called SEFL and they are proposing the verification engine called Symnet in this paper.
The authors decided to use their own modeling language due to scaling issues with C and limited functionality with approaches such as Header Space Analysis. To illustrate this, Stoenescu presents and example of symbolic execution of a piece of C code (static filtering in a firewall) to demonstrate the non-packet processing that takes place, even with only one viable path to take.
The next few minutes are spent in explaining the SEFL packet header and its memory layout and how to transform the same C code example into a SEFL representation.
Symnet is written in Scala and is about 10 KLOC. They use Z3 for constraint solving. Stoenescu demonstrates how the symbolic packet is processed according to the network model. An example of a filter + DNAT is also presented in which he illustrates how path reachability in symbolic execution reflects network reachability in practice.
The authors have developed many ready-made network models for various devices that are outlined in the paper/presentation.
The approach is evaluated with respect to model correctness, functionality and scalability, but only the latter two are dealt with in the presentation.
Symnet has its limitations in assuming that routers work properly and no performance related properties are modeled. They also cannot look at application layer protocols. Stoenescu goes on to explain their evaluation and how they ran out of memory, but revisited to optimize their approach and finally end up verifying a 500 entry table in under 8 seconds. The final word is that Symnet is comparable to HSA in terms of time taken, but that is justifiable since Symnet does inherently more complex and scalable verification.
Q : How can this be extended for stateful data plan operations?
A : There is a metadata structure in SEFL that can hold data plane state. It cannot hold state across flows, but can within. For e.g. NAT.
Q : How does Symnet scale with respect to storing state? What is a certain state has multiple values? How does it scale then?
A : Most boxes use a constant space for state. 1000 symbolic states isn't too high. (Question was taking offline).
Q : Marco Canini points out that their 2012 paper shows some techniques can be used for symbolic execution.
A : There is much work in that area (prior work pointed out). There are some malicious examples that just won't scale. Gives and example of TCP parsing from the kernel. Trying to constrain a language so permissive as C won't work in the long term because you probably have to boil those principles and lessons in the compiler so that developers obey these principles. So they decided to go towards a hardware modeling language.
Marco makes a very good point about if you are verifying high level properties, then you don't want to verify the TCP parser. Feeding packets in gets through the parsing code very very quickly.
Radu Stoenescu -- University Politehnica of Bucharest
Matei Popovici -- University Politehnica of Bucharest
Lorina Negreanu -- University Politehnica of Bucharest
Costin Raiciu -- University Politehnica of Bucharest
Presenter : Radu Stoenescu
Networks are becoming increasingly complex entities and as we have seen before, misconfigurations can lead to errors and a lot of pain. Data planes are also become more complex with much processing being shifted done to the DP. In view of this, understanding network reachability is posing real problems. The authors believe that states verification is the way to go. So they propose following a methodology that takes a data plane snapshot, creates a network model and then uses a verification engine to verify the network model against the data plane snapshot. They have created a language for modeling called SEFL and they are proposing the verification engine called Symnet in this paper.
The authors decided to use their own modeling language due to scaling issues with C and limited functionality with approaches such as Header Space Analysis. To illustrate this, Stoenescu presents and example of symbolic execution of a piece of C code (static filtering in a firewall) to demonstrate the non-packet processing that takes place, even with only one viable path to take.
The next few minutes are spent in explaining the SEFL packet header and its memory layout and how to transform the same C code example into a SEFL representation.
Symnet is written in Scala and is about 10 KLOC. They use Z3 for constraint solving. Stoenescu demonstrates how the symbolic packet is processed according to the network model. An example of a filter + DNAT is also presented in which he illustrates how path reachability in symbolic execution reflects network reachability in practice.
The authors have developed many ready-made network models for various devices that are outlined in the paper/presentation.
The approach is evaluated with respect to model correctness, functionality and scalability, but only the latter two are dealt with in the presentation.
Symnet has its limitations in assuming that routers work properly and no performance related properties are modeled. They also cannot look at application layer protocols. Stoenescu goes on to explain their evaluation and how they ran out of memory, but revisited to optimize their approach and finally end up verifying a 500 entry table in under 8 seconds. The final word is that Symnet is comparable to HSA in terms of time taken, but that is justifiable since Symnet does inherently more complex and scalable verification.
Q : How can this be extended for stateful data plan operations?
A : There is a metadata structure in SEFL that can hold data plane state. It cannot hold state across flows, but can within. For e.g. NAT.
Q : How does Symnet scale with respect to storing state? What is a certain state has multiple values? How does it scale then?
A : Most boxes use a constant space for state. 1000 symbolic states isn't too high. (Question was taking offline).
Q : Marco Canini points out that their 2012 paper shows some techniques can be used for symbolic execution.
A : There is much work in that area (prior work pointed out). There are some malicious examples that just won't scale. Gives and example of TCP parsing from the kernel. Trying to constrain a language so permissive as C won't work in the long term because you probably have to boil those principles and lessons in the compiler so that developers obey these principles. So they decided to go towards a hardware modeling language.
Marco makes a very good point about if you are verifying high level properties, then you don't want to verify the TCP parser. Feeding packets in gets through the parsing code very very quickly.
No comments:
Post a Comment