Trust in the-calculus

Abstract

This paper introduces trust analysis for higher-order languages. Trust analysis encourages the programmer to make explicit the trustworthiness of data, and in return it can guarantee that no mistakes with respect to trust will be made at run-time. We present a conuen t -calculus with explicit trust operations, and we equip it with a trust-type system which has the subject reduction property. Trust information is presented as annotations of the underlying Curry types, and type inference is computable in O(n 3 ) time. As computers are increasingly being used to handle important transactions (such as interchange of legal documents) in an open environment where also information that does not pertain directly to business is transferred between the same machines (for example e-mail), the issue of separating these two kinds of information o w has become more and more important. The issue is usually attacked using encryption and digital signatures for the important information o ws between machines, but what good does this do if somewhere inside a program, there is a data path between reading a message and some dangerous operation such that the dangerous operation depends on the contents of a message whose signature is not checked? An example where it is important to perform validity checks on all data paths from input to output, is in an HTTP (HyperText Transfer Protocol, the protocol used on the world-wide web) server that allows a web-browser to start a separate program (a so-called CGI script, for Common Gateway Interface) on the server machine by requesting a specic URL. The usual convention is that the browser requests a URL of the form http://www.company.com/cgi-bin/program-name. Since a CGI script can in principle be any program, it is important that the server checks that the requested program is one of the few programs that are allowed to be run in this fashion. In a complicated server, like most servers today, there are many data-paths from the initial reception of the URL request to the command to be executed, and it is imperative that the checks for allowed programs be performed on all these paths. The trust analysis presented in this paper is developed to help the programmer ensure that the requisite checks are always made. A very similar situation existed in a part of the Gopher (an earlier and simpler