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

CR-0121633 ITR/SY+SI：用于不可信软件分发的语言技术Karl克拉里，Robert哈珀，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.