Verifying access-control policies with arithmetic quantifier-free form constraints

Abstract

A system and method is provided for verifying an access-control policy against a particular constraint for a multi-step operation. In disclosed embodiments, the method includes expressing the access-control policy as a first quantifier-free form (QFF) constraint and identifying the particular constraint as a second QFF constraint. The method also includes identifying an operation vector and providing copies of the operation vector associated with steps in the multi-step operation. The method also includes determining a third QFF constraint using the first QFF constraint, the second QFF constraint, and the copies of the operation vector. The method also includes solving the third QFF constraint to determine a solution and outputting a result of the solving.

Claims

1. A method comprising: expressing an access-control policy as a first quantifier-free form (QFF) constraint; identifying a particular constraint for a multi-step operation as a second QFF constraint, the multi-step operation comprising a sequence of operational steps; identifying an operation vector defining an incoming IP packet comprising a destination address; providing a respective copy of the operation vector defining the incoming IP packet comprising the destination address associated with each respective step in the sequence of operational steps in the multi-step operation; determining a third QFF constraint using the first QFF constraint, the second QFF constraint, and the copies of the operation vector defining the incoming IP packet comprising the destination address; solving the third QFF constraint to determine a solution, wherein the solving indicates an extent to which permitting or prohibiting the multi-step operation by the access control policy is consistent with permitting or prohibiting the multi-step operation by the particular constraint, wherein the operational steps of the multi-step operation comprise different access operations at different security levels, and wherein in each step a security level of a target object against which a subject operation is to be performed by a subject object is to be less than two levels greater than a security level of the subject object; and outputting the solution.

2. The method of claim 1, wherein the solution comprises at least one of: an empty set, indicating that the access-control policy does not permit the multi-step operation; or operation vector values enumerating particular multi-step operations described by the second QFF constraint and permitted by the access-control policy.

3. The method of claim 1, wherein the third QFF constraint comprises a combination of: multiple instances of the first QFF constraint each separately applied to different copies of the operation vector; and the second QFF constraint applied to the copies of the operation vector.

4. The method of claim 1, wherein expressing the access-control policy further comprises parsing the access-control policy to express the access-control policy as the first QFF constraint.

5. The method of claim 1, wherein: the operation vector comprises a plurality of fields; each of the copies of the operation vector include a different set of variables for the fields; and each of the copies of the operation vector represent an operation step in the multi-step operation.

6. A non-transitory computer-readable medium storing program instructions for execution to perform: expressing an access-control policy as a first quantifier-free form (QFF) constraint; identifying a particular constraint for a multi-step operation as a second QFF constraint, the multi-step operation comprising a sequence of operational steps; identifying an operation vector defining an incoming IP packet comprising a destination address; providing a respective copy of the operation vector defining the incoming IP packet comprising the destination address associated with each respective step in the sequence of operational steps in the multi-step operation; determining a third QFF constraint using the first QFF constraint, the second QFF constraint, and the copies of the operation vector defining the incoming IP packet comprising the destination address; solving the third QFF constraint to determine a solution, wherein the solving indicates an extent to which permitting or prohibiting the multi-step operation by the access control policy is consistent with permitting or prohibiting the multi-step operation by the particular constraint, wherein the operational steps of the multi-step operation comprise different access operations at different security levels, and wherein in each step a security level of a target object against which a subject operation is to be performed by a subject object is to be less than two levels greater than a security level of the subject object; and outputting the solution.

7. The non-transitory computer-readable medium of claim 6, wherein the solution comprises at least one of: an empty set, indicating that the access-control policy does not permit the multi-step operation; or operation vector values enumerating particular multi-step operations described by the second QFF constraint and permitted by the access-control policy.

8. The non-transitory computer-readable medium of claim 6, wherein the third QFF constraint comprises a combination of: multiple instances of the first QFF constraint each separately applied to different copies of the operation vector; and the second QFF constraint applied to the copies of the operation vector.

9. The non-transitory computer-readable medium of claim 6, wherein expressing the access-control policy further comprises parsing the access-control policy to express the access-control policy as the first QFF constraint.

10. The non-transitory computer-readable medium of claim 6, wherein: the operation vector comprises a plurality of fields; each of the copies of the operation vector include a different set of variables for the fields; and each of the copies of the operation vector represent an operation step in the multi-step operation.

