CODEWITHSUNDEEP
z3z3py
Huan Sun
Huan Sun

Reputation: 177

How to automatically call a function like Or() in z3py using a loop or other methods?

I want to use z3py to implement an access policy analyzer just like AWS Zelkova. The first step I need to do is to encode the policy language into logical expressions. For instance, a control policy

effect:Allow
principal:students
action: getObject
resource: cs240/Example.pdf,cs240/Answer.pdf

should be converted into

p = students ∧ a = getObject ∧ (r = cs240/Example.pdf ∨ r = cs240/Answer.pdf)

and using z3py I can represent it as

s.add(x1 == And(a == StringVal("GetObject"),p == StringVal("tas"),Or(r == StringVal("cs240/Exam.pdf"),r == StringVal("cs240/Answer.pdf"))))

Here comes the question. When input a policy, After parsing the policy, I may get an Array of values about one key and I need to use a loop to call Or() in order to get the result as Or(r[0],r[1],...). How can I do that? I have tried something like this but obviously it doesn't work.

from z3 import *
Action = ["getObject"]
Principal = ["tas"]
Resource = ["cs240/Exam.pdf","cs240/Answer.pdf"]
a,p,r,x = Bools('a p r x')
a_t,p_t,r_t = Strings('a_t p_t r_t')
s = Solver()
for act in Action:
    a = Or(a,a_t == StringVal(act))
for principal in Principal:
    p = Or(p,p_t == StringVal(principal))
for resource in Resource:
    r = Or(r,r_t == StringVal(resource))
s.add(And(a,p,r))
print(s.check())
print(s.model())

That's the result of my program:

sat
[a_t = "", p = True, r_t = "", a = True, p_t = "", r = True]

Upvotes: 0

Views: 83

Answers (1)

alias
alias

Reputation: 30525

You should build the expression one piece at a time and add it all together. Pseudocode:

foo = False

for i in items:
   foo = Or(foo, i == ...whatever it should equal...)

s.add(foo)

When you build the expression, make sure to start the variable at False. Something like:

from z3 import *
Action = ["getObject"]
Principal = ["tas"]
Resource = ["cs240/Exam.pdf","cs240/Answer.pdf"]
a = False
p = False
r = False
a_t,p_t,r_t = Strings('a_t p_t r_t')
s = Solver()
for act in Action:
    a = Or(a,a_t == StringVal(act))
for principal in Principal:
    p = Or(p,p_t == StringVal(principal))
for resource in Resource:
    r = Or(r,r_t == StringVal(resource))
s.add(And(a,p,r))
print(s.check())
print(s.model())

This prints:

sat
[r_t = "cs240/Exam.pdf", p_t = "tas", a_t = "getObject"]

I can't tell whether this is a correct answer as I haven't really studied your constraints, but the model seems more relevant to the question.

Upvotes: 1

Related Questions