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.