Nuno Lopes, Nikolaj Bjorner, Patrice Godefroid, Karthick Jayaraman, and George Varghese
30 April 2014
Existing tools for network reachability such as HSA, Anteater, Veriflow and NetPlumber focus on queries for a single path and single snapshot in time – e.g., “which packets from a source to a destination pass through a middlebox?” Motivated by reachability problems in a large public cloud, we identify a need for reachability differences across multiple paths and across snapshots in time – e.g., “can packets be dropped on some load balanced paths but not others?” or “are packets being dropped which were being let through a day ago?”. We show that Datalog allows us to formulate such differential queries in space and time, and provides other useful features of a higher-level programming language such as definitions, recursion, and stratified negation. By adding a difference of cubes symbolic table representation, and an optimized filter-project operation to Datalog, we were able to complete large network benchmarks in seconds for standard and differential reachability queries. Our code is publicly available as part of the Z3 toolkit, and can be used as a foundation for deeper queries.