11. A system comprising: a processor; and a memory device communicably coupled to the processor, the memory storing: a constraint generating configured to express an access-control policy as a first quantifier-free form (QFF) constraint, and identify a particular constraint for a multi-step operation as a second QFF constraint, the multi-step operation comprising a sequence of operational steps; an operation vector providing unit configured to identify an operation vector defining an incoming IP packet comprising a destination address, and provide a respective copy of the operation vector defining the incoming IP packet comprising the destination address associated with each respective step in the sequence of operational steps in the multi-step operation; wherein the constraint generating unit is further configured to determine a third QFF constraint using the first QFF constraint, the second QFF constraint, and the copies of the operation vector defining the incoming IP packet comprising the destination address; and a constraint solving unit configured to solve the third QFF constraint to determine a solution, and output the solution, the solving indicating an extent to which permitting or prohibiting the multi-step operation by the access control policy is consistent with permitting or prohibiting the multi-step operation by the particular constraint, wherein the operational steps of the multi-step operation comprise different access operations at different security levels, and wherein in each step a security level of a target object against which a subject operation is to be performed by a subject object is to be less than two levels greater than a security level of the subject object.

12. The system of claim 11, wherein the solution comprises at least one of: an empty set, indicating that the access-control policy does not permit the multi-step operation; or operation vector values enumerating particular multi-step operations described by the QFF constraint and permitted by the access-control policy.

13. The system of claim 11, wherein the third QFF constraint comprises a combination of: multiple instances of the first QFF constraint each separately applied to different copies of the operation vector; and the second QFF constraint applied to the copies of the operation vector.

14. The system of claim 11, wherein the constraint generating unit is further configured to parse the access-control policy to express the access-control policy as the first QFF constraint.

15. The system of claim 11, wherein: the operation vector comprises a plurality of fields; each of the copies of the operation vector include a different set of variables for the fields; and each of the copies of the operation vector represent an operation step in the multi-step operation.

16. A method comprising: receiving an access-control policy in a policy language; parsing the access-control policy to express the access-control policy in a first quantifier-free form (QFF) constraint, wherein the first QFF constraint operates on fields of an operation vector defining a multi-step operation, the multi-step operation comprising a sequence of operational steps; identifying a second QFF constraint describing a particular constraint for the multi-step operation, the second QFF constraint operating on fields of copies of the operation vector, each copy provided for, and representing, a respective operation step of the sequence of operational steps of the multi-step operation; solving the first QFF constraint with the second QFF constraint to determine an extent to which permitting or prohibiting the multi-step operation by the access control policy is consistent with permitting or prohibiting the multi-step operation by the particular constraint, wherein the operational steps of the multi-step operation comprise different access operations at different security levels, and wherein in each step a security level of a target object against which a subject operation is to be performed by a subject object is to be less than two levels greater than a security level of the subject object; and outputting the solution.

17. The method of claim 16, wherein the operation vector describes a type of operation, the type of operation comprising at least one of: a write to an object in an operating system, a read from an object in an operating system, or a network data packet.

Description

BRIEF DESCRIPTION OF THE DRAWINGS

(1) The accompanying drawings, which are incorporated in and constitute a part of this specification, illustrate various embodiments. In the drawings:

(2) FIG. 1 illustrates an operating system environment 100 implementing a MLS access-control policy among objects.

(3) FIG. 2 illustrates a Venn diagram space of constraints, which may be compared by prior art solutions.

(4) FIG. 3 illustrates an operating system environment implementing a MLS access-control policy among objects, and illustrating a multi-step operation.

(5) FIG. 4 illustrates a computer system for verifying access-control policies.

(6) FIG. 5 illustrates a memory, which includes components that may be used for verifying access-control policies.

(7) FIG. 6 illustrates a method of verifying an access-control policy against a particular constraint.

(8) FIG. 7 illustrates a method of verifying an access-control policy against a particular constraint for a multi-step operation.

(9) FIG. 8 illustrates a Venn diagram space illustrating the solving of the third QFF constraints and outputted results.

DESCRIPTION OF THE EMBODIMENTS

