一种用于Java虚拟机的类型化低级语言

A Typed Low-Level Language Used in Java Virtual Machine

为了能够减小运算系统的需信任计算基础、描述较小粒度的安全策略,目前的研究倾向于从程序设计语言和编译器入手来提高软件的安全性·基于以上研究背景设计了一种类型化的低级语言TLL·TLL是一种为Java虚拟机即时编译器设计的类型安全中间语言,以构造一个具有更小需信任计算基础的Java虚拟机系统为目的·TLL的类型系统基于多态的类型化λ演算,它具有丰富的表现力且能够编码各种高级语言的抽象·基于TLL的一个虚拟机原型系统已经实现,它可以作为实现一个高安全且面向多种源语言的运行时系统的起点·

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.