LOW-LEVEL CODE REWRITER VERIFICATION

• US 20110231824A1
• Filed: 03/16/2010
• Published: 09/22/2011
• Est. Priority Date: 03/16/2010
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Chabbi, Milind Mohan, Fernando, Casimir Lakshan
• Granted Patent: US 8,381,175 B2
• Time in Patent Office: Days
• US Class Current: 717/126
• CPC Class Codes: G06F 11/0751 Error or fault detection not based on redundancy power supply failures G06F1/30; network fault management H04L41/06
• CPC Class Codes: G06F 11/3604 Software analysis for verifying properties of programs byte-code verification G06F9/44589

Abstract

Verification of low-level rewriters such as binary rewriters involves “vanilla” rewriting a file to generate a rewritten low-level file without performing any optimization, compaction, or other substantive low-level code transformation during the rewrite. Then the metadata of the original low-level file is automatically compared with matching metadata of the rewritten low-level file for semantic equivalence. A properly functioning rewriter produces semantically equivalent files, whereas a defective rewriter may produce files whose metadata semantics differ. Comparison may distinguish composite metadata entities from self-contained metadata entities, and transitive closures of metadata may be compared. Comparison may also test for bitwise equality of self-contained metadata entities, and test for equality between respective flags, strings, fields, and/or methods of the original and rewritten files. Syntactic variants may be detected during comparison, and metadata may be converted into a canonical form to facilitate comparison.

Claims

1. A process for verifying operation of a low-level rewriter, the process utilizing a device which has at least one logical processor in operable communication with at least one memory, the process comprising the steps of:

obtaining initial low-level file(s) containing code and metadata;

generating rewritten low-level file(s) from the initial low-level file(s) by applying the low-level rewriter to the initial low-level file(s) independently of any low-level code transformation; and

comparing metadata of the initial low-level file(s) with matching metadata of the rewritten low-level file(s) for semantic equivalence.

2. The process of claim 1, wherein the comparing step comprises distinguishing composite metadata entities from self-contained metadata entities.

3. The process of claim 2, wherein the comparing step comprises testing for bitwise equality of a self-contained metadata entity of the initial low-level file(s) and a matching self-contained metadata entity of the rewritten low-level file(s).

4. The process of claim 1, wherein the comparing step comprises at least one of the following:

testing for equality between flag(s) of a metadata entity of the initial low-level file(s) and flag(s) of a matching metadata entity of the rewritten low-level file(s);

testing for equality between a string of a metadata entity of the initial low-level file(s) and a string of a matching metadata entity of the rewritten low-level file(s);

testing for equality between field(s) of a metadata entity of the initial low-level file(s) and field(s) of a matching metadata entity of the rewritten low-level file(s);

testing for equality between method(s) of a metadata entity of the initial low-level file(s) and method(s) of a matching metadata entity of the rewritten low-level file(s).

5. The process of claim 1, wherein the comparing step comprises comparing a transitive closure of metadata of the initial low-level file(s) with a transitive closure of metadata of the rewritten low-level file(s) for semantic equivalence.

6. The process of claim 1, wherein the initial low-level file(s) contain a metadata entity alpha_initial and a metadata entity beta_initial in that alpha-beta order relative to one another, the generating step places in the rewritten low-level file(s) a metadata entity beta_rewritten and a metadata entity alpha_rewritten in that beta-alpha order relative to one another, and the process further comprises matching alpha_initial with alpha_rewritten and matching beta_initial with beta_rewritten.

7. The process of claim 1, wherein the process further comprises matching a metadata entity alpha_initial in the initial low-level file(s) with a metadata entity alpha_rewritten in the rewritten low-level file(s) after determining that each entity has the same literal ordering of method body instruction(s) and that operand(s), if any, of those corresponding instructions are semantically equivalent.

8. The process of claim 1, wherein the process further comprises matching a metadata entity alpha_initial in the initial low-level file(s) with a metadata entity alpha_rewritten in the rewritten low-level file(s) after determining that one entity is a syntactic variant of the other entity.

