Formal Verification of Control-flow Graph Flattening

International audienceCode obfuscation is emerging as a key asset in security by obscurity.It aims at hiding sensitive information in programs so that theybecome more difficult to understand and reverse engineer. Since theresults 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 ofa program.In this paper, we formally verify in Coq an advanced code obfuscationcalled control-flow graph flattening, that is used in stateof-the-artprogram obfuscators. Our control-flow graph flatteningis a program transformation operating over C programs, that is integratedinto the CompCert formally verified compiler. The semanticspreservation proof of our program obfuscator relies on a simulationproof performed on a realistic language, the Clight languageof CompCert. The automatic extraction of our program obfuscatorinto OCaml yields a program with competitive results