(10) In the following description, for purposes of explanation and not limitation, specific techniques and embodiments are set forth, such as particular sequences of steps, interfaces, and configurations, in order to provide a thorough understanding of the techniques presented here. While the techniques and embodiments will primarily be described in the context of the accompanying drawings, those skilled in the art will further appreciate that the techniques and embodiments can also be practiced in other electronic devices or systems.

(11) Reference will now be made in detail to exemplary embodiments of the present invention, examples of which are illustrated in the accompanying drawings. Whenever possible, the same reference numbers will be used throughout the drawings to refer to the same or like parts.

(12) As discussed, the prior art solutions to access-control policy verification determine, by different methods, the extent to which one constraint (e.g., access-control policy) subsumes another constraint. But the problem of verifying an access-control policy may be more difficult when multiple steps are involved.

(13) FIG. 3 illustrates an operating system environment 300 implementing a MLS access-control policy among objects, and illustrating a multi-step operation. Environment 300 may enforce similar access-control policy rules as environment 100 from FIG. 1. In particular, environment 300 may implement Equation 3, which states that in order for a subject object to write to or read from a target object, the security level of the target object must be less than two levels greater than the subject object's security level.

(14) Items 302-310 from FIG. 3 are similar to items 102-110 in FIG. 1. Environment 300 further includes operation 312, which is an attempt by Object0 308 to directly read from Object2 310. Operation 312 may be similar to operation 116 from FIG. 1. Specifically, operation 312 may be defined by the operation vector shown in Equation 4. Accordingly, operation 312 is prevented by environment 300, in accordance with the access-control policy rule in Equation 3.

(15) Environment 300 also includes Object1 314 at Security Level 1. Object1 314 may be used to implement operation 312 as a multi-step operation. In particular, operation 312 may be divided into operation 316 and 318, both of which are allowed by the access-control policy rule represented in Equation 3.

(16) In operation 316, Object1 314 reads from Object2 310. The operation vector for this may be:
[Object1,1,Object2,2,read]  Equation 5

(17) The operation vector in Equation 5 describes an operation in which a subject Object1 314 with a security level 1 seeks to read from a target Object2 310 with a security level of 2. Environment 300 may apply the access-control policy rule of Equation 3 to the operation vector of Equation 5. By doing so, environment 300 may determine that operation 316 is permitted because the target object (Object2) is less than two security levels greater than the subject object (Object1). Indeed, the difference in security levels between Object1 and Object2 is only one, which is less than two. After operation 316, Object1 314 has data from Object2 310.

(18) Next, in operation 318, Object0 308 reads from Object1 314. The operation vector for this may be:
[Object0,0,Object1,1,read]  Equation 6

(19) The operation vector in Equation 6 describes an operation in which a subject Object0 308 with a security level 0 seeks to read from a target Object1 314 with a security level of 1. An operating system may apply the access-control policy rule of Equation 3 to the operation vector of Equation 6. By doing so, the operating system would determine that operation 318 is permitted because the target object (Object1) is less than two security levels greater than the subject object (Object0). Indeed, the difference in security levels between Object0 and Object1 is only one, which is less than two.

(20) Accordingly, in operation 318, Object0 308 reads data from Object1 314, which previously read the same data from Object2 310. Thus, the access-control policy permits the combination of operations 316 and 318 and denies operation 312, even though they are both effectively the same operation. In this way, FIG. 3 shows an example of a multi-step operation (operations 316 and 318) permitted by an access-control policy in Equation 3, and yet violating the constraint that an subject cannot read from a target whose security level is two or more levels above the subject.

(21) Thus, when evaluating constraints against an access-control policy, it may be necessary to determine if an access-control policy will properly deny an operation prevented by a constraint, but will improperly allow a series of operations that, while individually do not violate the constraint, do so collectively.

(22) FIG. 4 illustrates a computer system 400 for verifying access-control policies. In some embodiments, computer system 400 may identify multi-step operations that violate a constraint, but are permitted by an access-control policy.

(23) Although a specific number of components are depicted in FIG. 4, any number of these components may be provided. Furthermore, the functions provided by one or more components of system 400 may be combined or separated. And the functionality of any one or more components of system 400 may be implemented by any appropriate computing environment.

