Add verigraph code base

JIRA: PARSER-111

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

7 files changed, 620 insertions, 0 deletions

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