C反编译控制流恢复的形式描述及算法

反编译是软件逆向工程的重要组成部分。控制流恢复是Ｃ反编译的重要组成部分。本文首先描述了验证反编译结果与原程序功能等价的模型；其次从数学角度提出了Ｃ编译和反编译控制结构的数学模型并给出其性质；再次根据对Ｃ控制语句编译结果的分析，以扩展的ＢＮＦ形式描述了Ｃ控制语句反编译的约束属性方法；最后给出并说明了反编译控制流恢复的算法及其运行示例。

FORMAL DESCRIPTION AND ALGORITHM OF THE RECOVERY OF CONTROL FLOW IN C DECOMPILER

Decompilation is an important component of software reverse engineer-ing. Control flow recovery is a significant part of C decompilation. In this paper,first,a model to verify the functional equivalence of a decompiler's result to its orig-inal low-level input is described; second,mathematical models and their characteris-tics of control structures in C compilation and decompilation are constructed respec-tively and explained from the point of view of mathematics(compilation is basicallya many-to-one mapping but can be transferred into a surjection, decompilation is arelation in nature but can be converted into an one-to-one mapping by constraints,so there exists a deterministic algorithm on control flow decompilation); third, theconstrained attribute grammar of C executive instructions is introduced in the formof expanded BNF (traditional BNF with attributes attaching to some terminatorsand constraints attaching to each production) according to the analysis of the com-pilation results of C control statements (directed by this grammar, one can definite-ly induce the control structures of binary files with the model of push-down ma-chine, this is a process somewhat like pattern matching); finally, a recovery algo-rithm on C control flow decompilation and an example of its result are presented. Itis proved by practice that the algorithm presented here is right and robust. It alsohas hlgh speed. There is still many things worthwhile dealing with, such as conv-erting some While statements to For statements to be more fit for the C languageprogramming style, and so on. So, a post processing system can be attached to thesystem.