*banner
 

Using Dependent Types to Certify the Safety of Assembly Code
Matthew Harren, George Necula

Citation
Matthew Harren, George Necula. "Using Dependent Types to Certify the Safety of Assembly Code". Static Analysis Symposium (SAS), Springer-Verlag LNCS, 155-170, September, 2005; Available at http://www.cs.berkeley.edu/~matth/papers/sas05.pdf.

Abstract
There are many source-level analyses or instrumentation tools that enforce various safety properties. In this paper we present an infrastructure that can be used to check independently that the assembly output of such tools has the desired safety properties. By working at assembly level we avoid the complications with unavailability of source code, with source-level parsing, and we certify the code that is actually deployed. The novel feature of the framework is an extensible dependently-typed framework that supports type inference and mutation of dependent values in memory. The type system can be extended with new types as needed for the source-level tool that is certified. Using these dependent types, we are able to express the invariants enforced by CCured, a source-level instrumentation tool that guarantees type safety in legacy C programs. We can therefore check that the x86 assembly code resulting from compilation with CCured is in fact type-safe.

Electronic downloads


(No downloads are available for this publication.)
Citation formats  
  • HTML
    Matthew Harren, George Necula. <a
    href="http://chess.eecs.berkeley.edu/pubs/42.html"
    >Using Dependent Types to Certify the Safety of Assembly
    Code</a>, Static Analysis Symposium (SAS),
    Springer-Verlag LNCS, 155-170, September, 2005; Available at
    http://www.cs.berkeley.edu/~matth/papers/sas05.pdf.
  • Plain text
    Matthew Harren, George Necula. "Using Dependent Types
    to Certify the Safety of Assembly Code". Static
    Analysis Symposium (SAS), Springer-Verlag LNCS, 155-170,
    September, 2005; Available at
    http://www.cs.berkeley.edu/~matth/papers/sas05.pdf.
  • BibTeX
    @inproceedings{HarrenNecula05_UsingDependentTypesToCertifySafetyOfAssemblyCode,
        author = {Matthew Harren and George Necula},
        title = {Using Dependent Types to Certify the Safety of
                  Assembly Code},
        booktitle = {Static Analysis Symposium (SAS)},
        organization = {Springer-Verlag LNCS},
        pages = {155-170},
        month = {September},
        year = {2005},
        note = {Available at
                  http://www.cs.berkeley.edu/~matth/papers/sas05.pdf},
        abstract = {There are many source-level analyses or
                  instrumentation tools that enforce various safety
                  properties. In this paper we present an
                  infrastructure that can be used to check
                  independently that the assembly output of such
                  tools has the desired safety properties. By
                  working at assembly level we avoid the
                  complications with unavailability of source code,
                  with source-level parsing, and we certify the code
                  that is actually deployed. The novel feature of
                  the framework is an extensible dependently-typed
                  framework that supports type inference and
                  mutation of dependent values in memory. The type
                  system can be extended with new types as needed
                  for the source-level tool that is certified. Using
                  these dependent types, we are able to express the
                  invariants enforced by CCured, a source-level
                  instrumentation tool that guarantees type safety
                  in legacy C programs. We can therefore check that
                  the x86 assembly code resulting from compilation
                  with CCured is in fact type-safe.},
        URL = {http://chess.eecs.berkeley.edu/pubs/42.html}
    }
    

Posted by Matthew Harren on 3 May 2006.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess