This page references the Coq developments related to my Ph.D., “Verification of static analyzes for low-level languages”.

Preliminary version of the manuscript

Abstract-Interpretation-Based Static Analysis with Coq

Coq source

CFG analyzer

Depends on CompCert 1.11 ported to Coq 8.4 with the additional CFG intermediate language.

Source code of the CFG analyzer

Self-modifying programs

Source code of the GOTO★ analyzer

Sample analyzed programs:

• Introductory example
• Multi-level run-time code generation
• Opcode modification
• Code obfuscation
• Code checking
• Array bound check
• Polymorphic program
• Control-flow modification
• Mutual modification
• Code encryption
• Fibonacci sequence
• Vector dot product. Variant without the optimization, that can be analyzed even if the input vector is unknown.
• Not-a-branch
• Flattened program
• Flattened Fibonacci
• Overlapping instructions
• Nested instructions

Memory domain

The source code relevant to this chapter is part of the CFG analyzer above. The relevant files are PointsTo.v (type and points-to domain), Nconvert.v (numerical conversion), FMem.v (intermediate specification of the concrete memory), and MemCFG.v (abstract memory domain) in the vanalysis directory.

Verasco C♯minor analyzer

Please refer to the Verasco analyzer homepage.