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 article.
Keywords : Coq Proof Assistant Abstract Interpretation Low-level programming language
Document type :
Journal articles
Complete list of metadatas

Cited literature [32 references]  Display  Hide  Download
https://hal.inria.fr/hal-01243700
Contributor : Sandrine Blazy <>
Submitted on : Friday, May 27, 2016 - 11:26:05 AM
Last modification on : Thursday, February 7, 2019 - 5:25:03 PM
Long-term archiving on : Sunday, August 28, 2016 - 10:24:08 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

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

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

1472

Files downloads

495

Contact


archive-ouverte@inria.fr