Languages

TLL

Typed Low-level Language for Open Runtime Platform (ORP)
 
Final Report Page

Introduction
The explosive growth of World Wide Web has induced interest in mobile computation. In this domain, the safety and security properties of programs are more crucial than ever before. Minimal Trusted Computing Base (TCB for short) is a classic computer security principle: The smaller and the simpler is the TCB of a system, the less vulnerable would it be. However today's computing system usually has heavyweight TCB. For example Java Virtual Machine (JVM for short) is a typical safe host to execute code obtained from network. A JVM implementation constitutes complicated components, such as a core virtual machine, a Just-In-Time (JIT for short) compiler, and a garbage collector. In most JVM, these parts are all in the TCB.
Inspired by the work on language-based security we propose Typed Low-Level Language (TLL for short). The design of TLL aims at the following three objectives:

  1. TLL is expressive enough to encode various high-level language features. It will allow TLL to be target language of multiple source languages.
  2. TLL is type safe, that is well-typed TLL code could not behave unsafely.
  3. TLL is suitable to be introduced to JVM as intermediate language of JIT compiler.

The primary purpose of this project is to reduce the TCB of an existing JVM implementation. Another benefit from the study is that a common intermediate language will allow us to construct a platform running programs in different source languages.
 
We designed and gave the formal specification of TLL. A subset of JVML, called FJVML, was chosen as the source language. It contains basic object-oriented features: classes and interfaces inheritance hierarchy, instance member access, and method invokation; and it also supports array manipulation. The type-preserving compilation from FJVML to TLL was discussed. TLL is used as certifying language in JIT compiler of an existent JVM, Open Runtime Platform (ORP).
A prototype system with JIT compiler based on TLL was built. Three papers depict the problems we faced to during studying.

Documentations

  • Completion Report (pdf) (doc)
  • Open Runtime Platform Internals (pdf) (doc)
  • A Brief Proof of Type Safety of TLL (in Chinese)(pdf) (doc)
  • Tech Report: A Prototype JVM with JIT Compiler using TLL as Intermediate Language (pdf) (doc)
  • Tech Report: A Enhanced Prototype Supporting Dynamic Type Analysis in Java (pdf) (doc)
  • Tech Report: Typed Low-level Language for Open Runtime Platform (ORP) (pdf) (doc)

Papers

  • A Typed Low-Level Language Used in Java Virtual Machine (in Chinese) (pdf) (doc)
  • Design Of A New Typed Low-level Language (in Chinese) (pdf) (doc)
  • A Tag Type For Certifying Compilation of Java Program (in Chinese) (pdf) (doc)

Software

  • The Prototype (rar)