From 9c41f06b30811b8f2d21a3fb5032ad5f2ecb2682 Mon Sep 17 00:00:00 2001 From: "riccardo.sisto" Date: Thu, 9 Mar 2017 17:19:31 +0100 Subject: Add verigraph documentation Add design doc and installation instructions (pointing to Readme in code base). User manual will be provided in next release Change-Id: I5118894e80a36c1fc0dc29b6e6c3b59637e1b6d0 Signed-off-by: riccardo.sisto --- docs/developer/design/images/verigraph.png | Bin 0 -> 207401 bytes docs/developer/design/verigraph.rst | 43 +++++++++++++++++++++++++++++ 2 files changed, 43 insertions(+) create mode 100644 docs/developer/design/images/verigraph.png (limited to 'docs/developer') diff --git a/docs/developer/design/images/verigraph.png b/docs/developer/design/images/verigraph.png new file mode 100644 index 0000000..dfcd586 Binary files /dev/null and b/docs/developer/design/images/verigraph.png differ diff --git a/docs/developer/design/verigraph.rst b/docs/developer/design/verigraph.rst index 91d5a36..d364091 100644 --- a/docs/developer/design/verigraph.rst +++ b/docs/developer/design/verigraph.rst @@ -5,3 +5,46 @@ Parser verigraph ================= +This document provides a description of VeriGraph, a formal verification tool for service graphs. + +.. contents:: + :depth: 3 + :local: + +Overview +-------- +Given a service graph, which can include stateful network functions and their configurations +(e.g., filtering rules for firewalls, and blacklists for anti-spamming filters), VeriGraph can +accurately and quickly check reachability properties in the graph (e.g. if a particular flow of +packets can go from one node of the graph to another node). + +VeriGraph exploits Satisfiability Modulo Theories (SMT) and the general-purpose SMT solver Z3. +It includes a library of network function models. + +Architecture +------------ +VeriGraph exploits two sub-modules: + +- **Z3**, the SMT solver developed by Microsoft +- **Neo4JManger**, a module that can store service graphs into a *Neo4J* graph-oriented database + +Neo4JManager can also extract from a service graph all the VNF chains that are +relevant for checking the reachability properties of that graph. + +How the tool works +------------------ +VeriGraph accepts JSON service graph descriptions that include endpoints, VNF instances, logical +directed links connecting them, and VNF configurations. + +When VeriGraph receives a service graph and a reachability property to verify, it forwards the graph +to Neo4JManager and asks Neo4JManager to extract the chains that connect the nodes addressed by the +property to be checked. For each one of these chains, VeriGraph builds a set of first order logic +formulas that represent a mathematical model of the forwarding behavior of the chain. +This model takes into account the forwarding behavior of the links and of the VNFs included in the chain, +taking into consideration their configurations. If the formulas that make up the model are satisfiable, +this means that it is possible for a packet to traverse the chain from one end to the other. +VeriGraph passes this model to Z3 which checks its satisfiability. +Based on the satisfiability result of the formulas that model the different paths, VeriGraph finally +derives the overall result (reachability property satisfied or not). + +.. image:: /images/verigraph.png -- cgit 1.2.3-korg