<html> <head> <meta http-equiv="content-type" content="text/html; charset=utf-8"> </head> <body text="#000000" bgcolor="#FFFFFF"> Hello, Thank you for your reply! We have spent some time looking into the Skydive project to become more familiar with its functionalities and architecture and believe that there is a great opportunity for integrating with Symnet. Symnet performs static analysis based on data plane configuration of network boxes and doesn't rely on packet injection to perform verification. As you mentioned, the two tools are complementary and may validate the "real" packet behavior through the network - i.e. Skydive's inject/capture mechanism - vs that of the "symbolic" one - i.e. Symnet outputs -. However, in order to run symbolic analysis against a network topology, we also require some extra information: 1) OpenFlow tables per each OVS switch 2) Iptables rules per each namespace 3) Routing tables per each namespace We are thinking to either add these functionalities as agent probes directly in Skydive and then have Symnet consume Skydive's graph events (from Scala via the WebSocket or REST interfaces) or to directly integrate them in our Scala project. Which approach do you think is better suited? Would you consider integrating the aforementioned configuration parameters in the official Skydive project? Regards, Dragos <blockquote type="cite" style="color: #000000;">Date: Mon, 17 Jul 2017 09:46:16 +0200 From: Sylvain Afchain <a class="moz-txt-link-rfc2396E" href="mailto:safchain@redhat.com"><safchain@redhat.com></a> To: Costin Raiciu <a class="moz-txt-link-rfc2396E" href="mailto:costin.raiciu@cs.pub.ro"><costin.raiciu@cs.pub.ro></a> Cc: Radu Stoenescu <a class="moz-txt-link-rfc2396E" href="mailto:radu.stoe@gmail.com"><radu.stoe@gmail.com></a>, Matei Popovici <a class="moz-txt-link-rfc2396E" href="mailto:pdmatei@gmail.com"><pdmatei@gmail.com></a>, <a class="moz-txt-link-abbreviated" href="mailto:skydive-dev@redhat.com">skydive-dev@redhat.com</a> Subject: Re: [Skydive-dev] Integrating formal verification with Symnet into Skydive Content-Type: text/plain; charset="utf-8" Hi, Thanks for reaching out us. I'm going to define what skydive does in the context of your project. Skydive collects all the events of the monitored topology. It listens for event from netlink, ovsdb, namespaces, docker and uses connectors to external SDN controllers (Neutron, Opencontrail) to enhance the captured topology. As Skydive is listening the events we keep all the modification of the topology in a data store which allows us to see any previous version. On top of that we can start packet capture and packet generation/injection. Since there is a mapping between the flows and the topology we can track a packet along its path and see where a packet was dropped. We do support multi-level of encapsulation useful for nested deployment like container over OpenStack meaning that we do support packet tracking between two containers hosted within two VMs. That where I think your project could be useful as we are currently working on a way to write validation rules leveraging topology/packet capture/packet injection, it seems to me that Symnet provides such mechanism. Depending on the language used by Symnet (Scala ?) it could be integrated within Skydive or just consuming information gathered. Internally the topology is kept as a graph and external tools can subscribe to it or just use the API (Gremlin language). Regards, Sylvain _______________________________________________ Skydive-dev mailing list <a class="moz-txt-link-abbreviated" href="mailto:Skydive-dev@redhat.com">Skydive-dev@redhat.com</a> <a class="moz-txt-link-freetext" href="https://www.redhat.com/mailman/listinfo/skydive-dev">https://www.redhat.com/mailman/listinfo/skydive-dev</a> </blockquote> </body> </html>