On Friday October 17, this site was moved to a new server, https://mw.hh.se. The original address will continue to work. Whithin a week or two this site will return to the original address. /Peo HH IT-dep

WG211/M15Brady: Difference between revisions

From WG 2.11
Jump to navigationJump to search
VisualWikitext
Sandrine (talk | contribs)
41 edits
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..."
 
Sandrine (talk | contribs)
41 edits
Blanked the page
 
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.

Latest revision as of 23:05, 25 October 2015

Retrieved from "http://mw.hh.se/wg211/index.php?title=WG211/M15Brady&oldid=1318"