JP4887985B2 - Policy inspection system, method, and program - Google Patents

Description

  The present invention relates to a policy checking system, method, and program, and more particularly, to a policy checking system, method, and program for checking a policy description that has a problem in application to a managed system.

  There is a technique for controlling a management target system using a policy (see, for example, Patent Document 1 for a policy-based management system). There is also a policy inspection system for inspecting a policy used in such a technique. The conventional policy inspection system is described in Non-Patent Document 1 and Non-Patent Document 2. FIG. 12 shows the configuration of the policy inspection system described in Non-Patent Document 1. This conventional policy inspection system 900 includes an input device 911, a simultaneous ignition inspection unit 912, a collision inspection unit 913, an output device 914, and a storage device 917. The storage device 917 includes a policy storage unit 915 and a collision rule storage unit 916.

  The input device 911 accepts a policy description to be registered in a policy management system as described in Patent Document 1. The policy description is a description of if-then type rules. Generally, the part that describes the firing condition indicating when the policy is executed and the management target that is executed when the firing condition is satisfied are described. And a part describing the operation. In this conventional policy inspection system 900, in addition to these, a predicate logical expression that represents an action that an operation on the management target gives to the management target in the policy description (hereinafter referred to as a postcondition for convenience). Is included.

  When the input device 911 receives the policy description to be checked, the input device 911 passes the policy to the simultaneous firing checking means 912. The simultaneous firing checking means 912 reads all the policy descriptions already registered in the policy storage unit 915, and symbolically indicates the firing condition of the policy description to be checked passed from the input device 911 among the read policy descriptions. A policy description having the same firing condition, that is, a policy description that can be fired at the same time is searched, and a set thereof is created. When the simultaneous firing inspection unit 912 creates a set of policy descriptions that may be fired at the same time as the policy description to be inspected, it passes the created set of policy descriptions and the policy description to be inspected to the collision inspection unit 913. .

  When the collision inspection unit 913 receives the set of policy descriptions and the policy description to be inspected, the collision inspection unit 913 reads a list of collision rules from the collision rule storage unit 916. A collision rule is a list of predicates. When the collision checking means 913 combines the post-conditions in the policy description set and the policy description to be checked, a predicate that becomes true based on the logical expression of the created post-condition is generated for each of the read collision rules. It is checked whether or not there are two or more in the collision rule. If there are two or more as a result of the investigation, the output device 914 is used to output that there is a possibility that there is a problem in the accepted policy description.

  Next, the policy inspection system described in Non-Patent Document 2 will be described. FIG. 13 shows the configuration of the policy inspection system described in Non-Patent Document 2. The policy inspection system 901 includes an input device 921, an inspection unit 922, a satisfaction determination unit 923, an output device 924, and a storage device 925. The storage device 925 includes a policy storage unit 926. When the input device 921 receives the policy description to be checked, the input device 921 passes the received policy description to the checking unit 922.

  Upon receiving the policy description to be checked, the checking unit 922 reads all the policy descriptions already registered in the policy storage unit 926. The checking means 922 checks whether or not each of the read policy descriptions collides with the policy description to be checked received from the input device 921. For this inspection, the satisfaction determination means 923 is used. First, the checking means 922 checks whether or not the policy firing condition can be satisfied, that is, whether or not the policy description causes simultaneous firing using the satisfaction determining means 923. Thereafter, the satisfaction determination means 923 is used to determine whether the policy description operation can be executed simultaneously for the policy that causes simultaneous firing. The firing condition and the operation method are described by predicate logic, and the satisfaction determination unit 923 determines whether or not the predicate logic can be satisfied. When it is determined that the predicate logic of the operation method cannot be satisfied for the policy descriptions that are fired simultaneously, the checking unit 922 determines that the policy descriptions collide, and causes the output device 924 to output the result.

  For example, let x be the attribute name of a setting file of a computer system. At this time, a policy description in which an operation of x = 10 (set the value of attribute x to 10) is defined and another policy description in which an operation of x = 20 (set the value of attribute x to 20) is defined. Let us consider a case where a collision is determined. The policy checking system 901 determines the logical expression of the ∧ combination of each operation of the given policy description, that is, the satisfiability of x = 10 ｘ x = 20 (the domain of x is an integer). If it is found that there is no combination of variables that cannot be satisfied, that is, satisfies a given logical expression, it is determined that the combination of the given policies does not match (collises).

JP 2002-111729 A Shetan Shiva Shankar, et al., “An ECA-P Policy-based Framework for Managing Ubiquitous Computing Environment (ECA-P Policy-based Framework for Managing Ubiquitous Computing Environments), Mobiquitous 2005 Minutes, USA Dakshi Agrawal, et al. "Policy Ratification", Policy 2005 Minutes, USA

  In Non-Patent Document 1, inconsistency between policy descriptions is detected by giving a post-condition to the policy description and further giving a collision rule indicating a combination of inappropriate post-conditions. In Non-Patent Document 1, there is a problem that it is necessary for humans to give in advance to the policy inspection system by assuming in advance all combinations of inappropriate policy descriptions that can be considered in advance. . Moreover, it is difficult to prepare all inappropriate combinations, and there is a high possibility that a policy description having a problem will be missed due to a lack of collision rules.

  In Non-Patent Document 2, unlike Non-Patent Document 1, it is possible to inspect a collision without a human being giving a collision rule by satisfaction determination. However, Non-Patent Document 2 does not consider the conditions that are satisfied on the management target system. For this reason, policy checks that appropriately reflect the nature of the managed system cannot be performed, and policy conflicts may be missed, and combinations of policy descriptions that should originally collide may be determined not to collide. There's a problem.

  The problems in Non-Patent Document 2 will be described with specific examples. Assume that one policy has a definition of a → b (if a, b), and another policy has a definition of a → ¬b (if a, not b). a and b are primitive logical expressions indicating true / false values such as x> 0 and y = 4. Further, in the collision determination in the satisfaction determination unit 923, it is determined that the policy collides when it cannot be satisfied.

  (A → b) ∧ (a → ¬b), which is a combination of the above two policy definitions, becomes true by assuming ¬a (not a), so it is determined that there is no collision in the policy inspection system. Is done. However, if the actual management target system has the property that “a” always holds, ¬a does not hold, so it must be determined that the previous policy collides. As described above, the conventional policy inspection system described in Non-Patent Document 2 does not consider the conditions that are satisfied in the management target system, and therefore there is a high possibility of missing a policy collision.

  Further, in Non-Patent Document 2, no consideration is given to the equivalence of the object indicated by the bound variable in the logical expression. For this reason, when a policy collision is inspected by the satisfiability determination, the constraint variable that appears in the logical expression does not include a constraint that considers the possibility of pointing to the same management target. There is also the problem that a collision may be missed.

  An object of the present invention is to provide a policy checking system that can check a policy description based on the property of a management target system when checking a problematic policy description by satisfiability determination.

  In addition, the present invention may give restrictions on the equivalence of objects indicated by the bound variables appearing in the logical expression when the problematic policy description is checked by the satisfiability determination after achieving the above-mentioned object. It is an object to provide a policy inspection system, method, and program that can be used.

