Towards a formally verified obfuscating compiler

Sandrine Blazy 1 Roberto Giacobazzi 2
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper extends the idea of specializing modified interpreters for systematically generating obfuscated code. By using the Coq proof assistant we specify some elementary obfuscations and prove that the resulting distorted interpreter is correct, namely it preserves the intended semantics of programs. The paper shows how the semantic preservation proofs generated and verified in Coq can provide a measure of the quality of the obfuscation. In particular we can observe that there is a precise corresponding between the potency of the obfuscation and the complexity of the proof of semantics preservation. Our obfuscation can be easily integrated into the CompCert C compiler, providing the basis for a formally verified obfuscating compiler which can be applied to any C program.
Type de document :
Communication dans un congrès
Christian Collberg. SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop, Jun 2012, Beijing, China. ACM SIGPLAN, 2012
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00762330
Contributeur : Sandrine Blazy <>
Soumis le : samedi 8 décembre 2012 - 06:51:24
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : samedi 17 décembre 2016 - 22:00:15

Fichier

paper-ieee.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00762330, version 1

Citation

Sandrine Blazy, Roberto Giacobazzi. Towards a formally verified obfuscating compiler. Christian Collberg. SSP 2012 - 2nd ACM SIGPLAN Software Security and Protection Workshop, Jun 2012, Beijing, China. ACM SIGPLAN, 2012. 〈hal-00762330〉

Partager

Métriques

Consultations de la notice

570

Téléchargements de fichiers

166