summaryrefslogtreecommitdiffstats
path: root/verigraph/tester/testcases
diff options
context:
space:
mode:
Diffstat (limited to 'verigraph/tester/testcases')
-rw-r--r--verigraph/tester/testcases/test_budapest_sap1_webserver_sat.json122
-rw-r--r--verigraph/tester/testcases/test_budapest_sap1_webserver_unsat.json122
-rw-r--r--verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficAllowed.json59
-rw-r--r--verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficBlocked.json59
-rw-r--r--verigraph/tester/testcases/test_user_nat_vpn_fieldmod_webserver_unsat.json94
-rw-r--r--verigraph/tester/testcases/test_user_nat_vpn_webserver_sat.json82
-rw-r--r--verigraph/tester/testcases/test_webserver_vpn_nat_user_unsat.json82
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