(24) System 400 may include a computing device 402. Device 402 may perform computing tasks, such as verifying access-control policies or enforcing access-control policies. Device 402 may be a desktop computer, laptop computer, a firewall, client, server, handheld, or mobile device. Device 402 may include a central processing unit (CPU) 404, a memory 406, a user interface 408, and/or an I/O unit 410.

(25) CPU 404 may execute computer program instructions to perform various processes and methods. CPU 404 may include a single processor or multiple processors. The multiple processors may execute in a single location or across multiple locations. CPU 404 may read the computer program instructions from memory 406 or from any computer-readable storage medium included in device 402, external to device 402, or accessible to device 402, for example, over a network. Memory 406 may include random access memory (RAM) and/or read only memory (ROM) configured to access and store information, such as access-control policies and other constraints, and computer program instructions. Memory 406 may also include additional memory to store data and computer program instructions, and/or one or more internal databases (not shown) to store tables, lists, or other data structures. Memory 406 may include a single memory device or multiple memory devices. The multiple memory devices may occur in a single location or may be distributed across multiple locations.

(26) User interface 408 may access user data, such as a user input for verifying access-control policies. In some embodiments, user interface 408 may be separate from device 402. User interface 408 may also include a visual display, keyboard, mouse, or touch screen, for example. I/O unit 410 may access data over a network or local drive. In addition, device 402 may access legacy systems (not shown) via a network, or may directly access legacy systems, databases, or other network applications.

(27) FIG. 5 illustrates a memory 406, which includes components that may be used for verifying access-control policies. The components in memory 406 may be logical portions or aspects of computer programs or computer program instructions stored in memory 406. These components may be implemented in hardware, software, or firmware, or a combination thereof.

(28) Memory 406 may include Constraint Generating Unit 502, Operation Vector Providing Unit 504, and Constraint Solving Unit 506.

(29) Constraint Generating Unit 502 may receive two or more constraints to compare with each other. For example, Constraint Generating Unit 502 may receive an access-control policy and a particular constraint. A user or process may need to determine the extent to which operations prohibited by the particular constraint are also prohibited by the access-control policy, for example. In another example, the user or process may need to determine the extent to which operations permitted by the constraint are also permitted by the access-control policy.

(30) The access-control policy and constraint may be expressed in some language or format. For example, one or more of the access-control policy or constraint may be expressed in accordance with an IPSec policy or SELinux policy, as understood by one of ordinary skill in the art.

(31) Constraint Generating Unit 502 may parse the access-control policy and/or the constraint to express one or more of them in an arithmetic quantifier-free form (QFF). The use of QFF in modeling access-control policies may be an advancement over the prior art. The QFF language may be a Boolean combination of simple/primitive arithmetic constraints. For example, a QFF expression may be in the form of:
X op Y  Equation 7
where X and Y are integer variables or constants (not just Boolean TRUE/FALSE constructs), and “op” is one or more of the following constraints: =, <, >, <=, >=, etc. Expressions of the type in Equation 7 may be joined with similar expressions using logical operators, such as AND, OR, etc.

(32) A QFF expression may also be in the form of:
contained(a,m,b,n)  Equation 8
which is true when the address range represented by (a, n) contains the address range represented by (b, n), where a, m, b, and n are integer variables or constants. The expression in Equation 8 may be useful in firewalls or other network systems.

(33) In this way, the QFF language is more expressive than simple Boolean logic, and expresses high level concepts easily. The QFF language is also more scalable than Boolean logic. The QFF language is also less verbose than XACML. As a result, QFF is easier to use than either prior art solution of using Boolean logic or XACML. Moreover, as will be described, QFF permits verification of an access-control policy to take into account multi-step operations.

(34) The QFF expressions of the access-control policy and constraint may be applied to fields of an operation vector. Operation Vector Providing Unit 504 may provide a generic operation vector with a predefined number of fields, and variables in the fields. For example, Operation Vector Providing Unit 504 may provide the operation vector of the form:
[a,b,c,d,e]  Equation 9
A set of values for the variables a-e may define a specific operation, for example, an operating system read/write, or a network packet passing through a firewall. But the generic operating vector in Equation 9 only describes a type of operation, and not a specific operation. For example, Equation 9 may express an operation vector format for describing an operating system read/write.

(35) In some embodiments, Operation Vector Providing Unit 504 may provide multiple copies of a generic operation vector. Each of the copies may represent a step in a multi-step operation. For example, Operation Vector Providing Unit 504 may provide the following copies of a generic operation vector, with different variable identifiers:
[a1,b1,c1,d1,e1]  Equation 10
[a2,b2,c2,d2,e2]  Equation 11
[a3,b3,c3,d3,e3]  Equation 12
Each of Equations 10-12 is a copy of the generic operation vector in Equation 9, and may represent a step in a multi-step operation.

(36) Constraint Solving Unit 506 may solve the access-control policy expressed in QFF with the particular constraint expressed in QFF, both generated by Constraint Generating Unit 502, as applied to the operation vector (Equation 9) or copies of the operation vector (Equations 10-12) as provided by Operation Vector Providing Unit 504. Constraint Solving Unit 506 may be Kodkod, or some other constraint solver or SAT solver known in the art. In some embodiments, Constraint Solving Unit 506 may output an indication of the extent to which the access-control policy subsumes the constraint. In some embodiments, Constraint Solving Unit 506 may take into account multi-step operations by using copies of the operation vector (Equations 10-12).

(37) FIG. 6 illustrates a method 600 of verifying an access-control policy against a particular constraint. Method 600 may be executed by CPU 404 from FIG. 4 by program instructions or other components stored in Memory 406, such as Constraint Generating Unit 502, Operating Vector Providing Unit 504, and/or Constraint Solving Unit 506.

(38) At block 602, Constraint Generating Unit 502 may receive an access-control policy in a policy language. The policy language may be, for example, a statement expressed in accordance with an IPSec policy or SELinux policy, as understood by one of ordinary skill in the art.

(39) At block 604, Constraint Generating Unit 504 may parse the access-control policy and convert the access-control policy from the policy language to a first QFF constraint. Accordingly, at block 606, Constraint Generating Unit 504 may express the access-control policy as the first QFF constraint. The first QFF constraint may operate on fields of a generic operation vector. The generic operation vector may be provided by Operating Vector Providing Unit 504. The generic operation vector may be similar to Equation 9, as discussed above. But the specific format of Equation 9 is exemplary only, and any number or type of fields or variables may be used alternatively.

(40) The generic operation vector provided by Operating Vector Providing Unit 504 may generically describe a type of operation, such as a write to an object in an operating system, a read from an object in an operating system, and a network data packet. The operation vector may describe other types of operations as well, and these operation types are exemplary only.

(41) At block 608, Constraint Generating Unit 504 may identify a second QFF constraint. The second QFF constraint may be a particular constraint compared with the first QFF constraint of the access-control policy, to determine the extent to which the first QFF constraint subsumes the second QFF constraint. The second QFF constraint may also operate on the fields of the same operation vector provided by Operating Vector Providing Unit 504.

(42) At block 610, Constraint Solving Unit 506 may solve the first QFF constraint with the second QFF constraint to determine the extent to which the first QFF constraint subsumes the second QFF constraint. At block 612 Constraint Solving Unit 506 may output a result of the solving. For example, Constraint Solving Unit 506 may store the result in memory, such Memory 406 or output the result to a user via User Interface 408.

(43) For example, should the first QFF constraint of the access-control policy completely subsume the second QFF constraint (such as set 202 subsuming set 204 in FIG. 2), then Constraint Solving Unit 506 may output the empty set at block 612 as the result of the solving. This may be because there are no operations prevented by the second QFF constraint that are not also prevented by the first QFF constraint, in this example. Alternatively, should the first QFF constraint of the access-control policy not subsume the second QFF constraint (such as set 202 not completely subsuming set 206 in FIG. 2), then Constraint Solving Unit 506 may output a set of values for the generic operation vector at block 612 as the result of the solving. The set of values for the generic operation vector may define a specific operation prevented by the second QFF constraint but permitted by the first QFF constraint.

(44) FIG. 7 illustrates a method 700 of verifying an access-control policy against a particular constraint for a multi-step operation. Method 700 may be executed by CPU 404 from FIG. 4 by program instructions or other components stored in Memory 406, such as Constraint Generating Unit 502, Operating Vector Providing Unit 504, and/or Constraint Solving Unit 506.

