Verified abstract interpretation techniques for disassembling low-level self-modifying code

DOI10.1007/S10817-015-9359-8MaRDI QIDQ287369zbMATH OpenOpenAlexFDO

Authors Sandrine Blazy, Vincent Laporte, David Pichardie

Publication date 26 May 2016

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01243700/file/main.pdf

zbMATH Keywords

abstract interpretationCoqlow-level programming language

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Verified abstract interpretation techniques for disassembling low-level self-modifying code
• scientific article; zbMATH DE number 1953021
• Trace Abstraction-Based Verification for Uninterpreted Programs
• scientific article; zbMATH DE number 1692950
• scientific article; zbMATH DE number 1953018
• scientific article; zbMATH DE number 1696591
• Certified Static Analysis by Abstract Interpretation
• Analyzing Information Flow Properties in Assembly Code by Abstract Interpretation

Cites work

• A certified denotational abstract interpreter
• A formally-verified alias analysis
• Abstract interpretation of annotated commands
• Building certified static analysers by modular construction of well-founded lattices
• Extracting a data flow analyser in constructive logic
• Grammar Analysis and Parsing by Abstract Interpretation
• High-level separation logic for low-level code
• Mechanized semantics for the clight subset of the C language
• Refinement-based CFG reconstruction from unstructured programs
• Structural Abstract Interpretation: A Formal Study Using Coq
• Types for Proofs and Programs
• Types for Proofs and Programs
• Verified heap theorem prover by paramodulation
• Verified just-in-time compiler on x86

Cited in

(7)

• Reachability Analysis of Self Modifying Code
• Bidirectional grammars for machine-code decoding and encoding
• Programming Languages and Systems
• Unveiling metamorphism by abstract interpretation of code properties
• LTL model checking of self modifying code
• Internal models of system F for decompilation
• Verified abstract interpretation techniques for disassembling low-level self-modifying code

Describes a project that uses

Uses Software

• Rocksalt
• VeriStar
• Coq

This page was built for publication: Verified abstract interpretation techniques for disassembling low-level self-modifying code

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q287369)