In order to achieve the above object, the policy inspection system of the present invention comprises:
A policy inspection system for inspecting a policy description to be inspected,
An input device for applying accept the policy description of said object,
An invariant condition storage unit that stores an invariant condition in which a condition that is always satisfied for the state of the managed system is described by first-order predicate logic;
A policy storage unit for storing registered policy descriptions;
A post-condition represented by a predetermined logical expression describing a condition to be satisfied with respect to the state of the managed system immediately after the operation defined in the policy description received by the input device using first-order predicate logic; and Inspection means for inspecting the policy description of the inspection object received by the input device based on the invariant condition stored in the invariant condition storage unit;
The inspection means is
A sufficiency judging means for judging sufficiency of the logical expression;
Refer to the invariant condition stored in the invariant condition storage unit and the registered policy description stored in the policy storage unit, and the post-condition and the registration included in the policy description of the inspection target received by the input device A logical expression generation means for generating a logical expression that is a combination of the postcondition included in the finished policy description and the invariant condition;
Policy consistency checking means for determining the satisfiability of the logical expression generated by the logical expression generation means using the satisfaction determination means;
A key attribute storage unit that stores information on a key attribute that always takes a unique value between the same classes with respect to the class of the managed system among the attributes of the instance that represents the state of the managed system;
Have
Prior to the determination by the policy consistency checking unit, the invariant condition storage unit is referred to, and a logical expression is generated by combining the postcondition included in the policy description to be inspected and the invariant condition. A fraud policy checking means for determining the satisfiability of the logical expression using the satisfaction determination means;
State of the managed system therefore is represented in instance,
The fraud policy inspection means includes:
Prior to sufficiency determination by the satisfaction judgment means, the Key attribute storage unit with reference to, corresponding to the bound variables appearing in formulas to be sufficiency determination of the states instance that expresses the managed system Add an equality constraint as a constraint to the formula, provided that the attached instances are equal,
When the values of the Key attributes of two bound variables appearing in the logical expression subject to the sufficiency determination are equal, the instances corresponding to the two bound variables are equal, and when the two bound variables are equal, Add all Key attribute value is equal to such value constraints you two bound variables in formulas to be the sufficiency determination,
It is characterized by that.

Policy inspection method of the present invention includes an input device for accepting a policy Identifier Description inspected, and invariant condition storage unit always stores the described invariants by first-order logic conditions which satisfies the state of the managed system, registration A policy storage unit for storing a policy description that has already been described, and a condition that should be satisfied for the state of the managed system immediately after the operation defined in the policy description received by the input device is described by first-order predicate logic Based on a postcondition expressed by a predetermined logical expression and the invariant condition stored in the invariant condition storage unit, an inspection unit that inspects the policy description to be inspected received by the input device ; A policy inspection method for inspecting a policy description to be inspected using a computer having
A first-order predicate representing the invariant condition stored in the invariant condition storage unit by the computer and a condition to be satisfied for the state of the managed system immediately after the operation defined in the policy description input by the input device A step of inspecting the policy description to be inspected by an inspection means based on a logical expression described by logic;
The policy description includes a post-condition that describes the condition to be satisfied for the state of the managed system immediately after the operation defined in the policy description by the first-order predicate logic and a pre-condition that describes the policy firing condition by the first-order predicate logic. Including
Checking the policy description comprises the steps of:
The computer refers to the invariant condition storage unit that stores the invariant condition, and generates a logical expression obtained by combining the a posteriori condition included in the policy description to be examined and the invariant condition;
A fraud policy checking step for determining satisfiability of the generated logical expression;
If it is determined that the illegal policy checking step is satisfied, the invariant condition storage unit and the policy storage unit are referred to, the precondition included in the policy description to be inspected, the precondition included in the registered policy description, and the invariant Generating a logical expression that is a combination of conditions;
Determining the satisfiability of the generated logical expression;
If it is determined that the condition is satisfied in the determining step, the invariant condition storage unit and the policy storage unit are referred to, the postcondition included in the policy description to be examined, the postcondition included in the registered policy description, and the invariant condition. Generating a logical expression obtained by combining
A policy consistency check step for determining satisfiability of the generated logical expression; and
Have
Prior to the determination by the policy consistency checking step, the invariant condition storage unit is referred to, and a logical expression is generated by combining the postcondition included in the policy description to be inspected and the invariant condition. A fraud policy checking step for determining satisfiability of the logical expression;
Prior to the sufficiency determination of the logical expression, the illegal policy checking step is a key attribute of the Key attribute that always takes a unique value among the same class among the attributes of the instance expressing the state of the managed system. By referring to the Key attribute storage unit that stores information, an equivalence constraint is added to the logical expression as a restriction on the condition that the instances associated with the bound variables appearing in the logical expression that is the target of the sufficiency determination are equal. Including steps,
In the step of adding the constraint, when the values of the Key attributes of the two bound variables appearing in the logical expression subject to the sufficiency determination are equal, the instances corresponding to the two bound variables are equal, and the 2 one of the added all equivalence constraint shall be the value of the Key attribute is equal of the two bound variables in formulas to be the sufficiency determining when bound variables are equal,
It is characterized by that.