(45) At block 702 Constraint Generating Unit 502 may express the access-control policy as a first quantifier-free form (QFF) constraint. In some embodiments, Constraint Generating Unit 502 may receive the access-control policy in a policy language and parse the policy language to express the access-control policy as the first QFF constraint.

(46) The first QFF constraint may be represented by the following function:
Legal(OpVec)  Equation 13
Thus, Legal is a QFF constraint on fields of an operation vector OpVec, which may be a generic operation vector similar to Equation 9. Accordingly, when Legal is true for any combination of values in OpVec, the access-control policy may permit the associated operation. Concrete examples of Equation 13 in QFF may be found in the Appendix. Other examples of QFF may be found in the indices accompanying Applicant's provisional application 61/287,307, the contents of which are fully incorporated by reference.

(47) At block 704, Constraint Generating Unit 502 may identify the particular constraint as a second QFF constraint. In this example, the second QFF constraint may be represented by the following function:
Bad(OpVec_1, . . . ,OpVec_k)  Equation 14
Thus, Bad is a QFF constraint on fields of a number of copies of an operation vector OpVec, such as OpVec_1 . . . , OpVec_k, for a total of k operation vector copies. These operation vectors may be copies of a generic operation vector, and may be similar to those described in Equations 10-12. Moreover, each of these operation vectors may represent an operation step in a multi-step operation. The Bad QFF constraint may operate on all variables in the copies of the operation vectors. For example, if Equations 10-12 represent the operation vector copies, then Bad may operate on variables a1, b1, c1, d1, e1, a2, b2, c2, d2, e2, a3, b3, c3, d3, and e3 of these operation vectors. When the QFF constraint of Bad is true, then some operation is allowed by Bad to occur. In this example, the operation allowed by Bad may be undesirable. Accordingly, method 700 may compare Bad with Legal to determine if “Bad” operations (permitted by Equation 14) are “Legal” (permitted by Equation 13).

(48) In block 706, Operating Vector Providing Unit 504 may identifying an operation vector. For example Operating Vector Providing Unit 504 may identify OpVec from Equation 13, which may be similar to the exemplary generic operation vector in Equation 9. As illustrated in Equation 9, the operation vector may include a plurality of fields (e.g., a-e).

(49) At block 708, Operating Vector Providing Unit 504 may provide copies of the operation vector associated with steps in the multi-step operation. For example Operating Vector Providing Unit 504 may provide OpVec_1, . . . , OpVec_k from Equation 14, which may be similar to the operation vector copies in Equations 10-12. Accordingly, each of the copies of the operation vector may represent an operation step in the multi-step operation. As also illustrated in Equations 10-12, each of the copies of the operation vector may include a different set of variables for the fields (e.g., a1-e1, a2-e2, and a3-e3)

(50) At block 710, Constraint Generating Unit 502 may determine a third QFF constraint using the first QFF constraint, the second QFF constraint, and the copies of the operation vector. In particular, Constraint Generating Unit 502 may instantiate multiple copies of the first QFF constraint, such as Equation 13. Constraint Generating Unit 502 may then apply each of the instantiated first QFF constraints (e.g., multiple copies of Legal) to one of the operational vector copies provided by Operating Vector Providing Unit 504, such as OpVec_1, OpVec_k or Equations 10-12. In this way, the third QFF may include multiple instances of the first QFF constraint each separately applied to different copies of the operation vector. This may be represented as:
Legal(OpVec_1)& . . . & Legal(OpVec_k)  Equation 15
In Equation 15 each instantiated copy of Legal is applied to a different copy of OpVec. These expressions are then logically ANDed together (represented by the “&”). The call to Legal at step i between 1 and k, checks if the i'th operation is permitted.

(51) Constraint Generating Unit 502 may also apply the second QFF constraint to the copies of the operation vector. For example, Constraint Generating Unit 502 may apply Bad from Equation 14 to the copies of OpVec_1, . . . OpVec_k or Equations 10-12. This may be represented as:
Bad(OpVec_1, . . . OpVec_k)  Equation 16
In Equation 16, a single instance of Bad is applied to all copies of OpVec. This is possible because Bad is defined to apply to variables in OpVec_1, . . . OpVec_k, in Equation 14. Legal, by contrast is defined to apply to only a single generic operation vector OpVec, as in Equation 13. Therefore, when evaluating multiple copies of the operation vector OpVec, Legal may instantiate a new copy of itself for each of the operation vector copies (as in Equation 15), while Bad may only be a single instance applied to all the operation vector copies (as in Equation 16). The call to Bad checks that these steps jointly satisfy a bad condition.

