Code obfuscation is emerging as a key asset in security by obscurity. It aims at hiding sensitive information in programs so that they become more difficult to understand and reverse engineer. Since the results on the impossibility of perfect and universal obfuscation, many obfuscation techniques have been proposed in the literature, ranging from simple variable encoding to hiding the control-flow of a program.
In this paper, we formally verify in Coq an advanced code obfuscation called control-flow graph flattening, that is used in state-of-the-art program obfuscators. Our control-flow graph flattening is a program transformation operating over C programs, that is integrated into the CompCert formally verified compiler. The semantics preservation proof of our program obfuscator relies on a simulation proof performed on a realistic language, the Clight language of CompCert. The automatic extraction of our program obfuscator into OCaml yields a program with competitive results.
This work has been submitted to CPP 2016. A draft of the paper can be found here.
The development has been made with Coq 8.4pl6 and OCaml 4.02.2, it should work with OCaml 4.0X and Coq 8.4plY. The sources are available here.
Note: the sources contain a modified version of CompCert 2.5.
tar -xvf CompCert-2.5-obf.tar.gz../configure then make all to:ccomp executable.Note: the first step (verifying the proofs) is CPU-intensive and may take several minutes to complete.
make clightgen to install clightgen.ccomp file.c will compile an obfuscated version of file.c.clightgen -dclight file.c will output an obfuscated C version of file.c in file.light.c.The documentation gives a commented listing of the Coq specifications and proofs for the main development files. Proof scripts are folded by default, but can be viewed by clicking on "Proof".
Control-Flow Graph Flattening:
Unseq pass which removes some skip statements: