DNA Pairing: Using Differential Network Analysis to find Reachability Bugs

Nuno Lopes, Nikolaj Bjorner, Patrice Godefroid, Karthick Jayaraman, and George Varghese

Abstract

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.

Details

Publication typeTechReport
NumberMSR-TR-2014-58
> Publications > DNA Pairing: Using Differential Network Analysis to find Reachability Bugs