(52) As discussed, the third QFF constraint may be determined using the first QFF constraint, the second QFF constraint, and the copies of the operation vector. In some embodiments, the third QFF constraint may be determined by combining Equations 15 and 16. For example, the third QFF constraint may be represented by:
Legal(OpVec_1)& . . . & Legal(OpVec_k)& Bad(OpVec_1, . . . OpVec_k)  Equation 17
Equation 17 is a logical AND operation between Equation 15 and Equation 16, represented by the “&” operator. In this way, the third QFF evaluates the first QFF constraint (relating to the access-control policy) and the second QFF constraint (relating to the particular constraint) for k steps in a multistep operation. Indeed, because each copy of OpVec refers to an operational step in the multi-step operation, Equation 17 evaluates Legal and Bad over multiple, k, steps.

(53) In block 712, Constraint Solving Unit 506 may solve the third QFF constraint to determine a solution. For example, a program like Kodkod, as is known in the art, may solve the expression of Equation 17. In block 714, Constraint Solving Unit 506 may output a result of the solving. For example, Constraint Solving Unit 506 may store the result in memory, such Memory 406 or output the result to a user via User Interface 408. The output may be either the empty set or one or more sets of values for the operation vector, such as OpVec.

(54) FIG. 8 illustrates a Venn diagram space 800 illustrating the solving of the third QFF constraints and outputted results. Space 800 includes set 802 associated with Legal and set 804 associated with Bad 1. The area inside set 802 may represent operations that are permitted by Legal. Accordingly, if Legal is separately true for all operation steps in a multi-step operation, then those steps fall within set 802.

(55) By contrast, the area inside set 804 may represent operations that are permitted by Bad 1. These may be operations that a user or process tries to prevent. Accordingly, if Bad 1 is true for a combination of steps in the multi-step operation, then those combined steps fall within set 804. If set 802 of Legal and set 804 of Bad 1 do not intersect, then there are no Bad 1 operations permitted by Legal. Accordingly, in this scenario, Constraint Solving Unit 506 may output the empty set, an error message, or any other appropriate indication. As shown in FIG. 8, there is no area of Venn diagram space 800 in which set 802 and set 804 intersect.

(56) Venn diagram space 800 also includes set 806, associated with Bad 2. The area inside set 806 may represent operations that are permitted by Bad 2. Accordingly, if Bad 2 is true for a combination of steps in the multi-step operation, then those combined steps fall within set 806. If set 802 of Legal and set 806 of Bad 2 do intersect, then there are some Bad 2 operations permitted by Legal. Accordingly, in this scenario, Constraint Solving. Unit 506 may output one or more sets of values for the operation vector (e.g., OpVec). These sets of values each define “Bad” operations identified by Bad 2 and permitted by Legal. As shown in Venn diagram space 800, set 802 of Legal and set 806 of Bad 2 intersect at hatched area 808. Accordingly, Constraint Solving Unit 506 may output one or more sets of operation vector values that define operations in hatched area 808.

(57) Venn diagram space 800 from FIG. 8 may be defined in an opposite manner as Venn diagram space 200 from FIG. 2. In particular, the area inside sets in Venn diagram space 200 represent operations prevented by a constraint. By contrast, the area inside sets in Venn diagram space 800 represent operations permitted by a constraint. One of ordinary skill will recognize that either type of Venn diagram may be used in describing disclosed embodiments.

(58) The foregoing description has been presented for purposes of illustration. It is not exhaustive and does not limit the invention to the precise forms or embodiments disclosed. Modifications and adaptations of the invention can be made from consideration of the specification and practice of the disclosed embodiments of the invention. For example, one or more steps of methods described above may be performed in a different order or concurrently and still achieve desirable results.

(59) Other embodiments of the invention will be apparent to those skilled in the art from consideration of the specification and practice of the invention disclosed herein. It is intended that the specification and examples be considered as exemplary only, with a true scope of the invention being indicated by the claims.

