Automated Verification of Safety Properties of Declarative Networking Programs

Networks are complex systems that unfortunately are ridden with errors. Such errors can lead to disruption of services, which may have grave consequences. Verification of networks is key to elim-inating errors and building robust networks. In this paper, we pro-pose an approach to verify networks using declarative networking, where networks are specified in NDlog, a declarative language. We focus on analyzing safety properties. We develop a technique to statically analyze NDlog programs: first, we build a dependency graph of the predicates of NDlog programs; then, we build a sum-mary data structure called a derivation pool to represent all pos-sible derivations and their associated constraints for predicates in the program; finally, properties specified in first-order logic are checked on the data structure with the help of the SMT solver Z3. We build a prototype tool and demonstrate the effectiveness of the tool in validating and debugging several SDN applications