Operators in multi-tenant cloud data centers require support for diverse and complex end-to-end policies like reachability, middlebox traversals, isolation, and network resource management. In this talk, we present Genesis, a network management system which allows these policies to be specified in a declarative manner without explicitly programming the data-plane behavior.
Genesis tackles the problem of enforcing the policies by synthesizing switch forwarding tables. In doing so, it uses the formal reasoning foundations of constraint solving in combination with fast off-the-shelf SMT solvers. To improve synthesis performance, Genesis incorporates a novel search strategy that uses regular expressions to specify properties that leverage the structure of datacenter networks, and a heuristic synthesis procedure which exploits the structure of policy interactions. Overall, the approach used by Genesis is general and instrumental to building a comprehensive network management system.