Collaborative Research: High-Assurance Common Language Runtime

提出的研究重点是设计和实现用于构建高置信度组件软件系统的新技术。这项新技术与提高Java虚拟机(JVM)和微软.NET公共语言运行时(CLR)等商业虚拟机的安全性直接相关。这项工作主要集中在三个方面：1.低层软件的高层规范。通用的和灵活的基于逻辑的类型系统(LTS)正在设计中。类型系统是从作者开发的认证二进制技术派生出来的，扩展了当前JVM和CLR实现中使用的验证技术的范围、表达能力和精度。一台高保证的虚拟机。使用作者的FoundationalProof承载代码技术，正在构建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.