The future of static verification in networking may be obscured by two clouds: the complexity of distributed systems with highly concurrent events, and the decision-making on infrastructures growing without a premeditated plan. This poster discusses a possible solution to these issues, in which the huge space of analyzing distributed systems and the macro-questions of system evolution are addressed by a common structure, a logical implication problem which we call indirect troubleshooting. The usefulness and feasibility of indirect troubleshooting is illustrated by a preliminary realization with the chase, a remarkable process for mechanically deciding implications.

The value of database in advancing networking - in the paradigm shift from protocols to software-defined networking - was once highlighted by database-inspired management of network states. Moving beyond factual states, this paper considers semantics management a new frontier in the databases-networking knowledge “transfer”, seeking to manage network policies via structural manipulation of the corresponding software (program). As a proof of concept, we make a case of semantics-based network transformation with the datalog structure and the chase, an elegant process for handling data dependencies (semantics). Our main result is an extension of the classic chase to faure-log; a networking extension of datalog for the richer networking policies.

Traditional network state management focuses on packets that exercise network structures (configurations, procedures) and testify semantics (intentions), but provides little insights into how the structure actually "causes" the semantics. In response to this missed opportunity, we propose reflective networking, which features a network structure capable of altering itself with a causal connection to its semantics. Specifically, we investigate the network datalog structure and the chase, a process that transforms datalog programs by "executing" intents (semantic constraints) that are themselves expressed in datalog. To illustrate the usefulness of reflective networking, this demonstration presents a first use case: we developed an intuitive specification of routing in datalog, and employed the chase to summarize a network's routing behavior by minimizing (repeatedly transforming) the corresponding datalog program.

BGP and its alternatives alike, struggle with distributed policy making in the absence of a central authority: BGP prioritizes independence of the participating networks (e.g., ASes), imposes zero coordination, but has to tolerate inflexible policies each network can express. On the other hand, BGP alternatives (source routing, for example), through coordination, trade independence for flexibility, but only achieve flexibility partially. This paper asks, to achieve flexible routing, what is the fitting adjustment between network independence and coordination? To answer this question, we propose a simple principle that the sole end to interfere with the flexibility of a participating network is to prevent harms — decreasing the level of flexibility — to others. As an instantiation of this principle, we introduce the concept of policy exchange that dynamically adjusts independently set policies on the fly, and develop a preliminary implementation with conditional table, a strong knowledge representation system that allows us to distribute and manipulate policies with the usual SQL-like operators. Our preliminary experiments on realistic network topology and synthetic policies are encouraging.

Formal analysis has been intensively studied (e.g., deep customization and synergistic co-design) in the networking domain, but one assumption remains largely unexamined: there is a complete evaluation that expects definite knowledge of the task, and is expected to output a decisive result. This paper argues for a "partial" approach, a departure from the de facto, to network analysis in a practical environment with uncertain events and limited visibility. Specifically, we seek (1) loss-less modeling in which network uncertainty is explicitly handled without corrupting the querying capability; and (2) complete verification relative to the level of information available, which reaches an inconclusive result only when more information is needed. As a realization of this vision, we present fauré, a preliminary design in which a datalog extension (called fauré-log) for incomplete information is developed to enable loss-less modeling, and combined with static analysis of pure datalog to implement example relative-complete verifiers.