Security language translations with logic resolution

• US 9,282,121 B2
• Filed: 02/13/2014
• Issued: 03/08/2016
• Est. Priority Date: 09/11/2006
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Inventors: Becker, Moritz Y., Dillaway, Blair B., Fournet, Cedric, Gordon, Andrew D., Mackay, Jason F.
• Primary Examiner(s): Rahman, Mohammad L
• Application Number:
  US14/180,292
• Publication Number:
  US 20140165139A1
• Time in Patent Office: 754 Days
• US Class Current: 1/1
• CPC Class Codes: G06F 21/36 by graphic or iconic representation
• CPC Class Codes: G06F 21/6236 between heterogeneous systems
• CPC Class Codes: G06F 2221/2141 Access rights, e.g. capability lists, access control lists, access tables, access matrices
• CPC Class Codes: H04L 63/20 for managing network security; network security policies in general filtering policies H04L63/0227

Abstract

Security language constructs may be translated into logic language constructs and vice versa. Logic resolution may be effected using, for example, the logic language constructs. In an example implementation, translation of a security language assertion into at least one logic language rule is described. In another example implementation, translation of a proof graph reflecting a logic language into a proof graph reflecting a security language is described. In yet another example implementation, evaluation of a logic language program using a deterministic algorithm is described.

Claims

1. A method comprising:

translating a fragment of a plurality of fragments of a first proof graph reflecting a logic language into a corresponding fragment of a second proof graph reflecting a security language, wherein each fragment of the plurality of fragments forms part of a structure of the first proof graph and includes at least two nodes and at least one directed edge;

repeating the translating for additional fragments of the plurality of fragments of the first proof graph; and

creating the second proof graph based on the translating.

2. The method as recited in claim 1, further comprising:

translating an assertion context of the security language into a program of the logic language;

evaluating the program of the logic language; and

producing the first proof graph, before translating the fragment of the plurality of fragments, responsive to the evaluating.

3. The method as recited in claim 2, wherein the evaluating comprises:

applying a deterministic algorithm based on tabling that utilizes a first table mapping predicates to sets of ground predicates and a second table mapping predicates to subgoals of the first proof graph.

4. The method as recited in claim 1, wherein the translating comprises:

matching a logic language pattern of the fragment of the plurality of fragments of the first proof graph to a corresponding security language pattern selected from multiple possible security language patterns.

5. The method as recited in claim 4, wherein each respective security language pattern of the multiple possible security language patterns is associated with a respective semantics rule of the security language.

6. The method as recited in claim 4, wherein the multiple possible security language patterns comprise at least three security language patterns, and wherein the three security language patterns comprise a first security language pattern that is associated with a conditional semantics rule, a second security language pattern that is associated with a delegation semantics rule, and a third security language pattern that is associated with an alias semantics rule.

7. The method as recited in claim 1, wherein the fragment of the plurality of fragments of the first proof graph includes one or more nodes of the at least two nodes defines at least one proved assertion and one or more nodes of the at least two nodes defines at least one side condition.

8. A system comprising:

one or more processors;

at least one input/output interface that accepts an assertion context including multiple assertions, each assertion of the multiple assertions including a syntax of a security language, the syntax for each assertion including an asserted fact and permitting one or more conditional facts and one or more constraints; and

memory storing executable instructions that, when executed by the one or more processors, cause the one or more processors to perform acts comprising;

translating the assertion context into a program in a logic language;

evaluating the program in the logic language in conjunction with an authorization query using a deterministic algorithm based on tabling, wherein the deterministic algorithm produces a first proof graph comprising a plurality of fragments, wherein each fragment of the plurality of fragments forms part of a structure of the first proof graph and includes at least two nodes and at least one directed edge; and

translating the first proof graph reflecting the logic language into a second proof graph reflecting the security language.

9. The system as recited in claim 8, wherein the deterministic algorithm utilizes an answer table that maps predicates to sets of ground predicates and a wait table that maps predicates to subgoals of the first proof graph.

10. The system as recited in claim 9, wherein at least one subgoal of the first proof graph comprises a top-level predicate of the first proof graph, a predicate to be solved next, and a list of predicates that are to be solved thereafter.

11. The system as recited in claim 8, wherein translation is effected by matching fragment samples that are associated with respective semantics rules of the security language to corresponding fragments of the first proof graph reflecting the logic language.

12. The system as recited in claim 8, wherein the logic language comprises a form of Datalog.

13. A system comprising:

one or more processors;

memory storing executable instructions that, when executed by the one or more processors, cause the one or more processors to perform acts comprising;

translating a fragment of a plurality of fragments of a first proof graph reflecting a logic language into a corresponding fragment of a second proof graph reflecting a security language, wherein each fragment of the plurality of fragments forms part of a structure of the first proof graph and includes at least two nodes and at least one directed edge;

repeating the translating for additional fragments of the plurality of fragments of the first proof graph; and

creating the second proof graph based on the translating.

14. The system as recited in claim 13, further comprising:

translating an assertion context of the security language into a program of the logic language;

evaluating the program of the logic language; and

producing the first proof graph, before the translating the fragment of the plurality of fragments, responsive to the evaluating.

15. The system as recited in claim 14, wherein the evaluating comprises:

applying a deterministic algorithm based on tabling that utilizes a first table mapping predicates to sets of ground predicates and a second table mapping predicates to subgoals of the first proof graph.

16. The system as recited in claim 13, wherein the translating comprises:

matching a logic language pattern of the fragment of the plurality of fragments of the first proof graph to a corresponding security language pattern selected from multiple possible security language patterns.

17. The system as recited in claim 13, wherein the fragment of the plurality of fragments of the first proof graph includes one or more nodes of the at least two nodes defines at least one proved assertion and one or more nodes of the at least two nodes defines at least one side condition.