The program of the present invention is a program for causing a computer to execute processing for inspecting a policy description to be inspected,
The computer, an input device to attach accept the policy description of the test object, and invariant condition storage unit always stores the described invariants by first-order logic to establish conditions for the state of the managed system, policy description registered And a predetermined logical expression describing a condition to be satisfied for the state of the managed system immediately after the operation defined in the policy description received by the input device using first-order predicate logic Based on the a posteriori condition represented by the above and the invariant condition stored in the invariant condition storage unit, function as an inspection unit that inspects the policy description of the inspection object received by the input device ,
In the computer,
An invariant condition in which a condition that is always satisfied for the state of the managed system is described by first-order predicate logic, and a condition that should be satisfied for the state of the managed system immediately after the operation defined in the policy description input by the input device Based on a logical expression described by first-order predicate logic, and a program for executing the step of checking the policy description to be checked by the checking means,
The policy description includes a post-condition that describes the condition to be satisfied for the state of the managed system immediately after the operation defined in the policy description by the first-order predicate logic and a pre-condition that describes the policy firing condition by the first-order predicate logic. Including
Checking the policy description comprises the steps of:
An illegal policy that refers to the invariant condition storage unit, generates a logical expression that is a combination of the postcondition included in the policy description to be examined and the invariant condition, and determines whether the generated logical expression is satisfiable An inspection step;
When it is determined that the illegal policy checking step is satisfied, the invariant condition storage unit and the policy storage unit are referred to, the precondition included in the policy description to be checked, the precondition included in the registered policy description, Generate a logical expression that is combined with the invariant condition, determine the satisfiability of the generated logical expression, and determine that the logical expression is satisfied in the determination, refer to the invariant condition storage unit and the policy storage unit, Generate a logical expression that combines the post-conditions included in the policy description to be inspected, the post-conditions included in the registered policy description, and the invariant conditions, and determine the satisfiability of the generated logical expression A policy consistency check step,
The fraud policy checking step includes:
Prior to determining the sufficiency of the logical expression, a key attribute storage unit that stores key attribute information that always takes a unique value among the same class among the attributes of the instance representing the state of the managed system is referred to. Adding an equivalence constraint as a constraint to the logical expression, provided that the instances associated with the bound variable appearing in the logical expression that is the subject of the sufficiency determination are equal ,
In the step of adding the constraint, when the values of the Key attributes of the two bound variables appearing in the logical expression subject to the sufficiency determination are equal, the instances corresponding to the two bound variables are equal, and the 2 one of the added all equivalence constraint shall be the value of the Key attribute is equal of the two bound variables in formulas to be the sufficiency determining when bound variables are equal,
It is characterized by that.

  Hereinafter, embodiments of the present invention will be described in detail with reference to the drawings. FIG. 1 shows the configuration of a policy inspection system according to the first embodiment of the present invention. The policy inspection system 10 includes a first inspection unit 11, a second inspection unit 12, a satisfaction determination unit 13, an input device 14, an output device 15, and a storage device 16. The policy inspection system 10 is configured as a computer system that operates by a program operation. The storage device 16 is a storage device such as a hard disk device, and has already been accepted with an invariant condition storage unit 161 that stores invariant conditions that express the conditions that should always be satisfied with respect to the state of the managed system by a first-order predicate logical expression. A policy storage unit 162 that stores a policy description registered in the policy management system.

  The input device 14 is a computer input device that receives a policy description to be examined. The first checking means (illegal policy checking means) 11 determines whether or not the policy description to be checked has an illegal action on the management target system. The second checking means (policy consistency checking means) 12 determines whether or not the policy description to be checked matches the policy description already registered. The sufficiency determination unit 13 is used when the first inspection unit 11 and the second inspection unit 12 perform an inspection, and determines whether the predicate logical expression is satisfiable. The output device 15 is an external output device such as a display or a file, and is used when the first inspection unit 11 and the second inspection unit 12 output inspection results.

  FIG. 2 shows the structure of the policy description. The policy description 71 includes a policy body and a policy specification. The policy body is a part describing if-then type rules used in the policy management system. The policy specification expresses the behavior of the policy body. FIG. 3 shows the configuration of the policy specification. The policy specification 72 includes a precondition and a postcondition. The precondition expresses the firing condition of the policy body by the first order predicate condition. The post-condition represents a condition that should be satisfied for the state of the management target system immediately after the operation defined in the policy body.

  In the policy description, when the content of the policy body and the content of the policy specification overlap, the information described in the policy body is used as the policy specification, and the policy specification does not need to include the overlapping information. For example, when the firing condition of the policy body is described by predicate logic, the logical expression is treated as a precondition, and the precondition does not have to be included in the policy specification.

  The first checking means 11 receives the policy description to be checked input by the input device 14. Upon receiving the policy description, the first checking unit 11 reads from the invariant condition storage unit 161 an invariant condition that expresses a condition that should always be satisfied for the state of the managed system, and satisfies the policy description and the read invariant condition. The possibility is determined using the satisfaction determination means 13. The first checking unit 11 passes the policy description to be checked to the second checking unit 12 when the sufficiency determining unit 13 determines that the filling is possible. Upon receipt of the policy description, the second checking means 12 reads all the policy descriptions that have already been registered from the policy storage unit 162, and whether each read policy description matches the policy description to be checked. Is determined using the satisfaction determination means 13.

  The satisfaction determination means 13 has a function of determining the satisfaction of the given first-order predicate logical expression. For example, “David Detlefs”, et al., “Simplify: A Theorem Prover for Program Checking”, Journal "Journal of the ACM, USA, Vol. 52, No. 3, May 2005, pages 365-473".

  FIG. 4 shows a schematic procedure of the overall operation of the policy inspection system 10. The policy description to be inspected is received by the input device 14 (step A10). The first checking means 11 receives the policy description to be checked from the input device 14 and checks whether the policy description has an illegal action on the management target system (step A20). If it is confirmed that there is no problem as a result of the inspection by the first inspection unit 11, the second inspection unit 12 determines that the policy description to be inspected is not consistent with other policy descriptions already registered. Whether or not matching occurs is inspected (step A30), and the inspection result is output to the output device 15.

  FIG. 5 shows the operation procedure of the inspection by the first inspection means 11 in step A20 of FIG. When the first checking unit 11 receives the policy description to be checked from the input device 14, the first checking unit 11 reads the invariant condition described in the first order predicate logic from the invariant condition storage unit 161. When the first inspecting unit 11 reads the invariant condition, the first inspecting unit 11 creates a logical expression in which the postcondition (FIG. 3) in the policy specification of the policy description to be inspected and the read invariant condition are combined by the heel (step B10). . After creating the logical expression, the first checking means 11 converts the created logical expression into a form that can be checked by the satisfaction determination means 13 (step B20). For example, in the simplify which is a satisfiability determination tool described in the above-mentioned document, the logical expression needs to be an S expression, and in step B20, the created logical expression is converted into such a format.

  The first checking means 11 uses the satisfaction determining means 13 to determine whether or not the logical expression composed of the postcondition and the invariant condition in the policy description to be checked can be satisfied after the logical expression is converted. (Step B30). The first inspection unit 11 determines whether or not the satisfaction determination unit 13 determines that the satisfaction is possible (step B40). When it is determined that the logical expression cannot be satisfied, the first checking unit 11 determines that the policy description to be checked has an illegal action on the management target system, and the policy description is output to the output device 15. Is output (step B50), and the entire process is terminated. When it is determined that the logical expression is satisfiable, the first checking unit 11 determines that the policy description to be checked does not have an illegal action on the management target system, and sets the policy description and the invariant condition as the first. 2 is passed to the inspection means 12 to execute the inspection in step A30 (FIG. 4).

  FIG. 6 shows an operation procedure of the inspection by the second inspection means 12 in step A30 of FIG. The second checking means 12 receives from the first checking means 11 the policy description that has been confirmed to be satisfiable simultaneously with the invariant condition and the invariant condition in the procedure shown in FIG. When receiving the policy description and the invariant condition, the second checking means 12 reads all policy specifications included in the registered policy description from the policy storage unit 162 (step C10), and starts checking the policy description. The second inspection means 12 determines whether or not the inspection has been completed for all of the read policy specifications (step C20). If the inspection has not yet been completed, one of the unexamined policy specifications is selected. Select (step C30).

  The second checking means 12 determines whether or not the policy description to be checked received from the first checking means 11 is likely to be fired simultaneously with the policy specification selected in Step C30 (Step C40). When it is determined that there is a possibility of simultaneous firing in step C40, the policy description to be examined and the policy description selected in step C30 are applied simultaneously under the conditions to be satisfied by the managed system. It means that there is a possibility. If there is no possibility of firing at the same time, the two policy descriptions are not applied at the same time. Therefore, the process returns to Step C20, and it is determined whether there is still a policy specification that has not been checked. Select a policy specification. If the second checking means 12 determines that simultaneous firing is possible, it determines whether the policy description to be checked and the policy specification selected in step C30 can be executed simultaneously (step C50).

  If the second checking means 12 determines that the simultaneous execution is impossible in Step C50, the second checking means 12 outputs that there is a problem in the policy description using the output device 15 (Step C60), and ends the entire processing. If it is determined that simultaneous execution is possible, the process returns to step C20 to determine whether or not an unexamined policy description remains. The second inspection unit 12 performs the inspection from step C30 to step C50 until it is determined in step C20 that there is no unexamined policy specification. As a result of the inspection, the second inspection means 12 determines that there is no problem in the policy description to be inspected when there is no policy specification determined in step C50 that it cannot be executed simultaneously with the policy description to be inspected. Then, the policy description to be examined is registered in the policy storage unit 162 (step C70), and the examination is terminated.

  FIG. 7 shows details of the operation procedure of step C40 (FIG. 6) for determining the possibility of simultaneous firing. In step C40, first, the second checking means 12 first calculates a logical expression obtained by combining the precondition included in the policy description to be checked, the invariant condition, and the precondition of the policy specification selected in step C30. Create (step D10). Next, the created logical expression is converted into a form that can be inspected by the satisfaction determination means 13 (step D20). Thereafter, whether or not the logical expression created in step D10 can be satisfied is determined using the satisfaction determination means 13 (step D30).

  The second inspection means 12 determines whether or not it is determined that it is satisfactorily determined in Step D30 (Step D40). If it is determined that the logical expression can be satisfied, the policy description to be inspected and the policy description associated with the policy specification selected in step C30 (FIG. 6) may be fired at the same time. It is determined that ignition is possible (step D50). In this case, the process proceeds from step C40 to step C50 to check whether simultaneous execution is possible. On the other hand, if it is determined that the logical expression cannot be satisfied, the policy description to be examined and the policy description corresponding to the selected policy specification are not likely to fire at the same time, so it is determined that there is no simultaneous firing. (Step D60). If not simultaneously fired, it is determined that no mismatch occurs between the policy descriptions for the combination, and the process returns from step C40 to step C20 to select the next policy specification.

  FIG. 8 shows details of the operation procedure of step C50 (FIG. 6) for determining whether or not execution is possible. In step C50, first, the second checking means 12 first generates a logical expression obtained by combining the postconditions included in the policy description to be checked, the invariant conditions, and the postconditions of the policy specification selected in step C30. Create (step E10). Next, the created logical expression is converted into a form that can be inspected by the satisfaction determination means 13 (step E20). Thereafter, whether or not the logical expression created in step E10 can be satisfied is determined using the satisfaction determination means 13 (step E30).

  The second inspection means 12 determines whether or not it is determined that the satisfaction is possible in the determination of Step E30 (Step E40). If it is determined that the logical expression is satisfiable, there is no problem even if the policy description to be examined and the policy description corresponding to the policy specification selected in step C30 (FIG. 6) are executed simultaneously. It is determined that simultaneous execution is possible (step E50). In this case, the process returns from step C50 to step C20, and an inspection with the following combination is performed. On the other hand, if it is determined that the logical expression cannot be satisfied, it is determined that the policy description to be inspected and the policy description corresponding to the selected policy specification cannot be executed simultaneously (step E60). ). Such a combination of policy descriptions is invalid, and the process proceeds from step C50 to step C60 to output that there is a problem with the policy to be examined.

  In the present embodiment, when the consistency between two policy descriptions is checked due to the satisfiability of the predicate logical expression corresponding to the policy description, the logical expression corresponding to the policy description to be inspected and the already registered policy are checked. Create a logical expression that is obtained by combining the logical expression corresponding to the description with the invariant that always holds for the status of the managed system. to decide. In this way, by adding the properties of the managed system as constraints at the time of inspection, the environment to which the policy description is applied can be expressed as a logical expression more accurately, and as a result, the policy description can be more accurately described. You will be able to inspect problems.

  Next, a second embodiment of the present invention will be described. FIG. 9 shows the configuration of the policy inspection system according to the second embodiment of the present invention. The policy inspection system 10a of this embodiment is different from the policy inspection system 10 of the first embodiment shown in FIG. 1 in that the storage device 16a includes a key attribute storage unit 163. In this embodiment, the managed system is represented by an object-oriented information model, and when the condition is described using the class or attribute name appearing in the information model, the instances indicated by the bound variables are the same. Is included as a constraint in the logical expression. As an example of an information model that expresses a managed system, “CIM Core Model White Paper ver2.4” August 30, 2000 [online] [March 2005] 8 day search], Distributed Management Task Force, Internet <URL http://www.dmtf.org/standards/documents/CIM/DSP0111.pdf> There is M (CIM).

  Each managed object constituting the managed system is expressed as an instance of a class having a specific property. Hereinafter, prior to the description of the condition inspection system in the present embodiment, an example of conditions for the state of such a managed system will be shown. Assume that the state of a process that runs on a computer that is a managed system and that provides a specific service to the outside is expressed as an instance of a Service class. At this time, the Service class has Name and Status as attributes representing the state. Name is the name of the service, and Status indicates the operating status of the service.

