From a42de79292d9541db7865b54e93be2d0b6e6a094 Mon Sep 17 00:00:00 2001
From: "serena.spinoso" <serena.spinoso@polito.it>
Date: Thu, 7 Sep 2017 10:22:39 +0200
Subject: update verigraph
JIRA: PARSER-154
code optimizations about graph manipulation and formula generation.
Change-Id: Idebef19b128281aa2bc40d1aeab6e208c7ddd93d
Signed-off-by: serena.spinoso <serena.spinoso@polito.it>
---
.../test_budapest_sap1_webserver_sat.json | 246 +++++++++++----------
.../test_budapest_sap1_webserver_unsat.json | 246 +++++++++++----------
...test_user_nat_dpi_webserver_trafficAllowed.json | 116 +++++-----
...test_user_nat_dpi_webserver_trafficBlocked.json | 116 +++++-----
...test_user_nat_vpn_fieldmod_webserver_unsat.json | 94 --------
.../testcases/test_user_nat_vpn_webserver_sat.json | 82 -------
.../test_webserver_vpn_nat_user_unsat.json | 82 -------
7 files changed, 369 insertions(+), 613 deletions(-)
delete mode 100644 verigraph/tester/testcases/test_user_nat_vpn_fieldmod_webserver_unsat.json
delete mode 100644 verigraph/tester/testcases/test_user_nat_vpn_webserver_sat.json
delete mode 100644 verigraph/tester/testcases/test_webserver_vpn_nat_user_unsat.json
(limited to 'verigraph/tester/testcases')
diff --git a/verigraph/tester/testcases/test_budapest_sap1_webserver_sat.json b/verigraph/tester/testcases/test_budapest_sap1_webserver_sat.json
index 62b4eb5..6a64eea 100644
--- a/verigraph/tester/testcases/test_budapest_sap1_webserver_sat.json
+++ b/verigraph/tester/testcases/test_budapest_sap1_webserver_sat.json
@@ -1,122 +1,128 @@
{
- "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"
- }
- ]
- }
+ "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",
+ "?type=reachability&source=sap3&destination=webserver1"
+ ],
+ "results": [
+ "SAT",
+ "SAT"
+ ],
+ "graph": {
+ "nodes": [
+ {
+ "neighbours": [
+ {
+ "name": "webserver1"
+ },
+ {
+ "name": "nat"
+ }
+ ],
+ "configuration": [
+ {
+ "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
index 211b310..e74194d 100644
--- a/verigraph/tester/testcases/test_budapest_sap1_webserver_unsat.json
+++ b/verigraph/tester/testcases/test_budapest_sap1_webserver_unsat.json
@@ -1,122 +1,126 @@
-{
- "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"
- }
- ]
- }
+{
+ "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"
+ ],
+ "results": [
+ "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
index 8e19352..227781c 100644
--- a/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficAllowed.json
+++ b/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficAllowed.json
@@ -1,59 +1,61 @@
{
- "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":[
-
- ]
- }
- ]
- }
+ "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"
+ ],
+ "results": [
+ "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
index 285ecf2..6cc5b22 100644
--- a/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficBlocked.json
+++ b/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficBlocked.json
@@ -1,59 +1,61 @@
{
- "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":[
-
- ]
- }
- ]
- }
+ "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"
+ ],
+ "results": [
+ "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
deleted file mode 100644
index 252e3b5..0000000
--- a/verigraph/tester/testcases/test_user_nat_vpn_fieldmod_webserver_unsat.json
+++ /dev/null
@@ -1,94 +0,0 @@
-{
- "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
deleted file mode 100644
index 2ae31bc..0000000
--- a/verigraph/tester/testcases/test_user_nat_vpn_webserver_sat.json
+++ /dev/null
@@ -1,82 +0,0 @@
-{
- "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
deleted file mode 100644
index 60d09b3..0000000
--- a/verigraph/tester/testcases/test_webserver_vpn_nat_user_unsat.json
+++ /dev/null
@@ -1,82 +0,0 @@
-{
- "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
--
cgit