| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code
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.
Cited literature [17 references]
https://hal.inria.fr/hal-01102445
Contributor : David Pichardie <>
Submitted on : Monday, January 12, 2015 - 5:12:05 PM
Last modification on : Friday, June 11, 2021 - 3:34:04 AM
Long-term archiving on: : Monday, April 13, 2015 - 11:10:22 AM
Contributor : David Pichardie <>
Submitted on : Monday, January 12, 2015 - 5:12:05 PM
Last modification on : Friday, June 11, 2021 - 3:34:04 AM
Long-term archiving on: : Monday, April 13, 2015 - 11:10:22 AM
File
itp14.pdf
Files produced by the author(s)