Typing a multi-language intermediate code

ABSTRACT

The Microsoft .NET Framework is a new computing architecture designed to support a variety of distributed applications and web-based services. .NET software components are typically distributed in an object-oriented intermediate language, Microsoft IL, executed by the Microsoft Common Language Runtime. To allow convenient multi-language working, IL supports a wide variety of high-level language constructs, including class-based objects, inheritance, garbage collection, and a security mechanism based on type safe execution.This paper precisely describes the type system for a substantial fragment of IL that includes several novel features: certain objects may be allocated either on the heap or on the stack; those on the stack may be boxed onto the heap, and those on the heap may be unboxed onto the stack; methods may receive arguments and return results via typed pointers, which can reference both the stack and the heap, including the interiors of objects on the heap. We present a formal semantics for the fragment. Our typing rules determine well-typed IL instruction sequences that can be assembled and executed. Of particular interest are rules to ensure no pointer into the stack outlives its target. Our main theorem asserts type safety, that well-typed programs in our IL fragment do not lead to untrapped execution errors.Our main theorem does not directly apply to the product. Still, the formal system of this paper is an abstraction of informal and executable specifications we wrote for the full product during its development. Our informal specification became the basis of the product team's working specification of type-checking. The process of writing this specification, deploying the executable specification as a test oracle, and applying theorem proving techniques, helped us identify several security critical bugs during development.

REFERENCES

• AC96: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• ASU86: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• Car97: L. Cardelli. Type systems. In A.B. Tucker, editor, The Computer Science and Engineering Handbook, chapter 103, pages 2208-2236. CRC Press, 1997.
• Coh89: A. Cohn, The notion of proof in hardware verification, Journal of Automated Reasoning, v.5 n.2, p.127-139, June 1989
• DE97: S. Drossopoulou and S. Eisenbach. Java is type safe-probably. In Proceedings ECOOP'97, June 1997.
• FKR+00: Robert Fitzgerald , Todd B. Knoblock , Erik Ruf , Bjarne Steensgaard , David Tarditi, Marmot: an optimizing compiler for Java, Software—Practice & Experience, v.30 n.3, p.199-232, Mar.1.2000 [doi>10.1002/(SICI)1097-024X(200003)30:3<199::AID-SPE296>3.0.CO;2-2]
• FM00: Stephen N. Freund , John C. Mitchell, The type system for object initialization in the Java bytecode language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.6, p.1196-1250, Nov. 1999 [doi>10.1145/330643.330646]
• GHL99: Andrew D. Gordon , Paul D. Hankin , Søren B. Lassen, Compilation and equivalence of imperative objects, Journal of Functional Programming, v.9 n.4, p.373-426, July 1999 [doi>10.1017/S0956796899003482]
• GS00: A.D. Gordon and D. Syme. Typing a multilanguage intermediate code. Technical Report MSR-TR-2000-106, Microsoft Research, 2000.
• HW00: A. Hejlsberg and S. Wiltamuth. C# Language Reference. Available at http:/ /msdn.microsoft.com/vstudio/nextgen/ technology/csharpintro.asp, 2000.
• IPW99: Atshushi Igarashi , Benjamin Pierce , Philip Wadler, Featherwieght Java: a minimal core calculus for Java and GJ, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.132-146, November 01-05, 1999, Denver, Colorado, United States
• Jon99: M.P. Jones. Typing Haskell in Haskell. In Proceedings Haskell Workshop, Paris, 1999. Available at http://www.cse.ogi.edu/~mpj/thih.
• Ler92: Xavier Leroy, Unboxed objects and polymorphic typing, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.177-188, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143205]
• MCGW98: J. Gregory Morrisett , Karl Crary , Neal Glew , David Walker, Stack-Based Typed Assembly Language, Proceedings of the Second International Workshop on Types in Compilation, p.28-52, March 25-27, 1998
• Mic00: Microsoft Corporation. Microsoft IL Assembly Programmer's Reference Manual, July 2000. Part of the NET Framework Software Development Kit, distributed on CD at the Microsoft Professional Developers Conference, Orlando, Florida, July 11-14, 2000.
• MTHM97: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• MWCG99: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• Nec97: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• Nor98: M. Norrish. C formalised in HOL. PhD thesis, University of Cambridge, 1998.
• PG92: Young Gil Park , Benjamin Goldberg, Escape analysis on lists, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.116-127, June 15-19, 1992, San Francisco, California, United States
• PHH+93: S. Peyton Jones, C. Hall, K. Hammond, W. Partain, and P. Wadler. The Glasgow Haskell compiler: a technical overview. In Proceedings UK Joint Framework for Information Technology (JFIT) Technical Conference, pages 249-257. 1993.
• PL91: Simon L. Peyton Jones , John Launchbury, Unboxed values as first class citizens in a non-strict functional language, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.636-666, June 1991, Cambridge, Massachusetts, United States
• PW92: S. Peyton Jones and P. Wadler. A static semantics for Haskell. Unpublished draft, Department of Computing Science, University of Glasgow. Available at http:// research.microsoft.com/users/simonpj, 1992.
• Qia99: Zhenyu Qian, A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and Subrountines, Formal Syntax and Semantics of Java, p.271-312, January 1999
• SA98: Raymie Stata , Martín Abadi, A type system for Java bytecode subroutines, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.149-160, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268959]
• Sha97: Z. Shao. An overview of the FLINT/ML compiler. In Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation (TIC'97), Amsterdam, The Netherlands, June 1997.
• Sym98: D. Syme. Declarative Theorem Proving for Operational Semantics. PhD thesis, University of Cambridge, 1998.
• Sym99: Don Syme, Proving Java Type Soundness, Formal Syntax and Semantics of Java, p.83-118, January 1999
• TMC+96: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• TT97: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]
• Van96: Myra Ellen Vaninwegen , Carl Gunter, The machine-assisted proof of programming language properties, 1996
• vN99: David von Oheimb , Tobias Nipkow, Machine-Checking the Java Specification: Proving Type-Safety, Formal Syntax and Semantics of Java, p.119-156, January 1999
• Yel99: Phillip M. Yelland, A compositional account of the Java virtual machine, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.57-69, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292548]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Design, Languages, Performance, Theory, Verification