PV1 ⊧ Zelkovaperforms one of built-in checks on an access policy

A policy analysis tool to reason about the semantics of AWS access control policies.

Application domain/field

• Cloud computing
• Access control policies
• Security

Expected input

AWS policy

Format:

• AWS policy/policies: AWS policy language, in JSON structure

Expected output

Set of declarative statements about what is true of the system. The user should check whether these findings are acceptable or not.

Internals

Tool that encodes access policies as logical formulas and uses SMT solvers to answer questions about these policies. Uses Z3, CVC4 and Z3Automata (in-house extension of Z3 to deal with regex).

Comments

The way this tool should be used has significantly changed by the CAV '22 paper. The tool now returns a detailed set of findings about the system instead of letting the user write specifications.