Applying Compiler Techniques to Proof-Carrying Code

提案编号：CCR-9974553标题：将编译器技术应用于携带证明代码PI：Andrew W.AppelProof携带代码(PCC)是移动代码安全领域一个令人兴奋的新发展。不受信任的代码提供者提供本机代码程序以及安全证明；代码使用者可以在执行程序之前检查该证明。由于校对是一个简单且易于机械化的过程，因此该系统的可信计算基础可能非常小。然而，PCC是一项不成熟的技术，面临着几个挑战：保持证明规模小，证明复杂操作(如分配和初始化数据结构)的安全性，以及使代码使用者的安全策略具有普遍性和语言独立性。本项目将解决这些问题，将为编译器开发的科学和技术应用到程序验证领域。

Proposal Number: CCR-9974553Title: Applying Compiler Technology to Proof-Carrying CodePI: Andrew W. AppelProof-carrying code (PCC) is an exciting new development in mobile-codesecurity. An untrusted code provider provides a native-code programalong with a proof of safety; the code consumer can check the proof beforeexecuting the program. Since proof-checking is a simple andeasily mechanized process, the trusted computing base of this systemcan be quite small. However, PCC is an immature technology and facesseveral challenges: keeping proof size small, proving safety of complexoperations such as allocating and initializing data structures, andmaking the code consumer's safety policy universal and language-independent.This project will address each of these issues, applying science andtechnologydeveloped for compilers to the area of program verification.