Authors: Radu Stonescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu
Presenter: Radu Stonescu
Middleboxes are everywhere, NFV, In-Networking Processing,... So, reasoning about the network behavior is increasingly difficult.
SymNET answers the question, on on how the packet will be forwarded and which and how the header-fields will change through symbolic execution.
SymNET takes click-configurations as input, parses the click-config and generates a network model. Finally this can then be analyzed.
Conclusion:
SymNET can analyze stateful network, do reachability tests and loop detection.
Q: What does a "flag" mean? Is it inside the packet-header or only part of SymNET?
A: SymNET is modelling a set of values, and these "flags" are inside SymNET on a per-packet basis.
Q: Does the firewall has to communicate with SymNET?
A: SymNET has to know exactly what the firewall does. The firewall's behavior is completly known a-priori.
Q: What about asymmetric paths?
A: That's not an issue for SymNET, it can handle asymmetric paths.
Q: Can this model a caching proxy?
A: SymNET assumes that two flows are independent, so this would not be possible with a caching proxy.
No comments:
Post a Comment