docs/developer/design/verigraph.rst

   1 .. This work is licensed under a Creative Commons Attribution 4.0 International License.
   2 .. http://creativecommons.org/licenses/by/4.0
   3
   4 ================
   5 Parser verigraph
   6 ================
   7
   8 This document provides a description of VeriGraph, a formal verification tool for service graphs.
   9
  10 .. contents::
  11    :depth: 3
  12    :local:
  13
  14 Overview
  15 --------
  16 Given a service graph, which can include stateful network functions and their configurations
  17 (e.g., filtering rules for firewalls, and blacklists for anti-spamming filters), VeriGraph can
  18 accurately and quickly check reachability properties in the graph (e.g. if a particular flow of
  19 packets can go from one node of the graph to another node).
  20
  21 VeriGraph exploits Satisfiability Modulo Theories (SMT) and the general-purpose SMT solver Z3.
  22 It includes a library of network function models.
  23
  24 Architecture
  25 ------------
  26 VeriGraph exploits two sub-modules:
  27
  28 - **Z3**, the SMT solver developed by Microsoft
  29 - **Neo4J**, a Java-based graph-oriented database
  30
  31 The Neo4J database is used for service graph manipulation and to extract from a
  32 service graph all the VNF chains that are relevant for checking the reachability
  33 properties of that graph.
  34
  35 How the tool works
  36 ------------------
  37 VeriGraph accepts JSON service graph descriptions that include endpoints, VNF instances, logical
  38 directed links connecting them, and VNF configurations.
  39
  40 When VeriGraph receives a service graph and a reachability property to verify, it saves the graph
  41 into Neo4J and it extracts the chains that connect the nodes addressed by the property to be
  42 checked. For each one of these chains, VeriGraph builds a set of first order logic formulas that
  43 represent a mathematical model of the forwarding behavior of the chain.
  44 This model takes into account the forwarding behavior of the links and of the VNFs included in the
  45 chain, taking into consideration their configurations. If the formulas that make up the model are
  46 satisfiable, this means that it is possible for a packet to traverse the chain from one end to the
  47 other. VeriGraph passes this model to Z3 which checks its satisfiability.
  48 Based on the satisfiability result of the formulas that model the different paths, VeriGraph finally
  49 derives the overall result (reachability property satisfied or not).
  50
  51 .. image:: /images/verigraph.png