An eager sat-based solver for a quantifier-free theory of strings and bit vectors

A computer-implemented method comprising:

• obtaining, by a solver used by an automated reasoning service of a cloud provider network, a formula including one or more string variables, wherein the formula relates to a question about a desired condition of a policy managed by an identity and access management service of a cloud provider network;
• determining, for at least one string variable of the one or more string variables, a respective length value indicating a bounded length of possible assignments to the string variable;
• generating a propositional encoding of the formula with respect to the respective length value for at least one string variable of the one or more string variables;
• invoking a SAT solver on the propositional encoding of the formula to obtain a results value indicating whether the formula, with respect to the respective length value for the at least one string variable of the one or more string variables, is satisfiable or unsatisfiable;
• and
• providing the results value to another component of the automated reasoning service.

A system comprising:

• a first one or more electronic devices to implement an automated reasoning service in a multi-tenant provider network, wherein the automated reasoning service includes instructions that upon execution cause the automated reasoning service to:
• generate a first-order logic formula, wherein the first-order logic formula is generated based on a policy managed by an identity and access management service of a cloud provider network and a rule, wherein the rule expresses a desired condition of the policy, and wherein the first-order logic formula includes one or more string variables;
• and
• a second one or more electronic devices to implement an automated reasoning solver in the multi-tenant provider network, wherein the automated reasoning solver includes instructions that upon execution cause the automated reasoning service to:
• generate a Boolean abstraction of the first-order logic formula, wherein the Boolean abstraction of the first-order logic formula includes one or more Boolean variables each representing an atomic formula of the first-order logic formula;
• determine, for each string variable of the one or more string variables, a respective length value indicating a bounded length of possible string assignments to the string variable;
• generate a propositional encoding of each atomic formula within the first-order logic formula based on the respective length value for each string variable;
• invoke a SAT solver on the Boolean abstraction of the first-order logic formula and the propositional encoding of each atomic formula in the first-order logic formula to obtain a result value indicating whether the first-order logic formula, with respect to the respective length value for each string variable, is satisfiable or unsatisfiable;
• determine, based on the result value, whether the policy conforms to the desired condition of the policy expressed by the rule;
• and
• cause display of information indicating whether the policy conforms to the desired condition of the policy expressed by the rule.