diff options
| -rw-r--r-- | docs/developer/design/images/verigraph.png | bin | 0 -> 207401 bytes | |||
| -rw-r--r-- | docs/developer/design/verigraph.rst | 43 | ||||
| -rw-r--r-- | docs/release/installation/installation.instruction.rst | 26 | ||||
| -rw-r--r-- | docs/release/release-notes/release-notes.rst | 4 |
4 files changed, 73 insertions, 0 deletions
diff --git a/docs/developer/design/images/verigraph.png b/docs/developer/design/images/verigraph.png Binary files differnew file mode 100644 index 0000000..dfcd586 --- /dev/null +++ b/docs/developer/design/images/verigraph.png 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 diff --git a/docs/release/installation/installation.instruction.rst b/docs/release/installation/installation.instruction.rst index 999080c..de6956a 100644 --- a/docs/release/installation/installation.instruction.rst +++ b/docs/release/installation/installation.instruction.rst @@ -105,3 +105,29 @@ Step 2: Install the policy2tosca module. python setup.py install +Parser verigraph installation +============================= + +In the present release, verigraph requires that the following software is also installed: + +- Java 1.8 (with javac compiler) +- Apache Tomcat 8 +- Microsoft Z3 (https://github.com/Z3Prover/bin/tree/master/releases) +- Neo4J (https://neo4j.org) + +Please follow the below installation steps to install verigraph. + +Step 1: Clone the parser project. + +.. code-block:: bash + + git clone https://gerrit.opnfv.org/gerrit/parser + +Step 2: Go to the verigraph directory. + +.. code-block:: bash + + cd parser/verigraph + +Step3: Follow the instructions in README.rst for downloading verigraph +dependencies and for installing verigraph. diff --git a/docs/release/release-notes/release-notes.rst b/docs/release/release-notes/release-notes.rst index c5360f9..5d62b74 100644 --- a/docs/release/release-notes/release-notes.rst +++ b/docs/release/release-notes/release-notes.rst @@ -94,6 +94,10 @@ Feature additions +--------------------------------------+--------------------------------------+ | | | +--------------------------------------+--------------------------------------+ +| PARSER-111 | Verigraph Code Base | +| | | ++--------------------------------------+--------------------------------------+ + Bug corrections ~~~~~~~~~~~~~~~~~~~~~ |
