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
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
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 article.
Keywords : Coq Proof Assistant Abstract Interpretation Low-level programming language
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2016, 56 (3), pp.26. 〈10.1007/s10817-015-9359-8〉
Liste complète des métadonnées

Littérature citée [32 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01243700
Contributeur : Sandrine Blazy <>
Soumis le : vendredi 27 mai 2016 - 11:26:05
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : dimanche 28 août 2016 - 10:24:08

Fichier

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

Identifiants

Collections

INRIA | IRISA | UR1-UFR-ISTIC | CENTRALESUPELEC | ENS-RENNES | UNIV-RENNES

Citation

Sandrine Blazy, Vincent Laporte, David Pichardie. Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. Journal of Automated Reasoning, Springer Verlag, 2016, 56 (3), pp.26. 〈10.1007/s10817-015-9359-8〉. 〈hal-01243700〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

1058

Téléchargements de fichiers

164

Contact


archive-ouverte@inria.fr