摘要： 花指令模糊变换是代码模糊变换策略中的一种有效方法。在分析现有花指令加密方法的基础上，给出一种随机花指令模糊变换加密方案，并利用形式化方法对其进行了描述。通过研究花指令模糊变换各种形式化的定义，推导出若干引理，从“JMP扩展”、“JMC变换”、“JMP后添加花指令”等3个方面形式化地证明了经上述随机花指令加密算法变换的程序具有与原始程序相同的逻辑性。

关键词: 代码模糊变换, 逻辑一致性, 花指令, 反汇编

Abstract: Junk code transformation is one of effective approach of the code obfuscation technology. Based on the analysis of current junk code strategies, this paper presents a new method named stochastic junk code encryption algorithm, and depicts the algorithm with formal language. The paper studies how to prove the logic invariability of junk code transformation with formalization method. After studying the formal definition of junk code transformation, some lemmas are educed. With these lemmas, and from three aspects such as “JMP Expand”, “JMC Switch” and “Junk Code”, the paper proves that the program which transforms with stochastic junk code algorithm has the same logicality with the original program.

Key words: Code obfuscating transformation, Logic invariability, Junk code, Disassemble