Security Language Expressions for Logic Resolution

• US 20080066160A1
• Filed: 09/11/2006
• Published: 03/13/2008
• Est. Priority Date: 09/11/2006
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Dillaway, Blair B., Becker, Moritz Y., Gordon, Andrew D., Fournet, Cedric
• Granted Patent: US 8,938,783 B2
• Time in Patent Office: Days
• US Class Current: 726/4
• CPC Class Codes: G06F 21/12 Protecting executable software
• CPC Class Codes: G06F 21/30 Authentication, i.e. establishing the identity or authorisation of security principals
• CPC Class Codes: G06F 21/62 Protecting access to data via a platform, e.g. using keys or access control rules
• CPC Class Codes: G06F 21/6218 to a system of files or objects, e.g. local or distributed file system or database
• CPC Class Codes: G06F 8/315 Object-oriented languages
• CPC Class Codes: G06F 8/316 Aspect-oriented programming techniques
• CPC Class Codes: G06F 8/43 Checking; Contextual analysis

Abstract

A security language expresses assertions and authorization queries in a manner that facilitates logic resolution. In an example implementation, assertion syntax and authorization query syntax are described. In another example implementation, checks on the safety of assertions and authorization queries are described. In yet another example implementation, semantics rules are described.

Claims

1. A system implementing a security scheme including a security language comprising an assertion syntax, an authorization query syntax, and a language semantics;

wherein the assertion syntax includes an asserted fact and enables specification of one or more conditional facts as well as one or more constraints;

wherein the authorization query syntax includes one or more atomic queries that are enabled to be combined by logical connectives; and

wherein the language semantics includes a conditional rule having a delegation flag.

2. The system as recited in claim 1, wherein the assertion syntax indicates that the asserted fact is valid if each of the one or more conditional facts is proved to be valid and if each of the one or more constraints is proved to hold.

3. The system as recited in claim 1, wherein the one or more constraints may include integer equalities and inequalities, tree order constraints, and regular expressions.

4. The system as recited in claim 1 wherein the assertion syntax enables an assertor to issue an assertion having at least an asserted fact;

and wherein the assertor is enabled to delegate all or a portion of a right to another principal.

5. The system as recited in claim 1, wherein the authorization query syntax further enables specification of one or more query constraints, and wherein the logical connectives of the authorization query syntax includes three logical connectives:

“

and”

, “

or”

, and “

not”

.

6. The system as recited in claim 5, wherein the language semantics further includes an authorization query semantics addressing the atomic queries, the one or more query constraints, and the three logical connectives;

and wherein negated queries as well as constraints are required to be ground when being evaluated.

7. The system as recited in claim 1, wherein the language semantics further includes a delegation rule that defines use of a delegation-directive verb or an alias rule that defines use of a verb enabling one principal to act for another.

8. The system as recited in claim 1, wherein the conditional rule defines when the asserted fact is deducible given an assertion context and the delegation flag.

9. The system as recited in claim 8, wherein the delegation flag is propagated to one or more conditional facts.

10. The system as recited in claim 1, wherein the language semantics further includes a delegation rule that defines when one principal can be deduced to state a particular fact based on another principal stating the particular fact given an assertion context and a delegation flag, the delegation flag capable of indicating that no transitive delegation or unbounded transitive delegation is permitted.

11. The system as recited in claim 1, wherein the language semantics further includes an alias rule that defines when an assertor can be deduced to state a first fact about a first principal and a particular verb phrase when given that the assertor has stated a second fact about a second principal and the particular verb phrase.

12. A method comprising:

checking that an assertion of an assertion context is safe;

checking that an authorization query is safe; and

if the assertion context and the authorization query are safe as determined from the checking, evaluating the safe authorization query in conjunction with the safe assertion context.

13. The method as recited in claim 12, wherein the action of checking that an assertion of an assertion context is safe comprises applying at least one assertion-level syntactic check to the assertion;

and wherein the action of checking that an authorization query is safe comprises applying at least one query-level syntactic check to the authorization query.

14. The method as recited in claim 12, wherein the action of checking that an assertion of an assertion context is safe comprises:

verifying that any initial variables of the assertion are safe by verifying that any initial variables are also present in at least one conditional fact of the assertion.

15. The method as recited in claim 12, wherein the action of checking that an assertion of an assertion context is safe comprises:

verifying that any constraint variables of the assertion are additionally otherwise present in the assertion.

16. The method as recited in claim 12, wherein the action of checking that an assertion of an assertion context is safe comprises:

verifying that any conditional facts of the assertion do not involve delegation.

17. The method as recited in claim 12, wherein the action of checking that an authorization query is safe comprises:

confirming that safety of the authorization query can be inferred by a finite number of applications of inference rules selected from a group of authorization query safety inference rules comprising;

a safe assertion inference rule, a safe conjunction inference rule, a safe disjunction inference rule, a safe negation inference rule, and a safe constraint inference rule.

18. A device that implements a security language comprising assertions and authorization queries in which an authorization query may be evaluated on an assertion context including at least one assertion;

wherein the at least one assertion may be checked for safety using one or more syntactic checks.

19. The device as recited in claim 18, wherein the authorization query may be checked for safety using one or more syntactic checks.

20. The device as recited in claim 18, wherein the security language further comprises three semantics rules;

and wherein the three semantics rules comprise a conditional rule addressing assertions with conditional facts, a delegation rule addressing assertions indicating at least part of a right is being delegated; and

an alias rule addressing assertions indicating that one principal may act for another.