US 12,425,455 B2
Authorization policy analysis
Emina Torlak, Seattle, WA (US); Kyle Headley, Arlington, VA (US); Michael W. Hicks, Silver Spring, MD (US); Neha Rungta, San Jose, CA (US); and Andrew Marshall Wells, Cupertino, CA (US)
Assigned to Amazon Technologies, Inc., Seattle, WA (US)
Filed by Amazon Technologies, Inc., Seattle, WA (US)
Filed on Nov. 28, 2022, as Appl. No. 18/070,371.
Prior Publication US 2024/0179188 A1, May 30, 2024
Int. Cl. H04L 29/06 (2006.01); H04L 9/40 (2022.01)
CPC H04L 63/205 (2013.01) [H04L 63/104 (2013.01)] 20 Claims
OG exemplary drawing
 
1. A method performed by one or more electronic devices in a provider network, the method comprising:
encoding a set of terms from an authorization policy based on validating the authorization policy as strictly typed based on an authorization policy schema to yield an encoding of the authorization policy, wherein the authorization policy comprises:
(a) an effect;
(b) an authorization policy head that selects principals, actions, or resources to which the authorization policy applies;
(c) one or more conditional clauses that further refine circumstances under which the authorization policy applies; and
(d) at least one expression in terms of one or more entities in an entity hierarchy represented as a directed acyclic graph;
inputting a Satisfiability Modulo Theories (SMT) formula to an SMT solver, the SMT formula translated from the encoding of the authorization policy and from concrete constraints on a form of the entity hierarchy;
receiving an output from the SMT solver indicating whether the SMT formula is satisfiable or unsatisfiable;
determining, based on the output from the SMT solver indicating whether the SMT formula is satisfiable or unsatisfiable, an answer to a first-order question about a behavior of the authorization policy; and
causing display of information indicating the answer.