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

摘要

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.

主权项

1. A method comprising:
verifying, by a processor, the processor comprising hardware, an access-control policy for operating system objects against a particular constraint for a multi-step operation between operating system objects to determine an extent to which handling of the multi-step operation by the access-control policy is consistent with handling of the multi-step operation by the particular constraint, the verifying comprising:
expressing the access-control policy as a first quantifier-free form (QFF) constraint;identifying the particular constraint as a second QFF constraint, the second QFF constraint for comparison to the first QFF constraint to determine the extent to which handling of the multi-step operation by the access-control policy is consistent with handling of the multi-step operation by the particular constraint, wherein the multi-step operation may be broken-down into a sequence of multiple operation steps; identifying an operation vector generically defining the multi-step operation between operating system objects; providing for each operation step of the sequence of multiple operation steps of the multi-step operation, a respective copy of the operation vector, the respective copy representing the operation step of the multi-step operation; determining a third QFF constraint based on the first QFF constraint, the second QFF constraint, and the provided copies of the operation vector; solving the third QFF constraint to determine a solution, the solution indicative of a level of consistency between the access-control policy and the particular constraint in handling the multi-step operation; and outputting the solution.