Advertisement

Proof-Directed De-compilation of Low-Level Code

  • Shin-ya Katsumata
  • Atsushi Ohori
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)

Abstract

We present a proof theoretical method for de-compiling low-level code to the typed lambda calculus. We first define a proof system for a low-level code language based on the idea of Curry-Howard isomorphism. This allows us to regard an executable code as a proof in intuitionistic propositional logic. As being a proof of intuitionistic logic, it can be translated to an equivalent proof of natural deduction proof system. This property yields an algorithm to translate a given code into a lambda term. Moreover, the resulting lambda term is not a trivial encoding of a sequence of primitive instructions, but reflects the behavior of the given program. This process therefore serves as proof-directed decompilation of a low-level code language to a high-level language. We carry out this development for a subset of Java Virtual Machine instructions including most of its features such as jumps, object creation and method invocation. The proof-directed de-compilation algorithm has been implemented, which demonstrates the feasibility of our approach.

References

  1. 1.
    S. Freund and J. Mitchell. A type system for object initialization in the Java byte code language. In Proc. OOPSLA’98, pages 310–328, 1998.Google Scholar
  2. 2.
    J. Gallier. Constructive logics part I: A tutorial on proof systems and typed λ-calculi. Theoretical Computer Science 110, pages 249–339, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.Google Scholar
  4. 4.
    T. Lindholm and F. Yellin. The Java virtual machine specification. AddisonWesley, 2nd edition, 1999.Google Scholar
  5. 5.
    J. Meyer and T. Downing. Java Virtual Machine. O’Reilly, 1997.Google Scholar
  6. 6.
    G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based typed assembly language. In Proc. Types in Compilation, LNCS 1473, pages 28–52, 1998.CrossRefGoogle Scholar
  7. 7.
    G. Morrisett, D. Walker, K. Crary, and N. Glew. From system F to typed assembly language. In Proc. POPL’98, pages 85–97, 1998.Google Scholar
  8. 8.
    G. Necula. Proof-carrying code. In Proc. POPL’98, pages 106–119, 1998.Google Scholar
  9. 9.
    R. O’Callahan. A simple, comprehensive type system for Java bytecode subroutines. In Proc. POPL’99, pages 70–78, 1999.Google Scholar
  10. 10.
    A. Ohori. A Curry-Howard isomorphism for compilation and program execution. In Proc. TLCA’99, LNCS 1581, pages 280–294, 1999.Google Scholar
  11. 11.
    A. Ohori. The logical abstract machine: a Curry-Howard isomorphism for machine code. In Proc. FLOPS’99, LNCS 1722, pages 300–318,1999.Google Scholar
  12. 12.
    C. Raffalli. Machine deduction. In Proc. Types for Proofs and Program, LNCS 806, pages 333–351, 1994.Google Scholar
  13. 13.
    R. Stata and M. Abadi. A type system for Java bytecode subroutines. In Proc. POPL’98, pages 149–160, 1998.Google Scholar
  14. 14.
    Proceedings of Working Conference on Reverse Engineering. IEEE Computer Society Press, 1993-.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Shin-ya Katsumata
    • 1
  • Atsushi Ohori
    • 2
  1. 1.Laboratory for Foundations of Computer ScienceUniversity of EdinburghEdinburghUK
  2. 2.Japan Advanced Institute of Science and TechnologyIshikawaJAPAN

Personalised recommendations