APPENDIX

(60) We now show how to use our invention to reason about access control across multiple steps. For example, one may want to check whether it is possible for information to flow from one entity to another via a sequence of intermediate agents. Access control policies only govern a single step so it is not obvious that multi-step flows satisfy intended security goals.

(61) As before, we transform an access control policy into a QFF constraint Legal on a generic operation vector of variables called OpVec. These variables are the fields of an operation that needs to be performed, whether it be a packet's attempt at passing through a firewall, or a process' attempt at writing to a file. When Legal is true for any values of these variables, the associated operation is permitted by the access control policy.

(62) For multi-step reasoning, we instantiate OpVec as many times as there are steps. To verify that it is not possible for there to be k operations that permit a Bad condition to hold, we check that the following constraint is unsolvable:

(63) Legal(OpVec_1) & . . . & Legal(OpVec_k) & Bad(OpVec_1, OpVec_k)

(64) The call to Legal at step i checks that the i'th operation is permitted. Bad checks that the k steps do result in an undesirable condition. If they do, then Constraint Solver will find values of fields in these operations, demonstrating how to cause the bad behavior. If they do not, the Constraint Solver will halt with failure, indicating that no legal sequence of k operations results in bad behavior.

(65) We now illustrate this idea for another class of SELinux policy rules, namely, Conditional Rules. The fact that we can handle this class indicates the broad applicability of our invention. Each SELinux conditional rule is of the form:

(66) Condition, allow, Subject, Target, Class, ListOps

(67) This means Subject is allowed to perform any operation in the set ListOps on Target of type Class, provided Condition holds. Condition is a constraint on a special class of variables called SELinux Booleans. Their values do not change across operations. The operation vector for such rules is, as before, [subject, target, class, operation]. A rule of the above form is transformed into the constraint:

(68) TABLE-US-00001         Condition &       subject=Subject &       target=Target &       class=Class &       (operation=c1 or operation=c2 or ... or operation=ck), each ci a member of ListOps

(69) The definition of Legal is then a disjunction of constraints derived for all the rules.

(70) An example of such a rule is:

(71) TABLE-US-00002 b_vm0_cddvd_mapped & b_vm0_highest_is_topsecret allow, vm0_t, device_t, dir,   [ioctl, write]

(72) The translation of the above rule into a QFF constraint:

(73) TABLE-US-00003 and[ b_vm0_cddvd_mapped   b_vm0_highest_is_topsecret   subject=vm0_t   target=device_t   class=dir   or[ operation=ioctl, operation=write]

(74) Suppose policy P consists of the above rule along with the following:

(75) TABLE-US-00004   b_vm1_cddvd_mapped & b_vm1_highest_is_secret   allow, vm1_t, device_t, dir, [ioctl, read]

(76) Then, the definition of Legal([subject, target, class, operation]) is the QFF:

(77) TABLE-US-00005   or[ and[ b_vm0_cddvd_mapped   b_vm0_highest_is_topsecret   subject=vm0_t   target=device_t   class=dir   or[ operation=ioctl, operation=write]] and[   b_vm2_cddvd_mapped   b_vm2_highest_is_topsecret   subject=vm2_t   target=device_t   class=dir    or[operation=ioctl, operation=read]]]

(78) Suppose, we now want to check if a subject can write to a target in the first step and another subject can read from the same target in the next step. This would imply a two step information flow from the first subject to the next. We would define this condition Bad([subject_1, target_1, class_1, operation_1, subject_2, target_2, class_2, operation_2]) to be the constraint:

(79) TABLE-US-00006 and[ not [subject_1=subject2],   operation_1=write   operation_2=read   class_1=class_2   target_1=target_2]

(80) We would then check whether the constraint

(81) Legal([subject_1, target_1, class_1, operation_1]) &

(82) Legal([subject_2, target_2, class_2, operation_2]) &

(83) Bad([subject_1, target_1, class_1, operation_1, subject_2, target_2, class_2, operation_2])

(84) has a solution. The solution turns out to be:

(85) TABLE-US-00007 subject_2=vm1_t target_2=device_t class_2=dir operation_2=read subject_1=vm0_t target_1=device_t class_1=dir operation_1=write