Abstract: Junk code transformation is an effective approach for the code obfuscation. Based on the analysis of current junk code strategies,the paper proposed a novel junk code encryption algorithm within sub-function and described the algorithm using formal language. With formalization method, the paper researched how to prove the logic consistency of junk code transformation within sub-function. We deduced some important lemmas after researching the formal definilion of junk code transformation within sub-function. With these lemmas, the paper proven from three aspects ("XOR and CMP Expand","Pseudo Embranchment Construction" and "Junk Code after JNE") that the program transformed by junk code algorithm within sub-function has the same logicality with its original one. At last, with the standard of the codcobfuscation's judgment,the paper gave the result of the algorithm in detailed analyzing.

Key words: Code obfuscation,Logic consistency,Junk code,Disassemble