×

Towards proving type safety of .NET CIL. (English) Zbl 1154.68359

Summary: A crucial role in the Microsoft .NET Framework Common Language Runtime security model is played by type safety of the Common Intermediate Language (CIL). In this paper, we formally prove type safety of a large subset of CIL. To do so, we begin by specifying the static and dynamic semantics of CIL by providing an abstract interpreter for CIL programs. We then formalize the bytecode verification algorithm, whose job it is to compute a well-typing for a given method. We then prove type safety of well-typed methods, i.e., the execution according to the semantics model of legal and well-typed methods does not lead to any run-time type violations. Finally, to prove CIL’s type safety, we show that the verification algorithm is sound, \(i.e.\), the typings it produces are well-typings, and complete, i.e., if a well-typing exists, then the algorithm computes one.

MSC:

68N25 Theory of operating systems

Software:

ML; LPTP; AsmL
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Hejlsberg A, Wiltamuth S, Golde P. C# language specification 1.2, MSDN; 2003.
[2] Microsoft .NET Framework 1.1 Software Development Kit, Web pages at \langle http://msdn.microsoft.com/netframework/howtoget/\rangle .
[3] Microsoft .NET Framework 2.0 Software Development Kit, Web pages at \langle http://msdn.microsoft.com/netframework/\rangle .
[4] ECMA International, C# language specification, Standard ECMA-334; 2001.
[5] Fruja NG. Towards Proving Type Safety of .NET CIL. Science of Computer Programming 2008;72(3):176. · Zbl 1154.68359 · doi:10.1016/j.scico.2008.05.004
[6] Fruja, N. G.; Börger, E.: Modeling the .NET CLR exception handling mechanism for a mathematical analysis, Journal of object technology 5, No. 3, 5-34 (2006)
[7] Fruja NG. Type safety of generics for the .NET common language runtime. In: Sestoft P, editor. ESOP ’06: programming languages and systems. Proceedings of the 15th European symposium on programming, Vienna, Austria. Lecture notes in computer science, vol. 3924. Berlin: Springer; 2006. p. 325 – 41. · Zbl 1178.68152
[8] Gurevich, Y.: Evolving algebras 1993: lipari guide, Specification and validation methods, 9-36 (1993) · Zbl 0852.68053
[9] Börger, E.; Stärk, R. F.: Abstract state machines. A method for high-level system design and analysis, (2003) · Zbl 1040.68042
[10] Börger, E.; Fruja, N. G.; Gervasi, V.; Stärk, R. F.: A high-level modular definition of the semantics of C, Theoretical computer science 336, No. 2 – 3, 235-284 (2005) · Zbl 1080.68006 · doi:10.1016/j.tcs.2004.11.008
[11] Stärk RF, Börger E. An ASM specification of C# threads and the .NET memory model. In: Zimmermann W, Thalheim B, editors. ASM ’04: proceedings of the 11th workshop on abstract state machines, Wittenberg, Germany. Lecture notes in computer science, vol. 3052. Berlin: Springer; 2004. p. 38 – 60. · Zbl 1188.68102
[12] Stärk, R. F.: Formal specification and verification of the C#thread model, Theoretical computer science 343, No. 3, 482-508 (2005) · Zbl 1077.68054
[13] Stärk, R. F.: The theoretical foundations of LPTP (a logic program theorem prover), Journal of logic programming 36, No. 3, 241-269 (1998) · Zbl 0911.68030 · doi:10.1016/S0743-1066(97)10013-9
[14] Jula HV. ASM semantics for C# 2.0. In: Beauquier D, Slissenko A, Börger E, editors. ASM ’05: proceedings of the 12th workshop on abstract state machines, Paris, France, 2005.
[15] Fruja NG. The correctness of the definite assignment analysis in C#. In: Skala V, Nienaltowski P, editors. .NET ’04: proceedings of the 2nd .NET technologies workshop, Pilsen, Czech Republic, 2004. p. 81 – 8.
[16] Fruja, N. G.: The correctness of the definite assignment analysis in C#(extended version), Journal of object technology 3, No. 9, 29-52 (2004)
[17] Fruja NG. Type safety of C#. Technical Report 612, ETH Zürich; 2008.
[18] .NET Framework Class Library. The System.ValueType class. Web pages at \langle http://msdn2.microsoft.com/en-us/library/system.valuetype.aspx\rangle .
[19] .NET Framework Class Library, The System.Exception class. Web pages at \langle http://msdn2.microsoft.com/en-us/library/system.exception.aspx\rangle .
[20] Jagger, J.; Perry, N.; Sestoft, P.: C#annotated standard, (2007) · Zbl 1138.68347
[21] Fruja NG. Specification and implementation problems for C#. In: Zimmermann W, Thalheim B, editors. ASM ’04: proceedings of the 11th workshop on abstract state machines, Wittenberg, Germany. Lecture notes in computer science, vol. 3052. Berlin: Springer; 2004. p. 127 – 43.
[22] Pierce, B.: Types and programming languages, (2002) · Zbl 0995.68018
[23] Milner, R.: A theory of type polymorphism in programming, Journal of computer and system sciences 17, 348-375 (1978) · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4
[24] Cook, W. R.: A proposal for making eiffel type-safe, Computer journal 32, No. 4, 305-311 (1989)
[25] Bruce, K. B.: Safe type checking in a statically-typed object-oriented programming language, , 285-298 (1993)
[26] Bruce, K. B.; Crabtree, J.; Murtagh, T. P.; Van Gent, R.; Dimock, A.; Muller, R.: Safe and decidable type checking in an object-oriented language, , 29-46 (1993)
[27] Drossopoulou S, Eisenbach S. Java is type safe — probably. In: ECOOP ’97: proceedings of the 11th European conference on object-oriented programming, Jyväskylä, Finland. Lecture notes in computer science, vol. 1241. Berlin: Springer; 1997. p. 389 – 418.
[28] Syme D. Proving Java type soundness. In: Alves-Foss J, editor. Formal syntax and semantics of Java. Lecture notes in computer science, vol. 1523. Berlin: Springer; 1999. p. 83 – 118.
[29] Nipkow, T.; Von Oheimb, D.: Javalight is type-safe — definitely, , 161-170 (1998)
[30] Drossopoulou S, Eisenbach S. Describing the semantics of Java and proving type soundness. In: Alves-Foss J, editor. Formal syntax and semantics of Java. Lecture notes in computer science, vol. 1523. Berlin: Springer; 1999. p. 41 – 82.
[31] von Oheimb D, Nipkow T. Machine-checking the Java specification: proving type-safety. In: Alves-Foss J, editor. Formal syntax and semantics of Java. Lecture notes in computer science, vol. 1523. Berlin: Springer; 1999. p. 119 – 56.
[32] Igarashi A, Pierce B. On inner classes. In: ECOOP ’00: proceedings of the 14th European conference on object-oriented programming, Sophia Antipolis and Cannes, France. Lecture notes in computer science, vol. 1850. Berlin: Springer; 2000. p. 129 – 53.
[33] Stärk, R. F.; Schmid, J.; Börger, E.: Java and the Java virtual machine — definition, verification, validation, (2001) · Zbl 0978.68033
[34] Hartel, P. H.; Moreau, L.: Formalizing the safety of Java, the Java virtual machine, and Java card, ACM computer surveys 33, No. 4, 517-558 (2001)
[35] Börger E, Stärk RF. Exploiting abstraction for specification reuse: the Java/C#case study. In: de Boer FS, et al., editors. FMCO ’03: proceedings of the 2nd symposium on formal methods for components and objects, Leiden, The Netherlands. Lecture notes in computer science, vol. 3188. Berlin: Springer; 2004. p. 42 – 76. · Zbl 1104.68357 · doi:10.1007/b100112
[36] Gurevich, Y.; Huggins, J. K.: The semantics of the C programming language, CSL ’92: selected papers from the 6th workshop on computer science logic, san miniato, Italy, 274-308 (1993) · Zbl 0788.68018
[37] Wallace, C.: The semantics of the C++ programming language, , 131-164 (1995) · Zbl 0852.68013
[38] Jula HV, Fruja NG. An executable specification of C#. In: Beauquier D, Slissenko A, Börger E, editors. ASM ’05: proceedings of the 12th workshop on abstract state machines, Paris, France, 2005. p. 275 – 87.
[39] Gurevich Y, Moss LS. Algebraic operational semantics and Occam. In: CSL ’89: proceedings of the 3rd workshop on computer science logic, Kaiserslautern, Germany. Lecture notes in computer science, vol. 40. Berlin: Springer; 1990. p. 176 – 92.
[40] Börger E, Durdanovic I, Rosenzweig D. Occam: specification and compiler correctness — part I: the primary model. In: PROCOMET ’94: proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 working conference on programming concepts, methods and calculi, San Miniato, Italy. IFIP Transactions, vol. A-56. Amsterdam: North-Holland; 1994. p. 489 – 508.
[41] Kutter, P. W.; Pierantonio, A.: The formal specification of oberon, Journal of universal computer science 3, No. 5, 443-503 (1997) · Zbl 0960.68112
[42] Börger, E.; Rosenzweig, D.: A mathematical definition of full prolog, Science of computer programming 24, No. 3, 249-286 (1995) · Zbl 0832.68022 · doi:10.1016/0167-6423(95)00006-E
[43] Mlotkowski M. Specification and optimization of the smalltalk programs. PhD thesis, University of Wroclaw; 2001.
[44] Alves-Foss J, editor. Formal syntax and semantics of Java. Lecture notes in computer science, vol. 1523. Berlin: Springer; 1998.
[45] M.R. Foundations of Software Engineering Group, Abstract State Machine Language (AsmL). Web pages at \langle http://research.microsoft.com/foundations/AsmL/\rangle .
[46] Schmid J. Executing ASM specifications with AsmGofer. Web pages at \langle http://www.tydo.de/AsmGofer\rangle .
[47] Schmid J. Refinement and implementation techniques for abstract state machines. PhD thesis, University of Ulm; 2002.
[48] Fruja NG. A modular design for the .NET CLR architecture. Technical Report 493, ETH Zürich; 2005.
[49] Paulson L, Nipkow T. Isabelle — generic theorem proving environment. Cambridge: Cambridge University, Technical University Munich.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.