Collaborative Research: High-Assurance Common Language Runtime

提出的研究重点是构建高置信度组件软件系统的新技术的设计和实现。这项新技术与提高商业虚拟机（如Java虚拟机（JVM）和微软的虚拟机）的安全性直接相关。NET公共语言运行时（CLR）。工作集中在三个方面：1。低级软件的高级规范。通用和灵活的基于逻辑的类型系统（LTS）正在设计中。这些类型系统源自作者开发的Certified Binaries技术，并扩展了当前JVM和CLR实现中使用的验证技术的范围、表达能力和精度。高保证虚拟机。使用作者的FoundationalProof-Carrying Code技术，可以构建更高保证的、经过验证的JVM或CLR基础架构实现。作者正致力于将他们的想法转移到英特尔正在建造的虚拟机中。资源认证。用于指定、组合和验证高级属性（如资源边界、内存和网络带宽）的新技术正在开发中。这些属性对于大型系统中不可信组件之间的安全互操作至关重要。

The proposed research focuses on the design and implementation of newtechnologies for building high-confidence component software systems. The newtechnology is directly relevant to improving security of commercialvirtual machines such as the Java virtual machine (JVM) andMicrosoft's .NET Common Language Runtime (CLR). The work concentrateson three areas:1. High-level specifications for low-level software. General andflexible logic-based type systems (LTS) are being designed. The typesystems are derived from the Certified Binaries technology developedby the authors and extend the scope, expressiveness and precision ofverification techniques used in current JVM and CLR implementations.2. A high-assurance virtual machine. Using the authors FoundationalProof-Carrying Code technology, higher-assurance, validatedimplementations of the JVM or CLR infrastructure are being built. Theauthors are engaged in technology transfer of their ideas to a virtualmachine being built at Intel.3. Resource certification. New technologies for specifying,composing, and verifying advanced properties such as resource boundson memory and network bandwidth are being developed. Theseproperties are crucial for safe and secure interoperation betweenuntrusted components in large-scale systems.