The following conditions can be considered as conditions related to the Service class.
∃s∈Service, s.Name = “mysql” ∧ s.Status = “running” (Logical expression A)
The above condition (logical expression A) indicates that there is an instance of the Service class, the Name attribute is mysql, and the Status attribute is running. Such a logical expression may be given as, for example, a pre-condition of a policy description that is fired when the MySQL service is activated, or a post-condition of a policy description that activates the MySQL service.

Next, in order to explain the problem, apart from the logical expression A above,
∃t∈Service, t.Name = “mysql” ∧ t.Status = “stopped” (Logical formula B)
(Condition B). The logical expression B is different from the logical expression A described above in the value of the Status attribute. A combination of these two logical expressions A and B can be satisfied.

  On the other hand, in order to uniquely identify an instance, a specific attribute takes a unique value among instances of the class. Such an attribute is called a Key attribute. Assuming that the Name attribute is the Key attribute, in the logical expressions A and B, since the value of the Name attribute is equal between s and t, s and t give a statement for the same instance. In this case, since a condition is given to set different values for the attribute of the same instance in a certain logical expression, that is, a policy description and another policy description, the policy description of such a combination is The result must be output so that it does not match. As described above, in order to realize the satisfiability determination in consideration of the case where the instances are the same, in this embodiment, the equivalence constraint of the instances is added at the time of satisfaction determination using the Key attribute.

  The key attribute storage unit 163 stores a class name and a list of key attributes defined in the class name in association with each other. In one class, one or more key attributes are defined. When there are a plurality of key attributes, a value obtained by combining a plurality of key attributes is unique among instances of the same class. In this embodiment, the 1st test | inspection means 11 and the 2nd test | inspection means 12 add the equivalence restrictions using a Key attribute to the formula which determines satisfiability, and determine satisfiability.

  FIG. 10 shows an operation procedure of a process for adding an equivalence constraint of an instance to be executed before the satisfiability determination. This process is executed after the logical expression is converted into a format that can be inspected by the satisfaction determination means 13 in step B20 (FIG. 5), step D20 (FIG. 7), or step E20 (FIG. 8). Note that the logical expression to which the equivalence constraint is to be added is a combination of the postcondition and the invariant condition (Fig. 5), the precondition of the policy description to be examined, the invariant condition, and the precondition of the registered policy description. Or a combination of the post-conditions of the policy description to be inspected, the invariant condition, and the post-conditions of the registered policy description (FIG. 8). In the following, as an example, the first checking means 11 applies an equivalence constraint to a logical expression in which a postcondition and an invariant condition are combined with each other. It explains using.

  The first checking means 11 first converts the logical expression into the crown standard form. As a result, the names of the bound variables appearing in the logical expressions are renamed so as not to overlap. Next, a table is created in which a class name appearing in the logical expression and a list of bound variable names associated with instances of the class name are paired (step F10). At this time, when the number of binding variables corresponding to the instance of the class is only one, it is not included in the table.

  Each row of the table created in step F10 stores a class name and a corresponding bound variable list. The first checking means 11 determines whether or not the processing has been completed for all the rows in the table (step F20). When an unprocessed line remains, one unprocessed line (class name) is selected (step F30). The first checking means 11 creates possible combinations of the respective bound variables that can be created by selecting two from the list of bound variables included in the selected row. Thereafter, it is determined whether or not an unprocessed combination exists in the created combination (step F40).

  When an unprocessed combination remains, the first checking unit 11 selects one of the unprocessed combinations and creates an empty list for storing logical expressions (step F50). This list is called a restriction list. The first checking unit 11 uses the class name included in the selected row to acquire a list of Key attribute names defined for the class name from the Key attribute storage unit 163 (Step F60). The first inspection unit 11 determines whether or not the processing has been completed for all of the acquired key attributes (step F70).

  The first checking means 11 selects one unprocessed Key attribute when the processing has not been completed for all the Key attributes, and generates a logical expression indicating that the Key attributes of the binding variables included in the combination are equal. Generate. The first checking means 11 stores the generated logical expression in the constraint list (step F80). At this time, if the constraint list is empty, the first checking unit 11 stores the generated logical expression in the constraint list as it is. When a logical expression is already stored in the constraint list, a combination of the logical expression to be stored and the stored logical expression is stored in the constraint list.

  For example, if the combination of bound variable names is x and y and the Key attribute name is p, the generated logical expression is x. p = y. p. If the constraint list is empty, the first checking means 11 adds x. p = y. Store p. If the logical expression L is already stored in the constraint list, L∧ (x.p = y.p) is stored in the constraint list in step F80.

