ITR/SY+SI: Language Technology for Trustless Software Dissemination

karl Crary, Robert Harper, Peter Lee， Frank pfenning摘要：该项目研究了在非可信环境下软件的无信任传播的理论和工程基础。为了实现这一点，该项目调查了符合安全性、完整性和隐私要求的机器可检查证书。这种可检查的证书允许参与者验证传播软件的内在属性，而不是外部属性，如软件的起源点。为了获得可检查的证书，该项目开发了证书编译器，使其目标代码具有代码属性证明的正式表示。具体来说，该项目调查了用于此目的的携带证明代码、类型化中间语言和类型化汇编语言的使用。在每种情况下，证书验证都简化为在合适的类型系统中进行类型检查。为了展示无信任软件传播的效用，该项目开发了一个基础设施，用于构建利用计算机网络计算资源的应用程序。基础设施包括运行在主机上的“管家”，它在安装和执行经过认证的二进制文件之前接受并验证它们，以及生成经过认证的二进制文件以在网络上分发的认证编译器。调查的范围包括规范和认证的理论，以及实现这些思想所需的系统建设。

CR-0121633ITR/SY+SI: Language Technology for Trustless Software DisseminationKarl Crary, Robert Harper, Peter Lee, Frank PfenningABSTRACT:The project investigates the theoretical and engineering basis for the trustless dissemination of software in an untrusted environment. To make this possible the project investigates machine-checkablecertificates of compliance with security, integrity, and privacyrequirements. Such checkable certificates allow participants toverify the intrinsic properties of disseminated software, rather thanextrinsic properties such as the software's point of origin.To obtain checkable certificates the project develops certifyingcompilers that equip their object code with formal representations of proofs of properties of the code. Specifically, the projectinvestigates the use of proof-carrying code, typed intermediatelanguages, and typed assembly languages for this purpose. In eachcase certificate verification is reduced to type-checking in asuitable type system.To demonstrate the utility of trustless software dissemination, theproject develops an infrastructure for building applications thatexploit the computational resources of a network of computers. Theinfrastructure consists of a "steward" running on host computers thataccepts and verifies certified binaries before installing andexecuting them, and certifying compilers that generate certifiedbinaries for distribution on the network.The scope of the investigation includes the theory of specificationand certification, and the systems building required to implementthese ideas.