|
|
| 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.
| |
