A Typed Low-Level Language Used in Java Virtual Machine

In the past ten years, there has been a trend in the field of trustworthy computing: building high-assurance software system based on programming languages and compilers. The most obvious advantage of these techniques is reducing trusted computing base of software system. Moreover the language-based techniques are suitable to describe and verify fine-grained safety policies. Inspired by these researches TLL is designed. It is expected to be a type-safe intermediate language used in the just-in-time compiler of Java virtual machine. The work described in this paper is based on Intel ORP, and aims at building a smaller trusted computing base. Compared with JVML, TLL is closer to the assemble language, and hence is convenient to encode high-level primitive efficiently. TLL type system is derived on polymorphic typed lambda calculus, which is expressive and general to encode various high-level language features. For case study, the self-application semantic, one of the most important safety properties of object-oriented language, is expressed and assured. A prototype using TLL as intermediate language in the just-in-time compiler can be granted as a starting point for building Java virtual machine with tiny trusted computing base.