The first inspection unit 11 returns from step F80 to step F70, and determines whether or not an unprocessed combination exists. When the processing is completed for all the key attributes, the logical expression included in the constraint list and the logical expression indicating that the instances indicated by the variable names included in the combination are logically equivalent. And the constraint is added to the logical expression for which the satisfaction is determined by connecting the created logical expressions (step F90). For example, if the logical expression included in the constraint list is L and the combination of bound variable names is x and y, the generated logical expression is
(L) ⇔ (x = y) or ((L) → (x = y)) ∧ ((x = y) → (L))
It becomes. Assuming that the generated logical expression is Q, and T is a logical expression for which satisfaction is determined, in step F90, T∧Q is generated by linking the logical expression T and the logical expression Q.

  After executing Step F90, the first inspection unit 11 returns to Step F40 and determines whether there is an unprocessed combination. When there is an unprocessed combination, the process proceeds to step F50, and one unprocessed row is selected. When the processing after step F50 is executed for all combinations, the process returns to step F20, and it is determined whether or not the processing has been completed for all the rows of the table created in step F10. When an unprocessed line remains, the process proceeds to step F30, and one unprocessed line is selected. When there is no unprocessed row, that is, for all the rows of the created table, the processing of the equivalence constraint is terminated when the processing of step F20 and subsequent steps is completed, and the subsequent satisfiability determination processing (step B30 (FIG. 5 Go to)).

  In the present embodiment, before giving a logical expression to the satisfaction determination means 13 and making a determination, a constraint expression related to equivalence is created for each class and for each combination of bound variables, and this is used to determine the satisfaction. The satisfaction determination means 13 makes a determination on the logical expression to which the constraint expression is added. As described above, prior to the satisfaction determination of the logical expression, the equivalence constraint of the instance is generated using the list of each Key attribute defined in the class name appearing in the logical expression, and the logical expression for performing the satisfaction determination By performing satisfaction after combining, the logical expression used for the inspection becomes more strict, and in addition to the effects obtained in the first embodiment, more accurate policy inspection considering instance equivalence is possible. The effect of becoming can be obtained.

  Next, a third embodiment of the present invention will be described. First, the purpose of this embodiment will be described. In the instance equivalence constraint addition described in the second embodiment, a constraint is added that instances that have the same value for all the Key attributes defined in the appearing class are the same. This constraint is satisfied when it is not clear whether or not the instances associated with the bound variables are the same, such as when any of the Key attributes is missing or when a condition related to the Key attribute does not appear. Does not affect. Therefore, in addition to the case where the instances are surely the same, there is a need for means for regarding the instances as being the same even when it is not clear whether the instances are the same. In the present embodiment, a constraint is added that the instances associated with the bound variables are equal, except when the logical expression condition clearly indicates that the instances are different. In this way, when it is not known whether the instances are the same or different, it is possible to determine the satisfiability by adding the constraint that “the instances are the same”.

  The configuration of the policy inspection system in the present embodiment is the same as the configuration of the policy inspection system 10a shown in FIG. FIG. 11 shows a part of the operation procedure of the present embodiment. The operation of the policy inspection system of this embodiment is different from the operation procedure of the second embodiment in the processing steps after step F60 in the constraint addition processing shown in FIG. When the first checking means 11 (or the second checking means 12) selects one combination of a specific class name and a bound variable name associated with the class name in step F50 (FIG. 10), A list of key attributes defined in the class name is acquired from the key attribute storage unit 163, and two bound variable names included in the combination in the logical expression that performs satisfaction determination among the acquired key attributes are used. Only the Key attribute referred to is detected (step G10).

  For example, it is assumed that the bound variable names included in the combination are x and y, and the class named ClassA is being processed. Further, it is assumed that the Key attribute of Class A is p1 and p2. In this case, if attribute references “x.p1”, “y.p1”, and “y.p2” appear in the logical expression, only the Key attribute p1 is detected in step G10. The Key attribute p2 is excluded because there is a reference by the bound variable y but there is no reference by the bound variable x. The first inspection means 11 determines whether or not the Key attribute has been detected in Step G10 (Step G20). If the detected Key attribute does not exist, a constraint that the two bound variable names included in the combination are equal is added to the constraint list (step G50). For example, if two bound variable names included in the combination are x and y, (x = y) is added to the constraint list.

  The first inspection unit 11 determines whether or not the processing has been completed for all the Key attributes detected in Step G10 (Step G30). If there is an unprocessed Key attribute, select one of them, generate a logical expression indicating that the Key attributes of the binding variables included in the combination are equal, and add the generated logical expression to the constraint list. Store (step G40). In step G40, as in step F80 of FIG. 10, if the constraint list is empty, the generated logical expression is stored in the constraint list as it is, and if the logical expression is already stored in the constraint list, the logic to be stored is stored. A combination of the expression and the stored logical expression is stored in the constraint list.

