cloudsec/examples/examples_multithread.py at main · applyfmsec/cloudsec · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
import sys

sys.path.append('/home/cloudsec')
sys.path.append('/home/cloudsec/cloudsec')

from cloudsec.core import Policy, PolicyEquivalenceChecker
from cloudsec.cloud import http_api_policy_type

'''
p => q cvc5 true
q => p cvc5 false
model: [('principal_tenant', "a2cps"),
        ('principal_username', "jstubbs"),
        ('resource_tenant', "a2cps"),
        ('resource_service', "files"),
        ('resource_path', "s2/home/jstubbs"),
        ('action', "POST")]
 z3 was slow '''
def example():
    # Examples of policies
    p = Policy(policy_type=http_api_policy_type,
               principal=("a2cps", "jstubbs"),
               resource=("a2cps", "files", "s2/home/jstubbs"),
               action="GET",
               decision="allow")

    q = Policy(policy_type=http_api_policy_type,
               principal=("a2cps", "jstubbs"),
               resource=("a2cps", "files", "s2/home/jstubbs"),
               action="*",
               decision="allow")

    # Note: p => q BUT q NOT=> p
    checker = PolicyEquivalenceChecker(policy_type=http_api_policy_type,
                                       policy_set_p=[p],
                                       policy_set_q=[q], backend='*')

    print("~~~~~~ Example p=>q ~~~~~~")
    solver, result = checker.p_implies_q()
    print("\n p=>q: solver: " + solver + " :" + str(result.proved)+ " found_counter_ex: " + str(result.found_counter_ex))
    print("\n model: " + str(result.model))
    print("~~~~~~ Example q=>p ~~~~~~")
    solver,result = checker.q_implies_p()
    print("\n q=>p: solver: " + solver + " :" + str(result.proved) + " found_counter_ex: " + str(result.found_counter_ex))
    print("\n model: " + str(result.model))


'''
p=>q z3 false
model: [resource_path = "s2/home/jstubbs/",
 action = "DELETE",
 principal_username = "jstubbs",
 resource_tenant = "a2cps",
 resource_service = "files",
 principal_tenant = "a2cps"]

q=>p cvc5 true
'''
def example2():
    # Examples of policies

    a1 = Policy(policy_type=http_api_policy_type,
                principal=("a2cps", "jstubbs"),
                resource=("a2cps", "files", "s2/home/jstubbs/*"),
                action="*",
                decision="allow")

    a2 = Policy(policy_type=http_api_policy_type,
                principal=("a2cps", "jstubbs"),
                resource=("a2cps", "files", "s2/*"),
                action="PUT",
                decision="deny")

    a3 = Policy(policy_type=http_api_policy_type,
                principal=("a2cps", "jstubbs"),
                resource=("a2cps", "files", "s2/*"),
                action="POST",
                decision="deny")

    b1 = Policy(policy_type=http_api_policy_type,
                principal=("a2cps", "jstubbs"),
                resource=("a2cps", "files", "s2/home/jstubbs/a.out"),
                action="GET",
                decision="allow")

    b2 = Policy(policy_type=http_api_policy_type,
                principal=("a2cps", "jstubbs"),
                resource=("a2cps", "files", "s2/home/jstubbs/b.out"),
                action="GET",
                decision="allow")

    # Note: {b1, b2} => {a1, a2, a3}    but   {a1,a2,a3}  NOT=> {b1, b2}

    checker2 = PolicyEquivalenceChecker(policy_type=http_api_policy_type,
                                        policy_set_p=[a1, a2, a3],
                                        policy_set_q=[b1, b2], backend='*')

    print("\n ~~~~~~ Example 2 p=>q ~~~~~~")
    solver, result = checker2.p_implies_q()
    print("\n p=>q: solver: " + solver + " :" + str(result.proved) + " found_counter_ex: " + str(result.found_counter_ex))
    print("\n model: " + str(result.model))
    print("\n ~~~~~~ Example 2 q=>p ~~~~~~")
    solver,result = checker2.q_implies_p()
    print("\n q=>p: solver: " + solver + " :" + str(result.proved) + " found_counter_ex: " + str(result.found_counter_ex))
    print("\n model: " + str(result.model))