Add verigraph code base

JIRA: PARSER-111

Change-Id: Ie76e14fabbb6c388ebc89d9a15dd3021b25fa892
Signed-off-by: serena.spinoso <serena.spinoso@polito.it>

10 files changed, 806 insertions, 0 deletions

diff --git a/verigraph/tester/README.rst b/verigraph/tester/README.rst
new file mode 100644
index 0000000..35396a3
--- /dev/null
+++ b/verigraph/tester/README.rst
@@ -0,0 +1,38 @@
+.. This work is licensed under a Creative Commons Attribution 4.0 International License.
+.. http://creativecommons.org/licenses/by/4.0
+
+In order to run the automatic testing script test.py, you need the
+following dependencies installed on your python distribution:
+
+-  "requests" python package ->
+   http://docs.python-requests.org/en/master/
+-  "jsonschema" python package ->
+   https://pypi.python.org/pypi/jsonschema
+
+IMPORTANT - If you have multiple versions of Python installed on your
+machine, check carefully that the version you are actually using when
+running the script, has the required packages installed. Requested
+version is Python 3+
+
+| HINT - to install a package you can raise the following command (Bash
+  on Linux or DOS shell on Windows):
+| python -m pip install jsonschema
+| python -m pip install requests
+
+Tested on PYTHON 3.4.3
+
+To add a new test, just put a new .json file inside the testcases
+folder. The corresponding JSON schema is in the testcase\_schema.json
+file and some examples are already available. Each json file should
+specify:
+
+-  id, an integer for the testcase;
+-  name, the name for the testcase;
+-  description, an optional description;
+-  policy\_url\_parameters, the parameters to be appended after the
+   verification URL (including the '?' character);
+-  result, the expected verification result;
+-  graph, the graph to be tested (the same object that you usually POST
+   to VeriGraph to create a new graph).
+   The test.py script will test each .json file contained into the
+   testcases folder and will provide a complete output.
diff --git a/verigraph/tester/test.py b/verigraph/tester/test.py
new file mode 100644
index 0000000..ad0b82a
--- /dev/null
+++ b/verigraph/tester/test.py
@@ -0,0 +1,115 @@
+#!/usr/bin/python
+
+##############################################################################
+# Copyright (c) 2017 Politecnico di Torino and others.
+#
+# All rights reserved. This program and the accompanying materials
+# are made available under the terms of the Apache License, Version 2.0
+# which accompanies this distribution, and is available at
+# http://www.apache.org/licenses/LICENSE-2.0
+##############################################################################
+
+from __future__ import print_function
+from jsonschema import validate
+from pprint import pprint
+import sys
+import requests
+from requests.exceptions import *
+from jsonschema.exceptions import *
+import json
+import getopt
+import os
+import subprocess
+
+# Constants (change them, if appropriate)
+VERIGRAPH_PORT = "8080"
+TEST_CASES_DIR = "testcases"
+BASE_URL = "http://localhost:"+VERIGRAPH_PORT+"/verify/api/graphs/"
+SCHEMA_FILE = "testcase_schema.json"
+
+# Variables
+success = 0
+run = 0
+
+# Utils
+def eprint(toPrint):
+    sys.stdout.flush()
+    print(toPrint, file=sys.stderr)
+    sys.stderr.flush()
+
+# Print PYTHON ver
+print("PYTHON " + sys.version)
+
+# Loading schema file
+try:
+    schema = json.load(open(SCHEMA_FILE))
+except ValueError:
+    eprint("Invalid json schema (check your "+SCHEMA_FILE+")!\nExiting.")
+    exit(-1)
+
+# Iterate over .json files contained in the TEST_CASES_DIR
+for i in os.listdir(TEST_CASES_DIR):
+    if i.endswith(".json"): 
+        with open(TEST_CASES_DIR+os.path.sep+i) as data_file:
+            try:
+                # Load json file (raise exception if malformed)
+                data = json.load(data_file)
+
+                # Validate input json against schema (raise exception if invalid)
+                validate(data, schema)
+
+                run += 1
+                print("Test case ID: "+str(data["id"]))
+                print("\tFILE NAME: "+i)
+                print("\tTEST NAME: "+data["name"])
+                print("\tTEST DESCRIPTION: "+data["description"])
+
+                # POST the graph
+                r = requests.post(BASE_URL, json=data["graph"])
+                if r.status_code == 201:
+                    graph_id = r.json()["id"]
+                    print("\tCreated Graph has ID " + str(graph_id) + " on VeriGraph")
+
+                    # GET the policy verification result
+                    policy = requests.get(BASE_URL+str(graph_id)+"/policy"+data["policy_url_parameters"])
+
+                    # Check the response
+                    if policy.status_code == 200:
+                        print("\tVerification result is " + policy.json()["result"])
+
+                        # Check the result with the expected one
+                        if policy.json()["result"] == data["result"]:
+                            # SUCCESS
+                            print("\t+++ Test passed +++")
+                            success += 1
+                        else:
+                            # FAIL
+                            eprint("\t[ERROR] Expected result was " + data["result"] + " but VeriGraph returned " + policy.json()["result"])
+                            print("\t--- Test failed ---")
+                    else:
+                        print("\tVeriGraph returned an unexpected response -> " + str(policy.status_code), policy.reason)
+                        print("\t--- Test failed ---")
+                print()
+            except ValueError:
+                print("Malformed json!\nSkipping "+i+" file")
+                print("\t--- Test failed ---")
+            except ValidationError:
+                print("Invalid json (see Schema file)!\nSkipping "+i+" file")
+                print("\t--- Test failed ---")
+            except ConnectionError:
+                print("Connection refused!")
+                print("\t--- Test failed ---")
+            except HTTPError:
+                print("HTTP error!")
+                print("\t--- Test failed ---")
+
+# Final output
+print("\nTest run = "+str(run))
+print("Test succeded = "+str(success))
+if run != 0:
+    if success != run:
+        print("\n --- Some tests failed. See the output. ---")
+    else:
+        print("\n +++ All tests passed +++")
+else:
+    print("\n\n +++ 0 tests executed +++")
\ No newline at end of file
diff --git a/verigraph/tester/testcase_schema.json b/verigraph/tester/testcase_schema.json
new file mode 100644
index 0000000..b069705
--- /dev/null
+++ b/verigraph/tester/testcase_schema.json
@@ -0,0 +1,33 @@
+{
+    "$schema": "http://json-schema.org/draft-04/schema#",
+    "title": "Testcase",
+    "description": "A testcase for VeriGraph",
+    "type": "object",
+    "properties": {
+        "id": {
+            "description": "The unique identifier for a testcase",
+            "type": "integer"
+        },
+        "name": {
+            "description": "Name of the testcase",
+            "type": "string"
+        },
+        "description": {
+            "description": "A description for the testcase, specifying what is going to be tested",
+            "type": "string"
+        },
+        "policy_url_parameters": {
+            "description": "The set of parameters to be passed in GET request to the verification service",
+            "type": "string"
+        },
+        "result": {
+            "description": "The set of parameters to be passed in GET request to the verification service",
+            "type": "string"
+        },
+        "graph": {
+        	"description": "The graph to be tested",
+        	"type": "object"
+        }
+    },
+    "required": ["id", "name", "policy_url_parameters", "result", "graph"]
+}
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_budapest_sap1_webserver_sat.json b/verigraph/tester/testcases/test_budapest_sap1_webserver_sat.json
new file mode 100644
index 0000000..62b4eb5
--- /dev/null
+++ b/verigraph/tester/testcases/test_budapest_sap1_webserver_sat.json
@@ -0,0 +1,122 @@
+{
+   "id":6,
+   "name":"budapest_test_case_sat",
+   "description":"This test case verifies budapest scenario, chain sap1->webserver1",
+   "policy_url_parameters":"?type=reachability&source=sap1&destination=webserver1",
+   "result":"SAT",
+   "graph": {
+      "nodes":[
+         {
+            "neighbours":[
+               {
+                  "name":"webserver1"
+               },
+               {
+                  "name":"nat"
+               }
+            ],
+            "configuration":[
+               {
+                  "ip_sap1":"webserver1"
+               }
+            ],
+            "name":"fw",
+            "functional_type":"firewall"
+         },
+         {
+            "neighbours":[
+               {
+                  "name":"sap3"
+               },
+               {
+                  "name":"fw"
+               }
+            ],
+            "name":"webserver1",
+            "functional_type":"webserver"
+         },
+         {
+            "neighbours":[
+               {
+                  "name":"sap1"
+               },
+               {
+                  "name":"dpi"
+               },
+               {
+                  "name":"fw"
+               }
+            ],
+            "configuration":[
+               "sap1",
+               "sap2"
+            ],
+            "name":"nat",
+            "functional_type":"nat"
+         },
+         {
+            "neighbours":[
+               {
+                  "name":"sap2"
+               }
+            ],
+            "configuration":[
+               "drug"
+            ],
+            "name":"dpi",
+            "functional_type":"dpi"
+         },
+         {
+            "neighbours":[
+               {
+                  "name":"nat"
+               }
+            ],
+            "configuration":[
+               {
+                  "url":"www.facebook.com",
+                  "body":"cats",
+                  "destination":"webserver1",
+                  "protocol":"HTTP_REQUEST"
+               }
+            ],
+            "name":"sap2",
+            "functional_type":"endhost"
+         },
+         {
+            "neighbours":[
+               {
+                  "name":"nat"
+               }
+            ],
+            "configuration":[
+               {  
+                  "url":"www.facebook.com",
+                  "body":"cats",
+                  "destination":"webserver1",
+                  "protocol":"HTTP_REQUEST"
+               }
+            ],
+            "name":"sap1",
+            "functional_type":"endhost"
+         },
+         {
+            "neighbours":[
+               {
+                  "name":"webserver1"
+               }
+            ],
+            "configuration":[
+               {
+                  "url":"www.facebook.com",
+                  "body":"cats",
+                  "destination":"webserver1",
+                  "protocol":"HTTP_REQUEST"
+               }
+            ],
+            "name":"sap3",
+            "functional_type":"endhost"
+         }
+      ]
+   }
+}
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_budapest_sap1_webserver_unsat.json b/verigraph/tester/testcases/test_budapest_sap1_webserver_unsat.json
new file mode 100644
index 0000000..211b310
--- /dev/null
+++ b/verigraph/tester/testcases/test_budapest_sap1_webserver_unsat.json
@@ -0,0 +1,122 @@
+{  
+   "id":7,
+   "name":"budapest_test_case_unsat",
+   "description":"This test case verifies budapest scenario, chain sap1->webserver1 with fw blocking",
+   "policy_url_parameters":"?type=reachability&source=sap1&destination=webserver1",
+   "result":"UNSAT",
+   "graph":{
+      "nodes":[
+         {
+            "neighbours":[
+               {
+                  "name":"webserver1"
+               },
+               {
+                  "name":"nat"
+               }
+            ],
+            "configuration":[
+               {
+                  "webserver1":"nat"
+               }
+            ],
+            "name":"fw",
+            "functional_type":"firewall"
+         },
+         {
+            "neighbours":[
+               {
+                  "name":"sap3"
+               },
+               {
+                  "name":"fw"
+               }
+            ],
+            "name":"webserver1",
+            "functional_type":"webserver"
+         },
+         {
+            "neighbours":[
+               {
+                  "name":"sap1"
+               },
+               {
+                  "name":"dpi"
+               },
+               {
+                  "name":"fw"
+               }
+            ],
+            "configuration":[
+               "sap1",
+               "sap2"
+            ],
+            "name":"nat",
+            "functional_type":"nat"
+         },
+         {
+            "neighbours":[
+               {
+                  "name":"sap2"
+               }
+            ],
+            "configuration":[
+               "drug"
+            ],
+            "name":"dpi",
+            "functional_type":"dpi"
+         },
+         {
+            "neighbours":[
+               {
+                  "name":"nat"
+               }
+            ],
+            "configuration":[
+               {
+                  "url":"www.facebook.com",
+                  "body":"cats",
+                  "destination":"webserver1",
+                  "protocol":"HTTP_REQUEST"
+               }
+            ],
+            "name":"sap2",
+            "functional_type":"endhost"
+         },
+         {
+            "neighbours":[
+               {
+                  "name":"nat"
+               }
+            ],
+            "configuration":[
+               {
+                  "url":"www.facebook.com",
+                  "body":"cats",
+                  "destination":"webserver1",
+                  "protocol":"HTTP_REQUEST"
+               }
+            ],
+            "name":"sap1",
+            "functional_type":"endhost"
+         },
+         {
+            "neighbours":[
+               {
+                  "name":"webserver1"
+               }
+            ],
+            "configuration":[
+               {
+                  "url":"www.facebook.com",
+                  "body":"cats",
+                  "destination":"webserver1",
+                  "protocol":"HTTP_REQUEST"
+               }
+            ],
+            "name":"sap3",
+            "functional_type":"endhost"
+         }
+      ]
+   }
+}
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficAllowed.json b/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficAllowed.json
new file mode 100644
index 0000000..8e19352
--- /dev/null
+++ b/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficAllowed.json
@@ -0,0 +1,59 @@
+{
+	"id": 2,
+	"name": "simple_test_case",
+	"description": "This test case contains a graph with client, firewall and server",
+	"policy_url_parameters": "?type=reachability&source=user1&destination=webserver",
+	"result": "SAT",
+	"graph": {
+	   "nodes":[
+	      {
+	         "name":"user1",
+	         "functional_type":"endhost",
+	         "neighbours":[
+	            {
+	               "name":"nat"
+	            }
+	         ],
+	        "configuration": 
+	            [
+					{
+						"body": "cartoon",
+						"protocol": "HTTP_REQUEST",
+						"destination": "webserver"
+					}
+	            ]
+	      },
+	      {
+	         "name":"nat",
+	         "functional_type":"nat",
+	         "neighbours":[
+	            {
+	               "name":"dpi"
+	            }
+	         ],
+	         "configuration":[
+	            "user1"
+	         ]
+	      },
+	      {
+	         "name":"dpi",
+	         "functional_type":"dpi",
+	         "neighbours":[
+	            {
+	               "name":"webserver"
+	            }
+	         ],
+	         "configuration":[
+	           "sex", "droga"
+	         ]
+	      },
+	      {
+	         "name":"webserver",
+	         "functional_type":"webserver",
+	         "neighbours":[
+	
+	         ]
+	      }
+	   ]
+	}
+}
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficBlocked.json b/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficBlocked.json
new file mode 100644
index 0000000..285ecf2
--- /dev/null
+++ b/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficBlocked.json
@@ -0,0 +1,59 @@
+{
+	"id": 1,
+	"name": "simple_test_case",
+	"description": "This test case contains a graph with client, firewall and server",
+	"policy_url_parameters": "?type=reachability&source=user1&destination=webserver",
+	"result": "UNSAT",
+	"graph": {
+	   "nodes":[
+	      {
+	         "name":"user1",
+	         "functional_type":"endhost",
+	         "neighbours":[
+	            {
+	               "name":"nat"
+	            }
+	         ],
+	        "configuration": 
+	            [
+					{
+						"body": "sex",
+						"protocol": "HTTP_REQUEST",
+						"destination": "webserver"
+					}
+	            ]
+	      },
+	      {
+	         "name":"nat",
+	         "functional_type":"nat",
+	         "neighbours":[
+	            {
+	               "name":"dpi"
+	            }
+	         ],
+	         "configuration":[
+	            "user1"
+	         ]
+	      },
+	      {
+	         "name":"dpi",
+	         "functional_type":"dpi",
+	         "neighbours":[
+	            {
+	               "name":"webserver"
+	            }
+	         ],
+	         "configuration":[
+	           "sex", "droga"
+	         ]
+	      },
+	      {
+	         "name":"webserver",
+	         "functional_type":"webserver",
+	         "neighbours":[
+	
+	         ]
+	      }
+	   ]
+	}
+}
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_user_nat_vpn_fieldmod_webserver_unsat.json b/verigraph/tester/testcases/test_user_nat_vpn_fieldmod_webserver_unsat.json
new file mode 100644
index 0000000..252e3b5
--- /dev/null
+++ b/verigraph/tester/testcases/test_user_nat_vpn_fieldmod_webserver_unsat.json
@@ -0,0 +1,94 @@
+{
+	"id": 4,
+	"name": "nat_vpn_with_fieldmodifier_test_case",
+	"description": "This test case contains a graph with client, nat, vpn (with field mod in between) and server",
+	"policy_url_parameters": "?type=reachability&source=user1&destination=webserver",
+	"result": "UNSAT",
+	"graph": {
+	   "nodes":[
+	      {
+	         "name":"user1",
+	         "functional_type":"endhost",
+	         "neighbours":[
+	            {
+	               "name":"nat"
+	            }
+	         ],
+	        "configuration": 
+	            [
+					{
+						"body": "cartoon",
+						"protocol": "HTTP_REQUEST",
+						"destination": "webserver"
+					}
+	            ]
+	      },
+	      {
+	         "name":"nat",
+	         "functional_type":"nat",
+	         "neighbours":[
+	            {
+	               "name":"user1"
+	            },
+	            {
+	               "name":"vpnaccess"
+	            }
+	         ],
+	         "configuration":[
+	            "user1"
+	         ]
+	      },
+	      {
+	         "name":"vpnaccess",
+	         "functional_type":"vpnaccess",
+	         "neighbours":[
+	         	{
+	               "name":"nat"
+	            },
+	            {
+	               "name":"fieldmodifier"
+	            }
+	         ],
+	         "configuration":[
+	            {"vpnexit": "vpnexit"}
+	         ]
+	      },
+	      {
+	         "name":"fieldmodifier",
+	         "functional_type":"fieldmodifier",
+	         "neighbours":[
+	         	{
+	               "name":"vpnaccess"
+	            },
+	            {
+	               "name":"vpnexit"
+	            }
+	         ]
+	      },
+	      {
+	         "name":"vpnexit",
+	         "functional_type":"vpnexit",
+	         "neighbours":[
+	            {
+	               "name":"fieldmodifier"
+	            },
+	            {
+	               "name":"webserver"
+	            }
+	         ],
+	         "configuration":[
+	            {"vpnaccess": "vpnaccess"}
+	         ]
+	      },
+	      {
+	         "name":"webserver",
+	         "functional_type":"webserver",
+	         "neighbours":[
+	         	{
+	         		"name": "vpnexit"
+	         	}
+	         ]
+	      }
+	   ]
+	}
+}
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_user_nat_vpn_webserver_sat.json b/verigraph/tester/testcases/test_user_nat_vpn_webserver_sat.json
new file mode 100644
index 0000000..2ae31bc
--- /dev/null
+++ b/verigraph/tester/testcases/test_user_nat_vpn_webserver_sat.json
@@ -0,0 +1,82 @@
+{
+	"id": 3,
+	"name": "nat_vpn_test_case",
+	"description": "This test case contains a graph with client, nat, vpn and server",
+	"policy_url_parameters": "?type=reachability&source=user1&destination=webserver",
+	"result": "SAT",
+	"graph": {
+	   "nodes":[
+	      {
+	         "name":"user1",
+	         "functional_type":"endhost",
+	         "neighbours":[
+	            {
+	               "name":"nat"
+	            }
+	         ],
+	        "configuration":
+	            [
+					{
+						"body": "cartoon",
+						"protocol": "HTTP_REQUEST",
+						"destination": "webserver"
+					}
+	            ]
+	      },
+	      {
+	         "name":"nat",
+	         "functional_type":"nat",
+	         "neighbours":[
+	            {
+	               "name":"user1"
+	            },
+	            {
+	               "name":"vpnaccess"
+	            }
+	         ],
+	         "configuration":[
+	            "user1"
+	         ]
+	      },
+	      {
+	         "name":"vpnaccess",
+	         "functional_type":"vpnaccess",
+	         "neighbours":[
+	         	{
+	               "name":"nat"
+	            },
+	            {
+	               "name":"vpnexit"
+	            }
+	         ],
+	         "configuration":[
+	            {"vpnexit": "vpnexit"}
+	         ]
+	      },
+	      {
+	         "name":"vpnexit",
+	         "functional_type":"vpnexit",
+	         "neighbours":[
+	            {
+	               "name":"vpnaccess"
+	            },
+	            {
+	               "name":"webserver"
+	            }
+	         ],
+	         "configuration":[
+	            {"vpnaccess": "vpnaccess"}
+	         ]
+	      },
+	      {
+	         "name":"webserver",
+	         "functional_type":"webserver",
+	         "neighbours":[
+	         	{
+	         		"name": "vpnexit"
+	         	}
+	         ]
+	      }
+	   ]
+	}
+}
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_webserver_vpn_nat_user_unsat.json b/verigraph/tester/testcases/test_webserver_vpn_nat_user_unsat.json
new file mode 100644
index 0000000..60d09b3
--- /dev/null
+++ b/verigraph/tester/testcases/test_webserver_vpn_nat_user_unsat.json
@@ -0,0 +1,82 @@
+{
+	"id": 5,
+	"name": "nat_vpn_test_case_serv_to_user",
+	"description": "This test case contains a graph with client, nat, vpn and server. webserver -> client",
+	"policy_url_parameters": "?type=reachability&source=webserver&destination=user1",
+	"result": "UNSAT",
+	"graph": {
+	   "nodes":[
+	      {
+	         "name":"user1",
+	         "functional_type":"endhost",
+	         "neighbours":[
+	            {
+	               "name":"nat"
+	            }
+	         ],
+	        "configuration":
+	            [
+					{
+						"body": "cartoon",
+						"protocol": "HTTP_REQUEST",
+						"destination": "webserver"
+					}
+	            ]
+	      },
+	      {
+	         "name":"nat",
+	         "functional_type":"nat",
+	         "neighbours":[
+	            {
+	               "name":"user1"
+	            },
+	            {
+	               "name":"vpnaccess"
+	            }
+	         ],
+	         "configuration":[
+	            "user1"
+	         ]
+	      },
+	      {
+	         "name":"vpnaccess",
+	         "functional_type":"vpnaccess",
+	         "neighbours":[
+	         	{
+	               "name":"nat"
+	            },
+	            {
+	               "name":"vpnexit"
+	            }
+	         ],
+	         "configuration":[
+	            {"vpnexit": "vpnexit"}
+	         ]
+	      },
+	      {
+	         "name":"vpnexit",
+	         "functional_type":"vpnexit",
+	         "neighbours":[
+	            {
+	               "name":"vpnaccess"
+	            },
+	            {
+	               "name":"webserver"
+	            }
+	         ],
+	         "configuration":[
+	            {"vpnaccess": "vpnaccess"}
+	         ]
+	      },
+	      {
+	         "name":"webserver",
+	         "functional_type":"webserver",
+	         "neighbours":[
+	         	{
+	         		"name": "vpnexit"
+	         	}
+	         ]
+	      }
+	   ]
+	}
+}
\ No newline at end of file