Semantic-based Automated Reasoning for AWS Access Policies using SMT Introduction Approach Policy language overview Example SMT Encoding String constraints Regular expression constraints Bit vector constraints Other operators Z3 Automata Zelkova Properties Organizational security checks Security best-practices <