| 摘要 |
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.
|
