Abstract
Popular mobile code architectures (Java and .NET) include verifiers to check for memory safety and other security properties. Since their formats are relatively high level, supporting a wide range of source language features is awkward. Further compilation and optimization, necessary for efficiency, must be trusted. We describe the design and implementation of a fully type-preserving compiler for Java and ML. Its strongly-typed intermediate language provides a low-level abstract machine model and a type system general enough to prove the safety of a variety of implementation techniques. We show that precise type preservation is within reach for real-world Java systems.
This work was sponsored in part by the Defense Advanced Research Projects Agency ISO under the title “Scaling Proof-Carrying Code to Production Compilers and Security Policies,” ARPA Order No. H559, issued under Contract No. F30602-99- 1-0519, and in part by NSF Grants CCR-9901011 and CCR-0081590. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the U.S. Government. Java is a registered trademark of Sun Microsystems, Inc. in the U.S. and other countries. CaffeineMark is a trademark of Pendragon Software.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. 2nd edn. Addison-Wesley (1999)
ECMA: Common language infrastructure. Drafts of the TC39/TG3 standardization process. http://msdn.microsoft.com/net/ecma/ (2001)
Tolksdorf, R.: Programming languages for the JVM. http://flp.cs.tu-berlin.de/~tolk/vmlanguages.html (2002)
Syme, D.: ILX: extending the.NET Common IL for functional language interoperability. In: Proc. BABEL Workshop on Multi-Language Infrastructure and Interoperability, ACM (2001)
Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Trans. on Programming Languages and Systems 21 (1999)
Necula, G. C.: Proof-carrying code. In: Proc. Symp. on Principles of Programming Languages, Paris, ACM (1997) 106–119
Fitzgerald, R., Knoblock, T. B., Ruf, E., Steensgaard, B., Tarditi, D.: Marmot: an optimizing compiler for Java. Software: Practice and Experience 30 (2000)
Stichnoth, J. M., Lueh, G. Y., Cierniak, M.: Support for garbage collection at every instruction in a Java compiler. In: Proc. Conf. on Programming Language Design and Implementation, Atlanta, ACM (1999) 118–127
League, C., Shao, Z., Trifonov, V.: Representing Java classes in a typed intermediate language. In: Proc. Int’l Conf. Functional Programming, Paris, ACM (1999)
League, C., Shao, Z., Trifonov, V.: Type-preserving compilation of Featherweight Java. ACM Trans. on Programming Languages and Systems 24 (2002)
Bruce, K. B., Cardelli, L., Pierce, B. C.: Comparing object encodings. Information and Computation 155 (1999) 108–133
Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press (1997)
Rémy, D.: Syntactic theories and the algebra of record terms. Technical Report 1869, INRIA (1993)
Colby, C., Lee, P., Necula, G. C., Blau, F., Cline, K., Plesko, M.: A certifying compiler for Java. In: Proc. Conf. on Programming Language Design and Implementation, Vancouver, ACM (2000)
Necula, G. C.: Personal communication (2001)
Schneck, R. R., Necula, G. C.: A gradual approach to a more trustworthy, yet scalable, proof-carrying code. In: Proc. Conf. on Automated Deduction. (2002)
Shao, Z., League, C., Monnier, S.: Implementing typed intermediate languages. In: Proc. Int’l Conf. Functional Programming, Baltimore, ACM (1998) 313–323
Appel, A. W.: SSA is functional programming. ACM SIGPLAN Notices (1998)
Cytron, R., Ferrante, J., Rosen, B. K., Wegman, M. N., Zadeck, F. K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. on Programming Languages and Systems 13 (1991) 451–490
Dean, J., Grove, D., Chambers, C.: Optimization of object-oriented programs using static class hierarchy analysis. In: Proc. European Conf. Object-Oriented Programming. (1995)
League, C., Trifonov, V., Shao, Z.: Functional Java bytecode. In: Proc. 5th World Conf. on Systemics, Cybernetics, and Informatics. (2001) Workshop on Intermediate Representation Engineering for the Java Virtual Machine.
Shao, Z., Saha, B., Trifonov, V., Papaspyrou, N.: A type system for certified binaries. In: Proc. Symp. on Principles of Programming Languages. (2002)
George, L.: Customizable and reusable code generators. Technical report, Bell Labs (1997)
Benton, N., Kennedy, A.: Interlanguage working without tears: Blending ML with Java. In: Proc. Int’l Conf. Functional Programming, Paris, ACM (1999) 126–137
League, C.: A Type-Preserving Compiler Infrastructure. PhD thesis, Yale University (2002)
Canning, P., Cook, W., Hill, W., Oltho., W., Mitchell, J. C.: F-bounded polymorphism for object-oriented programming. In: Proc. Int’l Conf. on Functional Programming and Computer Architecture, ACM (1989) 273–280
Castagna, G., Pierce, B. C.: Decidable bounded quantification. In: Proc. Symp. on Principles of Programming Languages, Portland, ACM (1994)
Barendregt, H.: Typed lambda calculi. In Abramsky, S., Gabbay, D., Maibaum, T., eds.: Handbook of Logic in Computer Science. Volume 2. Oxford (1992)
Mitchell, J. C., Plotkin, G. D.: Abstract types have existential type. ACM Transactions on Programming Languages and Systems 10 (1988) 470–502
Schürmann, C., Yu, D., Ni, Z.: An encoding of F-omega in LF. In: Proc.Workshop on Mechanized Reasoning about Languages with Variable Binding, Siena (2001)
Peyton Jones, S., Ramsey, N., Reig, F.: C—: a portable assembly language that supports garbage collection. In Nadathur, G., ed.: Proc. Conf. on Principles and Practice of Declarative Programming. Springer (1999) 1–28
Bothner, P.: A GCC-based Java implementation. In: Proc. IEEE Compcon. (1997)
Benton, N., Kennedy, A., Russell, G.: Compiling Standard ML to Java bytecodes. In: Proc. Int’l Conf. Functional Programming, Baltimore, ACM (1998) 129–140
Wright, A., Jagannathan, S., Ungureanu, C., Hertzmann, A.: Compiling Java to a typed lambda-calculus: A preliminary report. In: Proc. Int’l Workshop on Types in Compilation. Volume 1473 of LNCS., Berlin, Springer (1998) 1–14
Glew, N.: An efficient class and object encoding. In: Proc. Conf. on Object-Oriented Programming Systems, Languages, and Applications, ACM (2000)
Knoblock, T., Rehof, J.: Type elaboration and subtype completion for Java bytecode. In: Proc. Symp. on Principles of Programming Languages. (2000) 228–242
Gagnon, E., Hendren, L., Marceau, G.: Efficient inference of static types for Java bytecode. In: Proc. Static Analysis Symp. (2000)
Amme, W., Dalton, N., von Ronne, J., Franz, M.: SafeTSA: A type safe and referentially secure mobile-code representation based on static single assignment form. In: Proc. Conf. on Programming Language Design and Implementation, ACM (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
League, C., Shao, Z., Trifonov, V. (2003). Precision in Practice: A Type-Preserving Java Compiler. In: Hedin, G. (eds) Compiler Construction. CC 2003. Lecture Notes in Computer Science, vol 2622. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36579-6_8
Download citation
DOI: https://doi.org/10.1007/3-540-36579-6_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00904-7
Online ISBN: 978-3-540-36579-2
eBook Packages: Springer Book Archive