Semantic-based Automated Reasoning for AWS Access Policies using SMT

Cloud computing provides on-demand access to IT resources via the Internet. Permissions for these resources are defined by expressive access control policies. This paper presents a formalization of the Amazon Web Services (AWS) policy language and a corresponding analysis tool, called ZELKOVA, for verifying policy properties. ZELKOVA encodes the semantics of policies into SMT, compares behaviors, and verifies properties. It provides users a sound mechanism to detect misconfigurations of their policies. ZELKOVA solves a PSPACE-complete problem and is invoked many millions of times daily.

• Publication year

  2018

• Venue

  Formal Methods in Computer-Aided Design

• Publication date

  2018-10-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.23919/FMCAD.2018.8602994
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• ZSstrS: A string solver with theory-aware heuristics

  2017cited by this paper
• Automata-Based Model Counting for String Constraints

  2015cited by this paper
• Automated Analysis and Debugging of Network Connectivity Policies

  2014cited by this paper
• Z3: An Efficient SMT Solver

  2008cited by this paper
• Automated verification of access control policies using a SAT solver

  2008cited by this paper
• Specifying and Reasoning About Dynamic Access-Control Policies

  2006cited by this paper
• Verification and change-impact analysis of access-control policies

  2005cited by this paper
• Cassandra: flexible trust management, applied to electronic health records

  2004cited by this paper
• Model-Checking Access Control Policies

  2004cited by this paper
• Specification and verification of constraints in role based access control

  2003cited by this paper
• DATALOG with Constraints: A Foundation for Trust Management Languages

  2003cited by this paper
• EXtensible Access Control Markup Language (XACML) version 1

  2003cited by this paper
• Binder, a logic-based security language

  2002cited by this paper
• An algebra for composing access control policies

  2002cited by this paper
• SD3: a trust management system with certified evaluation

  2001cited by this paper
• Delegation Logic: A Logic-based Approach to Distrbuted Authorization

  2000cited by this paper
• An n log n algorithm for minimizing states in a finite automaton

  1971cited by this paper

• LLM-based Iterative Requirements Refinement in FSM with IEC 61499 Code Generation

  2025cites this paper
• Modeling the AWS Authorization Engine

  2025influential citation
• Per-Instance Subproblem Generation for Strategy Selection in SMT

  2025cites this paper
• BLIPS-PA: a qualitative-physics-based method for fault causality and probabilistic analysis of novel designs

  2025cites this paper
• Mechanics of Learned Reasoning 1: TempoBench, A Benchmark for Interpretable Deconstruction of Reasoning System Performance

  2025cites this paper
• LEOPARD: Accelerating Cloud-based Access Control Policy Verification Using Logical Encoding Optimization

  2025influential citation
• Exploring Large Language Models for Access Control Policy Synthesis and Summarization

  2025cites this paper
• Intent-Driven Network Isolation for the Cloud Computing Continuum

  2025cites this paper
• Analyzing Action Interference of Administrative Obligations for SMT-Based Verification

  2025cites this paper
• Relia: Accelerating the Analysis of Cloud Access Control Policies

  2025cites this paper
• Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems

  2025cites this paper
• Formal Methods for Verifying Authorization Policy in Microservice Systems

  2025cites this paper
• Logika: the Sireum verification framework

  2025cites this paper
• OSTRICH2: Solver for Complex String Constraints

  2025cites this paper
• HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)

  2025cites this paper
• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification

  2025cites this paper
• Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis

  2025cites this paper
• Synthesizing Access Control Policies Using Large Language Models

  2025cites this paper
• S2s: An Eager SMT Solver for Strings

  2025cites this paper
• Models for formal methods and tools: the case of railway systems

  2025cites this paper
• Automated Infrastructure as Code Program Testing

  2024cites this paper
• Test-suite-guided discovery of least privilege for cloud infrastructure as code

  2024cites this paper
• CloudLens: Modeling and Detecting Cloud Security Vulnerabilities

  2024cites this paper
• Projective Model Counting for IP Addresses in Access Control Policies

  2024influential citation
• Extending DRAT to SMT

  2024cites this paper
• Integrating SMT solvers into Goal-Directed Answer Set Programming, Challenges and Directions

  2024cites this paper
• Cloud Resource Protection via Automated Security Property Reasoning

  2024cites this paper
• Validating SMT Solvers for Correctness and Performance via Grammar-Based Enumeration

  2024cites this paper
• Automatically Reducing Privilege for Access Control Policies

  2024cites this paper
• Software Security Analysis in 2030 and Beyond: A Research Roadmap

  2024cites this paper
• Solving String Constraints with Concatenation Using SAT

  2024cites this paper
• Detecting Covert Channels in Cloud Access Control Policies Using Large Language Models

  2024cites this paper
• Formal Methods in Industry

  2024cites this paper
• Systematic literature review on security misconfigurations in web applications

  2024cites this paper
• An intent-based solution for network isolation in Kubernetes

  2024cites this paper
• Security Automation in next-generation Networks and Cloud environments

  2024cites this paper
• Static and Dynamic Analysis of a Usage Control System

  2024cites this paper
• Diffy: Data-Driven Bug Finding for Configurations

  2024cites this paper
