Patent ID: 11861409
Assignee: AMAZON TECHNOLOGIES, INC.
Field: Computer technology (Electrical engineering)
Classification: CPC G | IPC G

Claim 0:
1. A computer-implemented method comprising:
receiving, by a policy analysis service of a cloud provider network, a request to determine whether a formula is satisfiable, wherein the formula relates to an analysis of one or more policies applicable to one or more computing resources associated with a user of the cloud provider network;
identifying a set of predicates in the formula based on string variables included in the formula, wherein each predicate of the set of predicates is a binary-valued function of at least one string variable contained in the formula;
partitioning a search space associated with the formula into a plurality of sub-formulas, wherein each sub-formula of the plurality of sub-formulas includes the formula under an assumption that a respective predicate of the set of predicates is either true or false;
sending, to a satisfiability modulo theories (SMT) solver running on each of a plurality of computing resources, a respective sub-formula of the plurality of sub-formulas;
receiving, from the SMT solver running on a computing resource of the plurality of computing resources, an indication that the respective sub-formula analyzed by the SMT solver running on the computing resource is satisfiable;
causing display of information indicating that the formula is satisfiable, wherein satisfiability of the formula determines a property of the one or more policies defining permissions applicable to the one or more computing resources associated with the user of the cloud provider network; and
controlling access to the one or more computing resources according to the one or more policies defining permissions applicable to the one or more computing resources associated with the user of the cloud provider network.