Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

Type-Based Verification of Assembly Language

Bor-Yuh Evan Chang

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2008-186
December 29, 2008

http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-186.pdf

It is a common belief that certifying compilation, which typically verifies the well-typedness of compiler output, can be an effective mechanism for compiler debugging, in addition to ensuring basic safety properties. Bytecode verification is a fairly simple example of this approach and derives its simplicity in part by compiling to carefully crafted high-level bytecodes. In this paper, we seek to push this method to native assembly code, while maintaining much of the simplicity of bytecode verification. Furthermore, we wish to provide experimental confirmation that such a tool can be accessible and effective for compiler debugging. To achieve these goals, we present a type-based data-flow analysis or abstract interpretation for assembly code compiled from a Java-like language, and evaluate its bug-finding efficacy on a large set of student compilers.

Advisor: George Necula


BibTeX citation:

@mastersthesis{Chang:EECS-2008-186,
    Author = {Chang, Bor-Yuh Evan},
    Title = {Type-Based Verification of Assembly Language},
    School = {EECS Department, University of California, Berkeley},
    Year = {2008},
    Month = {Dec},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-186.html},
    Number = {UCB/EECS-2008-186},
    Abstract = {It is a common belief that certifying compilation, which typically verifies the well-typedness of compiler output, can be an effective mechanism for compiler debugging, in addition to ensuring basic safety properties.  Bytecode verification is a fairly simple example of this approach and derives its simplicity in part by compiling to carefully crafted high-level bytecodes.  In this paper, we seek to push this method to native assembly code, while maintaining much of the simplicity of bytecode verification.  Furthermore, we wish to provide experimental confirmation that such a tool can be accessible and effective for compiler debugging.  To achieve these goals, we present a type-based data-flow analysis or abstract interpretation for assembly code compiled from a Java-like language, and evaluate its bug-finding efficacy on a large set of student compilers.}
}

EndNote citation:

%0 Thesis
%A Chang, Bor-Yuh Evan
%T Type-Based Verification of Assembly Language
%I EECS Department, University of California, Berkeley
%D 2008
%8 December 29
%@ UCB/EECS-2008-186
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-186.html
%F Chang:EECS-2008-186