When the first checking means 11 stores the logical expression in the constraint list in step G40, the first checking means 11 returns to step G30 and determines whether or not all key attributes have been processed. When processing is completed for all the key attributes, the logical expression included in the constraint list and the logical expression indicating that the instances indicated by the variable names included in the combination are equal are logically equivalent. A logical expression is created, and the created logical expression is connected to the logical expression for which satisfaction is determined (step G60). For example, if the logical expression included in the constraint list is L and the combination of bound variable names is x and y, the logical expression to be created is
(L) ⇔ (x = y) or ((L) → (x = y)) ∧ ((x = y) → (L))
It becomes. Assuming that the created logical expression is Q, and T is a logical expression for performing satisfaction determination, T∧Q
Is a new logical expression for performing a satisfaction determination.

  The above-described constraint addition procedure to which the process shown in FIG. 11 is added is preferably inserted between step B20 and step B30 in FIG. 5 and between step E20 and step E30 in FIG. This is because the inspection shown in FIG. 5 and the inspection shown in FIG. 8 may be dangerous because it determines whether the policy description to be inspected collides with an invariant condition or another policy description. This is because it is preferable that the above cannot be satisfied. When it is not known whether or not the instances are the same, by making them the same, it becomes more difficult to satisfy the logical expression, and a potentially problematic policy description can be detected.

  On the other hand, in the inspection shown in FIG. 7, since policies that may be ignited simultaneously with the description of the policy to be inspected are selected, only combinations of policies that do not ignite at the same time should be excluded. If it is determined that the instances are the same when it is not known whether or not the instances are the same, there is a possibility that a combination of policy descriptions may be excluded because of the possibility of firing simultaneously. Therefore, unlike the inspection of FIG. 5 and the inspection of FIG. 8, the constraint addition operation of the procedure shown in FIG. 10 described in the second embodiment is inserted between step D20 and step D30 of FIG. It is preferable.

  In the present embodiment, among the bound variables appearing in the logical expression, in particular, inspecting the invariant condition and the postcondition (FIG. 5) and checking the postcondition and invariant condition of the two policy descriptions (FIG. 8). Thus, for a bound variable that is not referenced from the corresponding two bound variables, a constraint is added that the instances are equal. In this way, when it is not clear whether or not the instances are equal, it is possible to constrain the instances to be equal, and this broadly detects combinations of policy descriptions that may be problematic. It becomes possible.

  In the present invention, the conditions described in the first-order predicate logic include logical operators such as concatenation ∧, disjunction 含, implication →, negative ¬, and numerical values and characters such as “<”, “>”, “=”, etc. It is composed of a predicate based on a column comparison operation, a universal symbol ∀, an existence symbol 文字, and a character string that expresses the symbol ∈ indicating that the bound variable x such as x∈Class belongs to an instance of the class name Class by ASCII characters. The To refer to the attribute value of an instance, x. Describe as p. x is a bound variable name, and p is an attribute name defined for the class of the instance to which the bound variable belongs.

The outline of a method for performing satisfaction determination will be specifically described by taking two conditions described below as examples. The equivalence constraint adding method described here is in accordance with the second embodiment. A case will be described in which the following condition 1 is included in the policy description to be inspected, and the following condition 2 is set as an invariant condition, and the satisfaction determination is performed. It is assumed that the Key attribute of the class “Service” is only an attribute named “Name”.
Condition 1: exists s in Service, s.Name = "mysql" and s.Status = "running"
Condition 2: exists s in Service, s.Name = "mysql" and s.Status = "stopped"

A logical expression that is obtained by combining the above conditions into a canonical standard form is shown below.
exists s, t in Service, s.Name = "mysql" and s.Status = "running" and t.Name = "mysql" and t.Status = "stopped"
The steps so far correspond to step B10 (FIG. 5) and step B20. The procedure for converting a logical expression into a canonical standard form is well known.

A constraint addition procedure using the Key attribute shown in FIG. 10 is performed. The only class name that appears in the logical expression is Service. There are two bound variables that appear in the logical expression, s and t, and the combination is only (s, t). On the other hand, the Key attribute of Service is “Name”, which restricts the following logical expression added in Step F90.
((S.Name = t.Name) implies s = t)

  Next, a satisfaction determination method in the case where the satisfaction determination unit 13 implements simplify as a satisfaction possibility determination tool will be described. In order to make a satisfaction determination using a simplify, access to an attribute value of an instance is converted into a function call, and a character string is converted into an integer by taking a hash value, for example, and a logical expression is expressed by an S expression. Just do it. Further, in order to determine the satisfiability of negation of a given logical expression, the simplify preliminarily inverts the given logical expression.

