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.
A part of this work was done while both authors were at RIMS, Kyoto University.
Chapter PDF
Similar content being viewed by others
References
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.
J. Gallier. Constructive logics part I: A tutorial on proof systems and typed λ-calculi. Theoretical Computer Science 110, pages 249–339, 1993.
J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.
T. Lindholm and F. Yellin. The Java virtual machine specification. AddisonWesley, 2nd edition, 1999.
J. Meyer and T. Downing. Java Virtual Machine. O’Reilly, 1997.
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.
G. Morrisett, D. Walker, K. Crary, and N. Glew. From system F to typed assembly language. In Proc. POPL’98, pages 85–97, 1998.
G. Necula. Proof-carrying code. In Proc. POPL’98, pages 106–119, 1998.
R. O’Callahan. A simple, comprehensive type system for Java bytecode subroutines. In Proc. POPL’99, pages 70–78, 1999.
A. Ohori. A Curry-Howard isomorphism for compilation and program execution. In Proc. TLCA’99, LNCS 1581, pages 280–294, 1999.
A. Ohori. The logical abstract machine: a Curry-Howard isomorphism for machine code. In Proc. FLOPS’99, LNCS 1722, pages 300–318,1999.
C. Raffalli. Machine deduction. In Proc. Types for Proofs and Program, LNCS 806, pages 333–351, 1994.
R. Stata and M. Abadi. A type system for Java bytecode subroutines. In Proc. POPL’98, pages 149–160, 1998.
Proceedings of Working Conference on Reverse Engineering. IEEE Computer Society Press, 1993-.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Katsumata, Sy., Ohori, A. (2001). Proof-Directed De-compilation of Low-Level Code. In: Sands, D. (eds) Programming Languages and Systems. ESOP 2001. Lecture Notes in Computer Science, vol 2028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45309-1_23
Download citation
DOI: https://doi.org/10.1007/3-540-45309-1_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41862-7
Online ISBN: 978-3-540-45309-3
eBook Packages: Springer Book Archive