|
|
| Line 1: |
Line 1: |
| 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 talk, I will explain how we formally verified 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.
| |
