Verifying networks with symbolic execution and temporal logic

1 VERIFYING NETWORKS WITH SYMBOLIC EXECUTION Symbolic execution is a promising approach to network veri cation [5, 6]. Inspired from software veri cation where it is mainly used to generate test-cases (e.g. [1]), symbolic execution is a technique for exploring all viable execution paths of a program. Symbolic execution runs programs with symbolic inputs instead of concrete ones. Such an input models all possible values in it’s range. When executing conditional instructions, program execution is branched. In the case of an if statement, both the then and the else branches of the program will be explored, and the condition (resp. its complement) will be added as a constraint on each execution path. Adding constraints to a symbolic variable will restrict the values in its range. Constraints are added during branching as well as when executing other non-branching instructions (e.g. assignment). If constraints are unsatis able on a program branch, execution stops on that branch. The output of symbolic execution consists of all satis ed execution branches and for each branch — the set of constraints on each variable. To deploy symbolic execution for verifying networks, the topology is interpreted as a single program whose input is a symbolic packet (i.e. a packet having possibly symbolic header elds). The execution paths of such a program correspond to the set of all possible paths the packet may take through the network. Symnet [6] takes on this approach. Symnet is a symbolic execution engine which runs on SEFL (Symbolic Execution Friendly Language) programs. SEFL is a minimalist imperative language speci cally designed for: (i) modelling network processing and (ii) fast symbolic execution. To verify a network topology, each of its components (and the topology itself) are translated to SEFL code. Symnet is fast and can check large-scale networks (e.g. the Stanford backbone) in seconds.