CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016
Tue 19 Jan 2016 16:00 - 16:30 at Room St Petersburg II - Session 8: Compiler Verification

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 paper, we formally verify 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.

Tue 19 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

16:00 - 17:00
Session 8: Compiler VerificationCPP at Room St Petersburg II
Formal Verification of Control-flow Graph Flattening
Sandrine Blazy IRISA / University of Rennes 1, Alix Trieu ENS Rennes
Axiomatic Semantics for Compiler Verification
Steven Schäfer , Sigurd Schneider Saarland University, Gert Smolka Saarland University