The Safe Language Kernel (SLK) Project

 

Thorsten von Eicken, Chris Hawblitzel, Chi-Chao Chang, Grzegorz Czajkowski, and Deyu Hu

Department of Computer Science, Cornell University

 

Current "secure" systems based on Java suffer from two limitations. First, while the current Java security model based on the "security manager" is adequate for isolated protection domains that do not share with each other, the model does not address the needs of protection domains that must share data in a fine-grained manner while still being protected from one another. Second, the security of the system depends on the correctness of the Java virtual machine implementation. The size and complexity of a virtual machine (especially an optimizing just-in-time compiler), however, has led to bugs in many virtual machines that result in security holes.

To address the first problem, we have worked on capability-based mechanisms for sharing objects and classes among multiple protection domains. Because of the type safety provided by the language, all of the protection domains can co-exist in a single address space, resulting in a very low overhead for cross-domain calls. To demonstrate the value of this, we are extending Jigsaw, a popular Java-based web server, to support downloadable servlets. The web server is protected from the servlets, and the servlets are protected from each other, but they are still able to share code and data. In particular, the server and the servlets share information about http requests to the server. Because no address space switch is required to pass this information from the server to the servlet, requests can be handled faster than with CGI scripts. Protection is handled by building capabilities with unforgeable object references. We have developed a "type capability" model to precisely capture the relationship between object references, types, and traditional operating systems capabilities. In addition, to support flexible sharing of code among servlets, we are developing a Java virtual machine and verifier that safely handle the sharing of classes between different class loaders.

To address the second problem, we are developing a type-safe assembly language layer that can be verified at a much lower level than Java bytecode. Current Java just-in-time compilers perform a verification pass on the high-level Java bytecode to ensure that the bytecode is safe, but the checks performed by the verifier are ad-hoc, and safety is not necessarily preserved as the high-level bytecode is translated into low-level assembly code. In order to make the type system as low-level and flexible as possible, we are integrating proofs into the type system itself. Types are replaced by "type predicates", which allow the compiler to express incomplete knowledge about data and to discover knowledge by examining data. A compiler can only generate code to access data if it proves in its type predicates that the access is safe.