Monday, December 9, 2013

CoNEXT HotMiddlebox: SymNet: Static Checking for Stateful Networks

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.

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.