NetEgg: Programming Network Policies by Examples

Authors: Yifei Yuan, Rajeev Alur, Boon Thau Loo (University of Pennsylvania)

Emerging SDN DSLs may not be the best intuitive interface for programmers. The paper thus explores the problem of completely automating SDN programming. The proposed solution is NetEgg, a tool that synthesizes the controller program from examples. That is, in stead of programming with some SDN DSLs, the programmer specifies the application scenarios, or, in other words, examples.

Given user supplied examples, NetEgg generates a solution compromising of three components: the state table, the state table, and the genericprogram that processes traffic. The key in the synthesis process is to enumerate a pre-sketched policy table, exhaustively checking it against examples for consistency.

Q (Laurent Vanbever from Princeton): The output policy seems to be highly dependent of the examples supplied. Could more complex policies be synthesized? Possible examples such as TE, routing?  
A: Examples 

Q (Anduo Wang from UIUC): How to characterize/quantify input examples? What if corner cases are missing? 
A: It is debatable how complex the examples shall be. NetEgg provides no guarantee on correctness. NetEgg guarantees consistency with examples.

Q: Examples may conflict with each other, how does NetEgg deal with this?
A: NetEgg will detect inconsistency in examples.

Q: How to handle prioritized rules for IP prefixes.
A: NetEgg does not deal with priority. 

Q: How compact are the generated policies?
A: NetEgg first generates a strawman policies, then compresses it.

Q (Junchen Jiang from CMU): What is the connection to the DSL research in programming language community.
A: NetEgg is similar to Excel spreadsheet in microsoft. In fact, NetEgg cannot synthesizes a Turing complete program, the synthesis approach in general is restricted to DSL programs.

Q (A.W from UIUC): Will NetEgg synthesize policy updates (changes)?
A: Yes, NetEgg deals with this. But if the update involves change to "state table", it becomes complicated since NetEgg needs to modify the underlying logical formula.