Per group verification

• US 8,826,238 B2
• Filed: 01/22/2009
• Issued: 09/02/2014
• Est. Priority Date: 01/22/2009
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Shapiro, Adam, McGarvey, Conal, Levin, Vladimir A., Lichtenberg, Jakob F.
• Primary Examiner(s): Bullock, Jr., Lewis A
• Assistant Examiner(s): APONTE, FRANCISCO JAVIER
• Application Number:
  US12/357,583
• Publication Number:
  US 20100186003A1
• Time in Patent Office: 2,049 Days
• Field of Search: 717101-178, 706/47, 716/107, 709/203, 709/217, 714/1, 714/25, 714/E11.163, 714/38.14, 714/15, 714/E11.207, 703/21, 719/332
• US Class Current: 717/126
• CPC Class Codes: G06F 11/3604 Software analysis for verifying properties of programs byte-code verification G06F9/44589
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013
• CPC Class Codes: G06F 11/3612 by runtime analysis performance monitoring G06F11/3466
• CPC Class Codes: G06F 9/44589 Program code verification, e.g. Java bytecode verification, proof-carrying code high-level semantic checks G06F8/43; testing and debugging software G06F11/36

Abstract

Various embodiments provide per group verification techniques in which code may be verified against one or more rules on a group by group basis. In one or more embodiments relationships between portions of a module to be verified can be defined. By being aware of relationships between various code portions, various embodiments can divide a module into related groups and perform verification on the basis of the groups. Multiple groups can be derived based at least in part upon the relationships. Each group can then be verified separately for compliance with one or more rules. Verification results can be output for each of the groups.

Claims

1. A computer-implemented method comprising:

ascertaining multiple pathways in code to be verified by referencing a harness file that designates a position of callbacks within the code relative to a non-deterministic portion of the code defined by one or more non-deterministic choices, harness designations being sufficient to identify the multiple pathways;

forming groups for verification of the code according to identified pathways, each of the groups containing a portion of the code to be verified; and

directly verifying the code against one or more rules using the formed groups, including;

for a first rule;

executing respective pathways in the code corresponding to each of the groups; and

monitoring to determine compliance of the respective pathways with the first rule; and

when the code is verified against multiple rules, for each other said rule;

executing the respective pathways in the code corresponding to each of the groups; and

monitoring to determine compliance of the respective pathways with the other said rule.

2. The method of claim 1, wherein the rules are defined for interaction of the code with an environment in which the code operates.

3. The method of claim 1, wherein the harness file that describes relationships between multiple entry points within the code.

4. The method of claim 1, further comprising outputting a different verification result for each of the formed groups.

5. The method of claim 1, wherein the code corresponds to a driver.

6. The method of claim 1, wherein:

callbacks occurring before the non-deterministic portion are designated as “

Pre” and

relate to initialization operations of the code;

callbacks occurring in the non-deterministic portion are designated as “

Core” and

relate to core functionality of the code; and

callbacks occurring after the non-deterministic portion are designated as “

Post” and

relate to clean-up operations of the code.

18. The method of claim 1, further comprising:

constructing an environment model that is representative of an environment in which the code operates; and

employing the environment model to verify the code against the one or more rules.

7. A computer-readable storage device storing computer readable instructions to implement a harness file configured to:

describe relationships between entry points within code of a module corresponding to the harness file, the relationships described by designating a position of the entry points relative to a non-deterministic portion of the code of the module defined by one or more non-deterministic choices;

enable a verifier tool, referencing the harness file to verify the code of the module against a single rule, to form groups of the code that are associated with the entry points according to the described relationships, the verifier tool configured to verify the code of the module against multiple rules by referencing multiple harness files, each configured to enable the verifier tool to verify the code of the module on a per group basis against a respective said rule;

verify compliance of the code of the module with a single rule by directly verifying compliance of each of the formed groups of the code with the single rule separately such that each of the formed groups of the code is individually verified with the single rule in a sequence indicated by the harness file; and

generate verification results that indicate whether each of the formed groups of the code separately complies with the single rule.

8. The computer-readable storage device of claim 7, wherein the described relationships reflect the structure of the entry points within the code of the module.

9. The computer-readable storage device of claim 7, wherein the described relationships categorize the entry points within the code of the module according to functionality.

10. A system comprising:

one or more processors;

one or more computer-readable storage devices;

one or more modules embodied on the one or more computer-readable storage devices that are operable through interaction with an operating system to control respective devices; and

a verifier tool embodied on the one or more computer-readable storage devices and configured to;

derive groups of code containing code of at least one module using harness files that define the groups of code for multiple rules such that a different harness file is configured to define the groups of code for each of the multiple rules, at least one of the harness files defining the groups of code differently than another harness file, use of the harness files involving making reference to the harness files that are configured to represent a structure of the code of the at least one module by categorizing multiple callbacks within the code of the at least one module according to a relationship of the multiple callbacks to a non-deterministic portion of the code of the at least one module; and

directly verify compliance of the code of the at least one module with the multiple rules that are defined for interaction of the code of the at least one module with the operating system on a per group basis, including;

verify compliance of the code on a per group basis with a first of the multiple rules; and

until compliance with each of the multiple rules is verified, verify compliance of the code on a per group basis with one of the multiple rules for which compliance remains to be verified.

11. The system of claim 10, wherein the verifier tool is configured to employ an environment model of the operating system to verify compliance of the code of the at least one module with the multiple rules.

12. The system of claim 10, wherein the groups of code are derived to group portions of the code of the at least one module that are functionally related.

13. The system of claim 10, wherein the groups of code each comprise one or more entry points contained within the code of the at least one module.

14. The system of claim 10, wherein the harness files are configured to describe relationships between callbacks within the code of the at least one module.

15. The system of claim 10, wherein the verifier tool is configured to derive groups of code by:

ascertaining multiple pathways in the code of the at least one module; and

forming the groups of code to correspond to the ascertained pathways.

16. The system of claim 10, wherein the verifier tool is configured to verify on a per group basis for each of the groups of code by:

executing one or more callbacks corresponding to a group of code;

monitoring to determine compliance of the callbacks with the rule; and

outputting a verification result for the group of code with respect to the rule.

17. The system of claim 10, wherein the verifier tool is configured to derive different groups of code for each of said multiple rules against which the code of the at least one module is verified.

19. The system of claim 11, wherein the verifier tool is configured to construct the environment model of the operating system, the environment model representative of an environment in which the code of the at least one module operates.

20. The system of claim 16, wherein:

callbacks occurring before the non-deterministic portion are designated as “

Pre” and

relate to initialization operations of the code of the at least one module;

callbacks occurring in the non-deterministic portion are designated as “

Core” and

relate to core functionality of the code of the at least one module; and

callbacks occurring after the non-deterministic portion are designated as “

Post” and

relate to clean-up operations of the code of the at least one module.