Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code

Sandrine Blazy 1 Vincent Laporte 1 David Pichardie 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Static analysis of binary code is challenging for several reasons. In particular, standard static analysis techniques operate over control flow graphs, which are not available when dealing with self-modifying programs which can modify their own code at runtime. We formalize in the Coq proof assistant some key abstract interpretation techniques that automatically extract memory safety properties from binary code. Our analyzer is formally proved correct and has been run on several self-modifying challenges, provided by Cai et al. in their PLDI 2007 paper.
Type de document :
Communication dans un congrès
The 5th International Conference on Interactive Theorem Proving (ITP 2014), 2014, Vienna, Austria. Springer, 8558, pp.128 - 143, 2014, LNCS : Interactive Theorem Proving. 〈10.1007/978-3-319-08970-6_9〉
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01102445
Contributeur : David Pichardie <>
Soumis le : lundi 12 janvier 2015 - 17:12:05
Dernière modification le : jeudi 15 novembre 2018 - 11:57:41
Document(s) archivé(s) le : lundi 13 avril 2015 - 11:10:22

Fichier

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

Identifiants

Collections

UNIV-RENNES1 | INRIA | IRISA | IRISA-D4 | INSTITUT-TELECOM | UR1-UFR-ISTIC | ENS-RENNES | UNIV-RENNES

Citation

Sandrine Blazy, Vincent Laporte, David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. The 5th International Conference on Interactive Theorem Proving (ITP 2014), 2014, Vienna, Austria. Springer, 8558, pp.128 - 143, 2014, LNCS : Interactive Theorem Proving. 〈10.1007/978-3-319-08970-6_9〉. 〈hal-01102445〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

1107

Téléchargements de fichiers

159

Contact


archive-ouverte@inria.fr