Sandrine: Created page with "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 rev..."

2015-10-25T21:05:50Z

Created page with "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 rev..."

New page

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.

WG211/M15Blazy - Revision history

Sandrine: Created page with "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 rev..."