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

Claim 16:
17. A system comprising:
a first one or more electronic devices to implement a policy analysis service component in a multi-tenant provider network, wherein the policy analysis service component includes instructions that upon execution cause the policy analysis service component to:
receive 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 multi-tenant provider network,
identify a set of predicates in the formula based on a type of theory associated with 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,
partition a search space associated with the formula into a plurality of sub-formulas, wherein each sub-formula of the plurality of sub-formula includes the formula under an assumption that a respective predicate of the set of predicates is either true or false,
send, 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,
receive, 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, and
transmit a message indicating that the formula is satisfiable, wherein satisfiability of the formula determines a property of a policy defining permissions applicable to a computing resource associated with a cloud provider network;

a second one or more electronic devices to implement the SMT solver in the multi-tenant provider network, the SMT solver including instructions that upon execution cause the SMT solver to:
receive the respective sub-formula of the plurality of sub-formulas,
determine whether the sub-formula is satisfiable, and
send the indication that the respective sub-formula is satisfiable; and

a third one or more electronic devices to implement an identify and access management (IAM) service component in the multi-tenant provider network, the IAM service component including instructions that upon execution cause the IAM service component to:
control access to the computing resource according to the policy defining permissions applicable to the computing resource associated with the cloud provider network.