Type Systems for Secure Remote Evaluation

远程评估系统的特征在于客户端将程序发送到计算服务器以代表其执行。服务器向客户端返回执行程序的结果。这与RPC和CGI脚本相反，它们是服务器端程序的示例，而不是远程评估。远程评估似乎越来越流行，新出现的支持远程评估的编程语言就证明了这一点，其中包括Telescript、Tcl、Oblique和Java。Java和Java兼容的Web浏览器支持的下载和执行范例是远程评估的一个例子;然而，在这种情况下，Web服务器将Java增强的HTML文件发送到浏览器，然后浏览器执行该文件。服务器安全是远程评估的一个主要问题。服务器的可用性、隐私和完整性不得受到损害。当前用于确保服务器安全性的技术是自组织的。这些技术可以保证什么样的安全属性没有精确的描述。因此，典型的反应是限制（或者在大多数情况下完全禁止）应用程序对服务器资源的访问。这大大削弱了远程评价模式。本研究探讨的作用，编程语言的设计和类型系统，以确保服务器的安全性，在远程评估系统。具体来说，长期目标是在类型系统的上下文中开发静态分析，以确保远程评估的程序不会侵犯服务器的隐私或完整性。类型可靠性定理正在开发和证明的核心命令式语言的正式语义。它们精确地描述了用该语言编写的良好类型程序的安全属性。还研究了编程语言中的并发和异常等功能对安全属性的影响。***

A remote evaluation system is characterized by a client that sends a program to a compute server for execution on its behalf. The server returns to the client the results of executing the program. This is in contrast to RPC and CGI scripts which are examples of server-side programs, not remote evaluation. Remote evaluation appears to be gaining currency as evidenced by new programming languages emerging to support it. Among them are Telescript, Tcl, Oblique and Java. The download-and-execute paradigm supported by Java and Java-compatible Web browsers is an example of remote evaluation; in this case, however, a Web server sends a Java-enhanced HTML file to a browser which the browser then executes. Server security is a major problem with remote evaluation. A server's availability, privacy and integrity must not be compromised. Current techniques for ensuring server security is ad hoc. There is no precise characterization of what kind of security properties these techniques can guarantee. Consequently, the typical reaction is to limit, or in most cases prohibit altogether, an application's access to server resources. This greatly weakens the remote evaluation paradigm. This research investigates the role of programming language design and type systems in ensuring the security of servers in remote evaluation systems. Specifically, the long-term objective is to develop static analyses, within the context of type systems, to ensure that remotely-evaluated programs do not violate a server's privacy or integrity. Type soundness theorems are being developed and proved with respect to a formal semantics for a core imperative language. They precisely characterize the security properties of well-typed programs written in the language. The impact of features such as concurrency and exceptions in a programming language on security properties is also investigated. ***