Security policy analyzer service and satisfiability engine

Patent metadata

Field	Value
Publication number	US-10757128-B2
Application number	US-201715637227-A
Country	US
Kind code	B2
Filing date	Jun 29, 2017
Priority date	Jun 29, 2017
Publication date	Aug 25, 2020
Grant date	Aug 25, 2020

Abstract

Security policies may be utilized to grant or deny permissions related to the access of computing resources. Two or more security policies may be compared to determine whether the policies are equivalent, whether one security is more permissive than another, and more. In some cases, it may be possible to identify whether there exists a security permission that is sufficient to determine two security policies lack equivalency. Propositional logics may be utilized in the evaluation of security policies.

First claim

What is claimed is:

1. A computer-implemented method, comprising:
obtaining, via an interface, information specifying:
a first security policy encoding a first set of security permissions; and
a second security policy encoding a second set of security permissions, wherein the second set of security permissions encodes a constraint that is applicable when a source virtual computing environment endpoint exists and is inapplicable when the source virtual computing environment endpoint does not exist;

determining a first propositional logic expression based at least in part on the first set of security permissions;
determining a second propositional logic expression based at least in part on the second set of security permissions;
identifying a set of parameters that is sufficient to determine the first propositional logic and the second propositional logic lack equivalency such that applying the first security policy to the set of parameters results in a grant of access to a computing resource associated to the set of parameters and applying the second security policy to the set of parameters results in a denial of access to the computing resource, wherein the first propositional logic expression and the second propositional logic expression are collectively sufficient to identify the set of parameters; and
providing, via the interface, a result indicating that the first security policy grants a particular virtual computing environment endpoint access to a computing resource that the second security policy denies access to.

2. The computer-implemented method of claim 1 , wherein determining the first propositional logic and the second propositional logic lack equivalency comprises utilizing a satisfiability modulo theories (SMT) solver to determine whether constraints generated based at least in part from the first propositional logic and the second propositional logic are satisfiable.

3. The computer-implemented method of claim 2 , wherein the constraints generated based at least in part from the first propositional logic and the second propositional logic are in accordance with a SMT-LIB Standard.

4. The computer-implemented method of claim 1 , wherein the result comprises the set of parameters.

5. A system, comprising:
one or more processors;
memory that stores computer-executable instructions that, as a result of execution, cause the system to:
determine a first propositional logic based at least in part on a first set of security permissions;
determine a second propositional logic based at least in part on a second set of security permissions, wherein the second set of security permissions encodes a constraint that is applicable when a source virtual computing environment endpoint exists and is inapplicable when the source virtual computing environment endpoint does not exist;
identify a set of parameters that is sufficient to determine the first propositional logic and the second propositional logic lack equivalency using the first propositional logic and the second propositional logic, wherein the first propositional logic and the second propositional logic form information that is sufficient to determine that the first propositional logic and the second propositional logic lack equivalency, further wherein applying the first set of security permissions to the set of parameters results in a grant of access to a computing resource associated to the set of parameters and applying the second set of security permissions to the set of parameters results in a denial of access to the computing resource; and
provide an indication that the first set of security permissions and the second set of security permissions lack equivalency as a result of different access being granted to a particular virtual computing environment endpoint.

6. The system of claim 5 , wherein the computer-executable instructions that determine the first propositional logic and the second propositional logic lack equivalency further comprise computer-executable instructions that, as a result of execution, cause the system to utilize a satisfiability modulo theories (SMT) solver to determine whether constraints generated based at least in part from the first propositional logic and the second propositional logic are satisfiable.

7. The system of claim 5 , wherein the first set of security permissions are included in a first policy and the second set of security permissions are included in a second policy.

8. The system of claim 6 , wherein the constraints generated based at least in part from the first propositional logic and the second propositional logic are in accordance with a CVC format or DIMACS format.

9. The system of claim 5 , wherein the computer-executable instructions that identify the set of parameters that is sufficient to determine the propositional logic and the second propositional logic lack equivalency further comprise computer executable instructions that, as a result of execution, cause the system to:
generate a first set of constraints corresponding to access grants of the first set of security permissions; and
generate a second set of constraints corresponding to access denials of the first set of security permissions.

10. The system of claim 9 , wherein the computer-executable instructions that identify the set of parameters that is sufficient to determine the propositional logic and the second propositional logic lack equivalency further comprise computer executable instructions that, as a result of execution, cause the system to generate a third set of constraints corresponding to access neutral constrains of the first set of security permissions.

11. The system of claim 5 , wherein the second set of security permissions is obtained from a user selecting the second set of security permissions from a predetermined plurality of sets of security permissions.

12. The system of claim 5 , wherein the computer-executable instructions that identify the set of parameters that is sufficient to determine that the first propositional logic and the second propositional logic lack equivalency further comprise computer executable instructions that, as a result of execution, cause the system to determine that the first propositional logic and the second propositional logic are incomparable.

13. A non-transitory computer-readable storage medium storing executable instructions that, as a result of being executed by one or more processors of a computer system, cause the computer system to at least:
identify a set of parameters that is sufficient to determine that there exists a security permission associated with either a first set of security permissions or a second set of security permissions that is sufficient to determine a first propositional logic determined from the first set of security permissions and a second propositional logic determined from the second set of security permissions lack equivalency, wherein the first propositional logic and the second propositional logic form information that is sufficient to determine that the first propositional logic and the second propositional logic lack equivalency, wherein the second set of security permissions encodes a constraint that is applicable when a source virtual computing environment endpoint exists and is inapplicable when the source virtual computing environment endpoint does not exist, further wherein applying the first set of security permissions to the set of parameters results in a grant of access to a computing resource associated to the set of parameters and applying the second set of security permissions to the set of parameters results in a denial of access to the computing resource; and
provide an indicatio

Assignees

• Amazon Tech Inc

Inventors

• Cook John
• Rungta Neha
• Dodge Catherine
• Puchalski Jeff
• Varming Carsten

Classifications

• H04L41/0894

  Policy-based network configuration management · CPC title

• H04L63/1433 Primary

  Vulnerability analysis · CPC title

• H04L63/20 Primary

  for managing network security; network security policies in general (filtering policies H04L63/0227) · CPC title

• H04L9/40

  Network security protocols · CPC title

• H04L63/105

  Multiple levels of security · CPC title