MCDASH: Refinement-Based Property Verification for Machine Code
File(s)
Date
2009Author
Lal, Akash
Lim, Junghee
Reps, Thomas
Publisher
University of Wisconsin-Madison Department of Computer Sciences
Metadata
Show full item recordAbstract
This paper presents MCDASH, a refinement-based model checker for
machine code. While model checkers such as SLAM, BLAST, and DASH have
each made significant contributions in the field of
verification/flaw-detection, their use has been restricted to programs
for which source code is available. This paper discusses several
challenges that arise when working with machine code, and explains how
they are addressed in MCDASH. Unlike previous model checkers, MCDASH
does not require the usual preprocessing steps of (a) building
control-flow graphs, and (b) performing points-to analysis (or alias
analysis); nor does MCDASH require type information to be supplied.
The paper also describes how we extended MCDASH to check properties of
self-modifying code.
MCDASH is built using language-independent meta-tools that generate
the implementations of the required analysis components from
descriptions of an instruction set's syntax and semantics. It has
been instantiated for Intel x86 and PowerPC.
Permanent Link
http://digital.library.wisc.edu/1793/60682Citation
TR1659