Formal Verification of Control-flow Graph Flattening

Sandrine Blazy 1 Alix Trieu 2
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : 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 stateof-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.
Type de document :
Communication dans un congrès
ACM. Certified Proofs and Programs (CPP 2016), Jan 2016, Saint-Petersburg, United States. pp.12, 2016, Certified Proofs and Programs (CPP 2016). 〈https://people.csail.mit.edu/adamc/cpp16/index.html〉. 〈10.1145/2854065.2854082〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01242063
Contributeur : Sandrine Blazy <>
Soumis le : vendredi 27 mai 2016 - 11:29:50
Dernière modification le : mercredi 16 mai 2018 - 11:23:28

Fichier

cpp2016.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Sandrine Blazy, Alix Trieu. Formal Verification of Control-flow Graph Flattening. ACM. Certified Proofs and Programs (CPP 2016), Jan 2016, Saint-Petersburg, United States. pp.12, 2016, Certified Proofs and Programs (CPP 2016). 〈https://people.csail.mit.edu/adamc/cpp16/index.html〉. 〈10.1145/2854065.2854082〉. 〈hal-01242063〉

Partager

Métriques

Consultations de la notice

558

Téléchargements de fichiers

126