9. The process of claim 1, wherein the process further comprises matching a metadata entity alpha_initial in the initial low-level file(s) with a metadata entity alpha_rewritten in the rewritten low-level file(s) after converting each entity into a canonical form.

10. A computer-readable non-transitory storage medium configured with data and with instructions that when executed by at least one processor causes the at least one processor to perform a process for binary rewriter verification, the process comprising the steps of:

obtaining an initial binary file containing code and metadata;

generating a rewritten binary file from the initial binary file by applying the binary rewriter to the initial binary file independently of any binary code transformation;

distinguishing a composite metadata entity in the initial binary file from a self-contained metadata entity in the initial binary file;

comparing a metadata entity alpha_initial in the initial binary file with a metadata entity alpha_rewritten in the rewritten binary file for semantic equivalence after determining that one entity is a syntactic variant of the other entity; and

comparing additional metadata of the initial binary file with additional metadata of the rewritten binary file for semantic equivalence.

11. The configured medium of claim 10, wherein the comparing step comprises at least one of the following:

testing for equality between flags of a metadata entity of the initial binary file and flags of a metadata entity of the rewritten binary file;

testing for equality between a string of a metadata entity of the initial binary file and a string of a metadata entity of the rewritten binary file,

testing for equality between fields of a metadata entity of the initial binary file and fields of a metadata entity of the rewritten binary file;

testing for equality between methods of a metadata entity of the initial binary file and methods of a metadata entity of the rewritten binary file,

testing for bitwise equality of a self-contained metadata entity of the initial binary file and a self-contained metadata entity of the rewritten binary file.

12. The configured medium of claim 10, wherein the comparing step comprises comparing a transitive closure of metadata of the initial binary file with a transitive closure of metadata of the rewritten binary file for semantic equivalence.

13. The configured medium of claim 10, wherein the initial binary file contains a metadata entity alpha_initial and a metadata entity beta_initial in that alpha-beta order relative to one another, the generating step places in the rewritten binary file a metadata entity beta_rewritten and a metadata entity alpha_rewritten in that beta-alpha order relative to one another, and the process comprises comparing alpha_initial with alpha_rewritten for semantic equivalence and comparing beta_initial with beta_rewritten for semantic equivalence.

14. The configured medium of claim 10, wherein the process comprises comparing a metadata entity alpha_initial in the initial binary file with a metadata entity alpha_rewritten in the rewritten binary file for semantic equivalence after determining that each entity has the same literal ordering of method body instructions and that the operands of instructions (if any) are semantically equivalent.

15. The configured medium of claim 10, wherein the process further comprises converting at least one metadata entity in at least one of the binary files into a canonical form.

16. A computer system comprising:

a logical processor;

a memory in operable communication with the logical processor;

an initial binary file residing in the memory and containing code and metadata;

a binary rewriter verification tool residing in the memory and having a metadata semantic equivalence tester;

at least one of;

a binary rewriter residing in the memory;

a rewritten binary file residing in the memory;

and

a determination produced by the binary rewriter verification tool as to metadata semantic equivalence of the initial binary file and at least one of;

the rewritten binary file, a file produced using the binary rewriter.

17. The system of claim 16, further comprising a transitive closure of metadata of the initial binary file, the transitive closure residing in the memory.

18. The system of claim 16, further comprising a structural mapping between a metadata entity alpha_initial in the initial binary file and a metadata entity alpha_rewritten in the rewritten binary file, wherein each entity has the same literal ordering of method body instructions and wherein operands of corresponding instructions of entities are semantically equivalent.

19. The system of claim 16, further comprising a structural mapping between a metadata entity alpha_initial in the initial binary file and a metadata entity alpha_rewritten in the rewritten binary file, wherein one entity is a syntactic variant of the other entity.

20. The system of claim 16, further comprising a structural mapping between a canonical form of a metadata entity alpha_initial in the initial binary file and a canonical form of a metadata entity alpha_rewritten in the rewritten binary file.