MCDASH: Refinement Based Property Verification for Machine Code

Abstract

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 sets syntax and semantics. It has been instantiated for Intel x86 and PowerPC.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 2009
Accession Number
AD1006569

Entities

People

  • Akash Lal
  • Junghee Lim
  • Thomas Reps

Organizations

  • University of Wisconsin–Madison

Tags

Communities of Interest

  • C4I
  • Cyber

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Coding
  • Compilers
  • Computer Programming
  • Computer Programs
  • Computers
  • Debugging
  • Decoding
  • Instruction Set Architecture
  • Language
  • Machine Languages
  • Programming Languages
  • Software Development
  • Space Exploration
  • Specifications
  • Standards

Fields of Study

  • Computer science

Readers

  • Computer Programming and Software Development.
  • Database Systems and Applications