• GRASP: Hardening Serverless Applications through Graph Reachability Analysis of Security Policies

  2024influential citation
• Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization

  2024cites this paper
• Scaling Data Science Solutions with Semantics and Machine Learning: Bosch Case

  2023cites this paper
• Least-Privilege Calls to Amazon Web Services

  2023cites this paper
• Automated Security Assessments of Amazon Web Services Environments

  2023cites this paper
• Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively

  2023cites this paper
• Incremental Dead State Detection in Logarithmic Time

  2023cites this paper
• SoK: Run-time security for cloud microservices. Are we there yet?

  2023cites this paper
• Algorithm selection for SMT

  2023cites this paper
• Towards Reliable Infrastructure as Code

  2023cites this paper
• Greybox Penetration Testing on Cloud Access Control with IAM Modeling and Deep Reinforcement Learning

  2023cites this paper
• Specifying a Usage Control System

  2023cites this paper
• Interactive Greybox Penetration Testing on Cloud Access Control with IAM Modeling and Deep Reinforcement Learning

  2023cites this paper
• Quantitative Policy Repair for Access Control on the Cloud

  2023cites this paper
• Solving String Constraints Using SAT

  2023cites this paper
• SMT-Based Verification of NGAC Policies

  2023cites this paper
• Detecting Multi-Step IAM Attacks in AWS Environments via Model Checking

  2023cites this paper
• Generating and Exploiting Automated Reasoning Proof Certificates

  2023cites this paper
• Z3-Noodler: An Automata-based String Solver (Technical Report)

  2023cites this paper
• Solving String Constraints with Lengths by Stabilization

  2023influential citation
• Fixing Privilege Escalations in Cloud Access Control with MaxSAT and Graph Neural Networks

  2023cites this paper
• Ambit: Verification of Azure RBAC

  2023influential citation
• cvc5: A Versatile and Industrial-Strength SMT Solver

  2022cites this paper
• Verifiable Access Control for Augmented Reality Localization and Mapping

  2022cites this paper
• Quantifying Permissiveness of Access Control Policies

  2022influential citation
• Actions over Core-closed Knowledge Bases

  2022cites this paper
• Finding and Understanding Incompleteness Bugs in SMT Solvers

  2022cites this paper
• Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language

  2022cites this paper
• P-Verifier: Understanding and Mitigating Security Risks in Cloud-based IoT Access Policies

  2022influential citation
• The Runtime model checking Method for Zero Trust Security Policy

  2022cites this paper
• Verifying Zookeeper based on Model-Based runtime Trace-Checking using TLA+

  2022cites this paper
• Detecting conflict of heterogeneous access control policies

  2022cites this paper
• Qubit Mapping and Routing via MaxSAT

  2022influential citation
• A Billion SMT Queries a Day (Invited Paper)

  2022influential citation
• Flexible Proof Production in an Industrial-Strength SMT Solver

  2022cites this paper
• Even Faster Conflicts and Lazier Reductions for String Solvers

  2022cites this paper
• Quacky: Quantitative Access Control Permissiveness Analyzer✱

  2022cites this paper
• Applying cognitive principles to model-finding output: the positive value of negative information

  2022cites this paper
• Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning (Extended Abstract)

  2021cites this paper
• Code‐level model checking in the software development workflow at Amazon Web Services

  2021cites this paper
• MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers

  2021cites this paper
• Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities

  2021cites this paper
• CertiStr: a certified string solver

  2021cites this paper
• Assessing the Effectiveness of the Shared Responsibility Model for Cloud Databases: the Case of Google’s Firebase

  2021cites this paper
• Slang: The Sireum Programming Language

  2021cites this paper
• MedleySolver: Online SMT Algorithm Selection

  2021cites this paper
• One-click formal methods

  2020cites this paper
• Specifying and verifying usage control models and policies in TLA+\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$^+$$

  2020influential citation
• MOILab: towards a labelled theorem prover for intuitionistic modal logics

  2020cites this paper
• Symbolic Boolean derivatives for efficiently solving extended regular expression constraints

  2020cites this paper
• Rule-based Word Equation Solving

  2020cites this paper
• Stratified Abstraction of Access Control Policies

  2020influential citation
• A Decision Procedure for String to Code Point Conversion

  2020cites this paper
• Scalable Optimal Deployment in the Cloud of Component-based Applications using Optimization Modulo Theory, Mathematical Programming and Symmetry Breaking

  2020cites this paper
• Monadic Decomposition in Integer Linear Arithmetic

  2020cites this paper
• Soteria: A Provably Compliant User Right Manager Using a Novel Two-Layer Blockchain Technology

  2020cites this paper
• Formal Methods and Computing Identity-based Mentorship for Early Stage Researchers

  2020cites this paper
• Reductions for Strings and Regular Expressions Revisited

  2020cites this paper
• A domain-specific language for filtering in application-level gateways

  2020cites this paper
• Block public access: trust safety verification of access control policies

  2020influential citation
• Combining Learning and Model-Based Reasoning to Reduce Uncertainties in Cloud Security and Compliance Auditing

  2019influential citation
• Towards Multiverse Databases

  2019cites this paper