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

1. AC96.M. Abadi and L. Cardelli. A Theory of Objects. Springer Verlag, 1996.]]
2. ASU86.A.V. Aho, R. Sethi, and J.D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.]]
3. Car97.L. Cardelli. Type systems. In A.B. Tucker, editor, The Computer Science and Engineering Handbook, chapter 103, pages 2208-2236. CRC Press, 1997.]]
4. Coh89.A. Cohn. The notion of proof in hardware verification. Journal of Automated Reasoning, 5(2):127-139, June 1989.]]
5. DE97.S. Drossopoulou and S. Eisenbach. Java is type safe-probably. In Proceedings ECOOP'97, June 1997.]]
6. FKR+00.R. Fitzgerald, T.B. Knoblock, E. Ruf, B. Steensgaard, and D. Tarditi. Marmot: An optimizing compiler for Java. Software: Practice and Experience, 30(3), 2000.]]
7. FM00.S. Freund and J.C. Mitchell. A type system for object initialization in the Java bytecode language. ACM Transactions on Programming Languages and Systems, 2000. To appear.]]
8. GHL99.A.D. Gordon, P.D. Hankin, and S.B. Lassen. Compilation and equivalence of imperative objects. Journal of Functional Programming, 9(4):373-426, 1999.]]
9. GS00.A.D. Gordon and D. Syme. Typing a multilanguage intermediate code. Technical Report MSR-TR-2000-106, Microsoft Research, 2000.]]
10. HW00.A. Hejlsberg and S. Wiltamuth. C# Language Reference. Available at http:/ /msdn.microsoft.com/vstudio/nextgen/ technology/csharpintro.asp, 2000.]]
11. IPW99.A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), October 1999.]]
12. Jon99.M.P. Jones. Typing Haskell in Haskell. In Proceedings Haskell Workshop, Paris, 1999. Available at http://www.cse.ogi.edu/~mpj/thih.]]
13. Ler92.X. Leroy. Unboxed objects and polymorphic typing. In 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 177-188. ACM Press, 1992.]]
14. MCGW98.G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based typed assembly language. In Workshop on Types in Compilation, volume 1473 of Lecture Notes in Computer Science, pages 28-52. Springer Verlag, 1998.]]
15. 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.]]
16. MTHM97.R. Milner, M. Tofte, R. Harper, and D. Mac- Queen. The Definition of Standard ML (Revised). MIT Press, 1997.]]
17. MWCG99.G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):528-569, 1999.]]
18. Nec97.G. Necula. Proof-carrying code. In 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106-119. ACM Press, 1997.]]
19. Nor98.M. Norrish. C formalised in HOL. PhD thesis, University of Cambridge, 1998.]]
20. PG92.Y.G. Park and B. Goldberg. Escape analysis on lists. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 116-127. ACM Press, 1992.]]
21. 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.]]
22. PL91.S. Peyton Jones and J. Launchbury. Unboxed values as first class citizens. In Functional Programming Languages and Computer Architecture, volume 523 of Lecture Notes in Computer Science, pages 636-666. Springer Verlag, 1991.]]
23. 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.]]
24. Qia99.Z. Qian. A formal specification of Java TM virtual machine instructions for objects, methods and subroutines. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1532 of Lecture Notes in Computer Science, pages 271-312. Springer Verlag, 1999.]]
25. SA98.R. Stata and M. Abadi. A type system for Java bytecode subroutines. In Proceedings POPL'98, pages 149-160. ACM Press, 1998.]]
26. 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.]]
27. Sym98.D. Syme. Declarative Theorem Proving for Operational Semantics. PhD thesis, University of Cambridge, 1998.]]
28. Sym99.D. Syme. Proving Java type soundness. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1532 of Lecture Notes in Computer Science, pages 83-119. Springer Verlag, 1999.]]
29. TMC+96.D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In Proc. PLDI'96, pages 181-192, 1996.]]
30. TT97.M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109-176, 1997.]]
31. Van96.M. VanInwegen. The Machine-Assisted Proof of Programming Language Properties. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, May 1996.]]
32. vN99.D. von Oheimb and T. Nipkow. Machinechecking the Java specification: Proving typesafety. In J. Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1532 of Lecture Notes in Computer Science, pages 119- 156. Springer Verlag, 1999.]]
33. Yel99.P.M. Yelland. A compositional account of the Java TM Virtual Machine. In 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 57-69. ACM Press, 1999.]]

Index Terms

• Theory of computation

  • Logic

  • Models of computation

    • Computability

  • Semantics and reasoning

    • Program constructs

      • Type structures

    • Program semantics