Collaborative Research: High-Assurance Common Language Runtime

Yale University, New Haven CT

Investigators

Abstract

The proposed research focuses on the design and implementation of new technologies for building high-confidence component software systems. The new technology is directly relevant to improving security of commercial virtual machines such as the Java virtual machine (JVM) and Microsoft's .NET Common Language Runtime (CLR). The work concentrates on three areas: 1. High-level specifications for low-level software. General and flexible logic-based type systems (LTS) are being designed. The type systems are derived from the Certified Binaries technology developed by the authors and extend the scope, expressiveness and precision of verification techniques used in current JVM and CLR implementations. 2. A high-assurance virtual machine. Using the authors Foundational Proof-Carrying Code technology, higher-assurance, validated implementations of the JVM or CLR infrastructure are being built. The authors are engaged in technology transfer of their ideas to a virtual machine being built at Intel. 3. Resource certification. New technologies for specifying, composing, and verifying advanced properties such as resource bounds on memory and network bandwidth are being developed. These properties are crucial for safe and secure interoperation between untrusted components in large-scale systems.