Fauré: A Partial Approach to Network Analysis

ABSTRACTFormal 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.