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

Expected input

Two AWS policies to compare or one AWS policy and the name of a built-in Zelkova check.

Format:

Expected output

When comparing policies: it returns whether the first policy in the payload is less permissive, more permissive, equivalent or incomparable with respect to the second policy For built-in Zelkova check: returns true or false based on whether the check is satisfied. It can also return unknown if it could not handle a construct in the policy or the solver times out.

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).
Security

Related papers

https://doi.org/10.23919/FMCAD.2018.8602994 (FMCAD '18)

Last publication date

2018

Related tools

SecGuru, IAM Access Analyzer

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.