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

Download the whole development

Browse the Source

Static Analyzer

• Main.v: Main theorems
• Goto.v: Programming language syntax
• GotoSem.v: Semantics
• AbGoto.v: Abstract memory
• GotoAnalysis.v: Abstract semantics
• FirstGotoAnalysis.v: Interface for OCaml

Numeric Domains

• AbMachineNonrel.v: Signature of numeric domains
• Intervals.v: Intervals of machine integers
• IntervalDomain.v: Intervals of machine integers
• IntSet.v: Finite sets of machine integers
• IntSetDom.v: Finite sets of machine integers
• StridedIntervals.v: Strided intervals of machine integers
• CompleteLattice.v
• LatticeSignatures.v
• AdomLib.v

More Libraries

• aritmo.v: Arithmetic
• Integers.v: Machine integers
• AbCfg.v: Generate CFG
• AbCfg2.v: Generate unrolled CFG
• DebugAbMachineNonrel.v
• DebugMemDom.v
• Errors.v
• Coqlib.v
• Maps.v
• TreeAl.v
• ToString.v
• PrintPos.v
• GotoString.v
• DebugMemDom.v
• DLib.v
• Util.v

Sample programs

• First example
• Multilevel runtime code generation
• Array bounds check
• Opcode modification
• Code obfuscation
• Code checking
• Polymorphic code
• Control-flow modification
• Mutual modification
• Code encryption
• Fibonacci
• Vector dot product