A conversion of the above example into a logical expression given to simplify is shown below. Here, the character string mysql is replaced with 1, the running is replaced with 2, and the stopped is replaced with an integer of 3.
(NOT (EXISTS (st)
(AND
(AND
(AND (EQ (Service ## Name s) 1)
(EQ (Service ## Status s) 2))
(AND (EQ (Service ## Name t) 1)
(EQ (Service ## Status t) 3)))
(IFF
(EQ (Service ## Name s) (Service ## Name t))
(EQ st)))))
Since the above logical expression cannot be satisfied, a reply “valid” is issued in the simplify. Note that if it is satisfiable or cannot be determined, an invalid response is returned. Since the logical expression satisfaction determination (step B40) is completed and it is determined that the logical expression cannot be satisfied, the process proceeds to step B50, and an error is output.

  The present invention has been described above based on the preferred embodiment. However, the policy inspection system, method, and program of the present invention are not limited to the above embodiment, and various configurations are possible from the configuration of the above embodiment. Those modified and changed as described above are also included in the scope of the present invention.

  The present invention can be applied to uses such as a policy inspection apparatus for inspecting a policy description problem and a program for realizing the policy inspection apparatus in a computer when creating a policy description. Further, it can be applied to a policy management apparatus that manages a computer system or a network system in accordance with a policy description, and detects and eliminates an inappropriate policy description at the time of registration.

The block diagram which shows the structure of the policy inspection system of 1st Embodiment of this invention. The block diagram which shows the structure of a policy description. The block diagram which shows the structure of a policy specification. The flowchart which shows the schematic procedure of the whole operation | movement of a policy inspection system. The flowchart which shows the operation | movement procedure of the test | inspection by a 1st test | inspection means. The flowchart which shows the operation | movement procedure of the test | inspection by a 2nd test | inspection means. The flowchart which shows the detail of the operation | movement procedure of the step which judges the possibility of simultaneous ignition. The flowchart which shows the detail of the operation | movement procedure of the step which determines whether it can perform. The block diagram which shows the structure of the policy inspection system of 2nd Embodiment of this invention. The flowchart which shows the operation | movement procedure of the process which adds the equivalence constraint of an instance. The flowchart which shows the one part operation | movement procedure of the addition process of an equivalence constraint. The block diagram which shows the structure of the policy inspection system described in the nonpatent literature 1. FIG. The block diagram which shows the structure of the policy inspection system described in the nonpatent literature 2. FIG.

Explanation of symbols

10: Policy inspection system 11: First inspection means 12: Second inspection means 13: Satisfaction determination means 14: Input device 15: Output device 16: Storage device 161: Invariant condition storage unit 162: Policy storage unit 163: Key Attribute storage unit 71: policy description 72: policy specification

Claims (13)

A policy inspection system for inspecting a policy description to be inspected,
An input device for applying accept the policy description of said object,
An invariant condition storage unit that stores an invariant condition in which a condition that is always satisfied for the state of the managed system is described by first-order predicate logic;
A policy storage unit for storing registered policy descriptions;
A post-condition represented by a predetermined logical expression describing a condition to be satisfied with respect to the state of the managed system immediately after the operation defined in the policy description received by the input device using first-order predicate logic; and Inspection means for inspecting the policy description of the inspection object received by the input device based on the invariant condition stored in the invariant condition storage unit;
The inspection means is
A sufficiency judging means for judging sufficiency of the logical expression;
Refer to the invariant condition stored in the invariant condition storage unit and the registered policy description stored in the policy storage unit, and the post-condition and the registration included in the policy description of the inspection target received by the input device A logical expression generation means for generating a logical expression that is a combination of the postcondition included in the finished policy description and the invariant condition;
Policy consistency checking means for determining the satisfiability of the logical expression generated by the logical expression generation means using the satisfaction determination means;
A key attribute storage unit that stores information on a key attribute that always takes a unique value between the same classes with respect to the class of the managed system among the attributes of the instance that represents the state of the managed system;
Have
Prior to the determination by the policy consistency checking unit, the invariant condition storage unit is referred to, and a logical expression is generated by combining the postcondition included in the policy description to be inspected and the invariant condition. A fraud policy checking means for determining the satisfiability of the logical expression using the satisfaction determination means;
State of the managed system therefore is represented in instance,
The fraud policy inspection means includes:
Prior to sufficiency determination by the satisfaction judgment means, the Key attribute storage unit with reference to, corresponding to the bound variables appearing in formulas to be sufficiency determination of the states instance that expresses the managed system Add an equality constraint as a constraint to the formula, provided that the attached instances are equal,
When the values of the Key attributes of two bound variables appearing in the logical expression subject to the sufficiency determination are equal, the instances corresponding to the two bound variables are equal, and when the two bound variables are equal, Add all Key attribute value is equal to such value constraints you two bound variables in formulas to be the sufficiency determination,
A policy inspection system characterized by that. The policy description further includes a precondition in which the policy firing condition is described in first order predicate logic,
The policy consistency checking means refers to the invariant condition storage unit and the policy storage unit, and includes a precondition included in the policy description to be inspected, a precondition included in the registered policy description, and the invariant condition. Is generated using the above-described satisfaction determination means, and if it is determined that the satisfaction is satisfied, the post-conditions included in the policy description to be inspected, and The policy checking system according to claim 1, wherein a satisfiability of a logical expression obtained by combining the postcondition included in the registered policy description and the invariant is determined. The fraud policy inspection means includes:
For any two combinations of the bound variables that appear in the logical expression that is the target of the sufficiency determination, whether there is a Key attribute that is referenced using the two arbitrary bound variables in the logical expression determine whether, when it is determined that there is no added equivalence constraint shall be the instances are equal corresponding to the arbitrary two bound variables in formulas to be the sufficiency determination, if it is determined that there is , When the values of all Key attributes of any two bound variables are equal, the instances corresponding to the two bound variables are equal, and when any two bound variables are equal, all of the two bound variables are all Add the value is equal to the equivalence constraint you of Key attributes to the logical expression to be the sufficiency determination, the policy checking system according to claim 1 or 2. The policy consistency checking means includes:
When the values of the Key attributes of two bound variables appearing in the logical expression subject to the sufficiency determination are equal, the instances corresponding to the two bound variables are equal, and when the two bound variables are equal, Add all Key attribute value is equal to such value constraints you two bound variables in formulas to be the sufficiency determination, the policy checking system according to claim 1, 2 or 3. The policy consistency checking means includes:
For any two combinations of the bound variables that appear in the logical expression that is the target of the sufficiency determination, whether there is a Key attribute that is referenced using the two arbitrary bound variables in the logical expression determine whether, when it is determined that there is no added equivalence constraint shall be the instances are equal corresponding to the arbitrary two bound variables in formulas to be the sufficiency determination, if it is determined that there is , When the values of all Key attributes of any two bound variables are equal, the instances corresponding to the two bound variables are equal, and when any two bound variables are equal, all of the two bound variables are all Add the value is equal to the equivalence constraint you of Key attributes to the logical expression to be the sufficiency determination, the policy checking system according to any one of claims 1 to 4. Policy for storing an input device for accepting a policy Identifier Description inspected, and invariant condition storage unit always stores the described invariants by first-order logic conditions which satisfies the state of the managed system, the registered policy description It is expressed by a predetermined logical expression describing a condition to be satisfied for the state of the managed system immediately after the operation defined in the policy description received by the storage unit and the input device, using first-order predicate logic. Inspection using a computer having inspection means for inspecting the policy description of the inspection object received by the input device based on the postcondition and the invariant condition stored in the invariant condition storage unit A policy inspection method for inspecting a target policy description,
A first-order predicate representing the invariant condition stored in the invariant condition storage unit by the computer and a condition to be satisfied for the state of the managed system immediately after the operation defined in the policy description input by the input device A step of inspecting the policy description to be inspected by an inspection means based on a logical expression described by logic;
The policy description includes a post-condition that describes the condition to be satisfied for the state of the managed system immediately after the operation defined in the policy description by the first-order predicate logic and a pre-condition that describes the policy firing condition by the first-order predicate logic. Including
Checking the policy description comprises the steps of:
The computer refers to the invariant condition storage unit that stores the invariant condition, and generates a logical expression obtained by combining the a posteriori condition included in the policy description to be examined and the invariant condition;
A fraud policy checking step for determining satisfiability of the generated logical expression;
If it is determined that the illegal policy checking step is satisfied, the invariant condition storage unit and the policy storage unit are referred to, the precondition included in the policy description to be inspected, the precondition included in the registered policy description, and the invariant Generating a logical expression that is a combination of conditions;
Determining the satisfiability of the generated logical expression;
If it is determined that the condition is satisfied in the determining step, the invariant condition storage unit and the policy storage unit are referred to, the postcondition included in the policy description to be examined, the postcondition included in the registered policy description, and the invariant condition. Generating a logical expression obtained by combining
A policy consistency check step for determining satisfiability of the generated logical expression; and
Have
Prior to the determination by the policy consistency checking step, the invariant condition storage unit is referred to, and a logical expression is generated by combining the postcondition included in the policy description to be inspected and the invariant condition. A fraud policy checking step for determining satisfiability of the logical expression;
Prior to the sufficiency determination of the logical expression, the illegal policy checking step is a key attribute of the Key attribute that always takes a unique value among the same class among the attributes of the instance expressing the state of the managed system. By referring to the Key attribute storage unit that stores information, an equivalence constraint is added to the logical expression as a restriction on the condition that the instances associated with the bound variables appearing in the logical expression that is the target of the sufficiency determination are equal. Including steps,
In the step of adding the constraint, when the values of the Key attributes of the two bound variables appearing in the logical expression subject to the sufficiency determination are equal, the instances corresponding to the two bound variables are equal, and the 2 one of the added all equivalence constraint shall be the value of the Key attribute is equal of the two bound variables in formulas to be the sufficiency determining when bound variables are equal,
A policy inspection method characterized by the above. In the step of adding the constraint, any two combinations of the bound variables appearing in the logical expression that is the target of the sufficiency determination are referred to in the logical expression using the two arbitrary bound variables. that determines whether or not the Key attribute is present, it is determined that there is no logical expression comprising the equivalence constraint shall be the instances are equal corresponding to the arbitrary two bindings variables subject to the sufficiency determination The policy inspection method according to claim 6, which is added to. The policy description includes a post-condition that describes the condition to be satisfied for the state of the managed system immediately after the operation defined in the policy description by the first-order predicate logic and a pre-condition that describes the policy firing condition by the first-order predicate logic. Including
Checking the policy description comprises the steps of:
The computer refers to the invariant condition storage unit and the policy storage unit, and combines the precondition included in the policy description to be inspected, the precondition included in the registered policy description, and the invariant condition. and generating the logical expression, of the attributes of an instance that represents the state of the managed system, by referring to Key attribute storage unit that stores information Key attributes whose always unique value between the same class, before article added the equivalent constraint that instance associated with the bound variable appearing the precondition and invariant conditions ∧ bound logical expression that is generated is provided that is equal as a constraint in the logical expression, adding the constraint If it is determined that the logical expression is satisfiable and is satisfied in the satisfaction determination, the invariant condition storage unit and the policy storage unit are referred to, and the policy description to be inspected is referred to. And Murrell postcondition, wherein a post-condition included in the registered policy description, the a invariants generate ∧ bound logical expression of attributes of an instance that represents the state of the managed system, between the same class Referring to the Key attribute storage unit that stores information of the Key attribute that always takes a unique value, it is associated with a bound variable that appears in a logical expression generated by linking the postcondition and the invariant condition. added the equivalent constraint that the condition that the instance is equal as a constraint in the logical expression has a logical expression policy consistency check determining satisfiability of plus the constraints,
In the policy consistency checking step, when a constraint is applied to a logical expression, if all the Key attribute values of the two bound variables appearing in the logical expression subject to the sufficiency determination are equal, the two bound variables are equal the corresponding instance, and adding all the values are equal the equivalence constraint you of Key attributes of the two of the two bound variables when bound variables is equal to a logical formula to be the sufficiency determination The policy inspection method according to claim 6 or 7. In the policy consistency checking step, for any two combinations of bound variables appearing in a logical expression obtained by linking the post-condition and the invariant condition, the arbitrary two bound variables are included in the logical expression. determining whether the Key attribute referenced there with, if it is determined that there is added equivalence constraint shall be the instances are equal corresponding to the arbitrary two bound variables in the formulas The policy inspection method according to claim 8. A program for causing a computer to execute a process for inspecting a policy description to be inspected,
The computer, an input device to attach accept the policy description of the test object, and invariant condition storage unit always stores the described invariants by first-order logic to establish conditions for the state of the managed system, policy description registered And a predetermined logical expression describing a condition to be satisfied for the state of the managed system immediately after the operation defined in the policy description received by the input device using first-order predicate logic Based on the a posteriori condition represented by the above and the invariant condition stored in the invariant condition storage unit, function as an inspection unit that inspects the policy description of the inspection object received by the input device ,
In the computer,
An invariant condition in which a condition that is always satisfied for the state of the managed system is described by first-order predicate logic, and a condition that should be satisfied for the state of the managed system immediately after the operation defined in the policy description input by the input device Based on a logical expression described by first-order predicate logic, and a program for executing the step of checking the policy description to be checked by the checking means,
The policy description includes a post-condition that describes the condition to be satisfied for the state of the managed system immediately after the operation defined in the policy description by the first-order predicate logic and a pre-condition that describes the policy firing condition by the first-order predicate logic. Including
Checking the policy description comprises the steps of:
An illegal policy that refers to the invariant condition storage unit, generates a logical expression that is a combination of the postcondition included in the policy description to be examined and the invariant condition, and determines whether the generated logical expression is satisfiable An inspection step;
When it is determined that the illegal policy checking step is satisfied, the invariant condition storage unit and the policy storage unit are referred to, the precondition included in the policy description to be checked, the precondition included in the registered policy description, Generate a logical expression that is combined with the invariant condition, determine the satisfiability of the generated logical expression, and determine that the logical expression is satisfied in the determination, refer to the invariant condition storage unit and the policy storage unit, Generate a logical expression that combines the post-conditions included in the policy description to be inspected, the post-conditions included in the registered policy description, and the invariant conditions, and determine the satisfiability of the generated logical expression A policy consistency check step,
The fraud policy checking step includes:
Prior to determining the sufficiency of the logical expression, a key attribute storage unit that stores key attribute information that always takes a unique value among the same class among the attributes of the instance representing the state of the managed system is referred to. Adding an equivalence constraint as a constraint to the logical expression, provided that the instances associated with the bound variable appearing in the logical expression that is the subject of the sufficiency determination are equal ,
In the step of adding the constraint, when the values of the Key attributes of the two bound variables appearing in the logical expression subject to the sufficiency determination are equal, the instances corresponding to the two bound variables are equal, and the 2 one of the added all equivalence constraint shall be the value of the Key attribute is equal of the two bound variables in formulas to be the sufficiency determining when bound variables are equal,
A program characterized by that. In the step of adding the constraint, any two combinations of the bound variables appearing in the logical expression that is the target of the sufficiency determination are referred to in the logical expression using the two arbitrary bound variables. that determines whether or not the Key attribute is present, it is determined that there is no logical expression comprising the equivalence constraint shall be the instances are equal corresponding to the arbitrary two bindings variables subject to the sufficiency determination The program according to claim 10, added to the program. The policy description includes a post-condition that describes the condition to be satisfied for the state of the managed system immediately after the operation defined in the policy description by the first-order predicate logic and a pre-condition that describes the policy firing condition by the first-order predicate logic. Including
Checking the policy description comprises the steps of:
Referring to the invariant condition storage unit and the policy storage unit, a logical expression obtained by combining the precondition included in the policy description to be examined, the precondition included in the registered policy description, and the invariant condition The key attribute storage unit that stores the key attribute information that always takes a unique value among the same class among the attributes of the instance that represents the state of the managed system that is generated, and is invariant with the precondition An equivalence constraint is added to the logical expression as a constraint, provided that the instances associated with the bound variables appearing in the logical expression generated by linking the conditions with each other are equal , and the logical expression satisfying the constraint is satisfied Determining the possibility, and determining that the satisfaction is satisfied in the satisfaction determination, refer to the invariant condition storage unit and the policy storage unit, and a postcondition included in the policy description of the inspection target; And post-condition included in the serial registered policy description, the a invariants generate ∧ bound logical expression of attributes of an instance that represents the state of the managed system, always only value between the same class Referring to a key attribute storage unit that stores information on the key attribute to be taken, the condition is that the instances associated with the bound variable appearing in the logical expression generated by linking the postcondition and the invariant condition are equal And a policy consistency check step for determining the satisfiability of the logical expression to which the constraint is added,
In the policy consistency checking step, when a constraint is applied to a logical expression, if all the Key attribute values of the two bound variables appearing in the logical expression subject to the sufficiency determination are equal, the two bound variables are An equivalence constraint is added to the logical expression subject to the sufficiency determination that the corresponding instances are equal and the values of all the Key attributes of the two bound variables are equal when the two bound variables are equal. Item 12. The program according to item 10 or 11.   In the policy consistency checking step, for any two combinations of bound variables appearing in a logical expression obtained by linking the post-condition and the invariant condition, the arbitrary two bound variables are included in the logical expression. Whether or not the Key attribute referred to exists, and if it does not exist, an equivalence constraint that the instances corresponding to the two arbitrary bound variables are equal is added to the logical expression. Item 13. The program according to item 12.

Images