BRICS RS-95-31 Palsberg & �rb�k: Trust in the λ-calculus

BRICS

Basic Research in Computer Science

Trust in the λ-calculus

Jens Palsberg Peter �rb�k

BRICS Report Series RS-95-31 ISSN 0909-0878 June 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Trust in the λ-calculus

Jens Palsberg Peter Ørbæk

BRICS^{∗}

Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C, Denmark

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 confluent λ-calculus with explicit trust operations, and we equip it with a trust-type system which has the subject reduction property. Trust information in presented as two annotations of each function type constructor, and type inference is computable in O(n^{3}) time.

1 Introduction

With todays popular client-server software, server software needs to be very careful about the input they get from possibly untrustworthy clients. While writing server software one needs to be permanently aware of which data should be trusted (e.g., data coming from local databases or from authenticated clients) and which data cannot be trusted, such as input coming from unauthenticated clients.

Trust analysis aims to help the programmer write secure systems that cannot as easily be spoofed into trusting untrustworthy data. On one hand trust analysis enforces a certain discipline on the programmer, on the other hand it offers some guarantees that the software doesn’t mistakenly trust untrustworthy data.

In [14] the second author introduced the concept of trust analysis for a simple first order imperative language using abstract interpretation. This paper extends trust analysis to a language with higher order functions.

∗Basic Research in Computer Science, Centre of the Danish National Research Foundation.

E-mail: {palsberg,poe}@daimi.aau.dk.

The remainder of the paper is structured as follows. First we give some intuitions about the intended program analysis, the semantics of our example language, and the type system. Then we present an extension of the λ-calculus together with an operational reduction semantics. The semantics is shown to have the Church-Rosser property. We define our static trust analysis in terms of a type system. The type system is shown to have the Subject Reduction property with respect to the reduction rules of the semantics. We then relate our type system to the classical Curry type system for λ-calculus and see that our system is a proper restriction of Currys system in that it accepts fewer programs. We also state some results relating reductions in our semantics with reductions in λ-calculus and finally we prove that well-typed terms are strongly normalizing. Then a type inference algorithm is presented and proved correct with respect to the type system. Finally we discuss how to extend the type system to handle recursion and polymorphism, and we relate trust analysis to other program analyses.

1.1 Motivation

Suppose we are writing a program using a patient database and assume the database contains sensitive data that should be accessible only to a few privileged people. In our library we are given two functions:

see-some: PatientId ⟶ Info see-all: PatientId ⟶ Info.

The see-some function returns non-sensitive information related to a patient, whereas see-all returns all recorded information about a patient.

With ordinary types these two functions seems to be interchangeable, and the lazy programmer may choose to use see-all at all times because it’s just plain easier to remember one function than two. Our aim is to force the programmer to distinguish these two functions. In the type system presented in Section 3 the typings would be:

see-some: PatientId⟶^{⊤ ⊤}Info # ⊥ see-all: PatientId⟶^{⊥ ⊥}Info # ⊥ .

Each function (and in general each expression) is associated with a decorated type and an annotation about the trustworthiness of the value of that expression. An expression having annotation ⊥ (bottom) is treated as trusted whereas the annotation ⊤ (top) means that the value cannot be trusted. Expressions of function type s ⟶^{u v} t take arguments of decorated type s and these arguments must be at least as trustworthy as stated by the decoration u. The result of applying the function will have decorated type t, and the result will be trustworthy only if v is and the function applied is itself trusted.

With this in mind calls to see-all would not be allowed by the type system unless the actual argument had a trustworthy value, i.e., one derived solely from other trustworthy values or explicitly blessed into being trusted.

In order to allow programs to implement validity checks on data that subsequently should be regarded as trusted, our language includes a trust construct that behaves as the identity with respect to values, but informs the analysis that the result should henceforth be regarded as trustworthy. Symmetrically, there is a distrust construct that “curses” data into being untrusted.

The programmer is thus forced to make explicit when she needs trustworthy data and when untrusted data will do. Since raising of trustworthiness has to be made explicit in the program it can be better controlled, and we minimize the risk of using untrustworthy data (provided by some villain) unintentionally where trusted data are needed.

There is a third construct in our language: check, which intuitively aborts evaluation if the argument is not trustworthy. This would be what forces the type of see-all above. One might imagine the definition see-all looking like (ML’ish syntax):

fun see-all pid = let tpid = check pid in ...

We want a static analysis that can guarantee the programmer that no mistakes concerning trust exists in the program, i.e., that no untrustworthy data reach a check. Our decorated type system keeps explicit track of the trust “tags” together, and in parallel with, the ordinary type of values, and there are no trust tags around during run-time.

With all of this under our belts, we may now consider the following program fragment:

credentialsOK: Cred⟶^{⊥ ⊥} Bool # ⊥

fun validateID credentials id g f =

if credentialsOK credentials then // if we are credible

g (trust id) // call the “good” continuation else

f id // call “failure” continuation endif

... let info = validateID credentials id see-all see-some in ...

Assuming credentials is trusted and id untrusted, validateID would get the type:

Cred⟶^{⊥ ⊥}PatientId⟶^{⊤ ⊥} (PatientId⟶^{⊥ ⊥}Info)⟶^{⊥ ⊥} (PatientId⟶^{⊤ ⊤}Info)⟶^{⊥ ⊤} Info .

E, F, G, H ::= x | λx.E | EE | trust E | distrust E | check E

Figure 1: The syntax of expressions

If the program is written such that trust occurs only in such validate routines then the trust analysis will effectively guarantee us that see-all and similarly typed functions will only be called in situations where the process’ credentials are in order.

Note the close coupling between checking credentials and the application of trust. This is a central point in the setup. It is here that the static analysis is coupled with the run-time properties of the program. Trust analysis deals with properties of data that cannot be decided from the values of that data. In some runs of the above program, a PatientId number might be trusted whereas in other runs of the same program that same number might be untrusted. This is a main point where trust analysis differs from many other program analyses. The differences between trust analysis and other program analyses is further discussed in Section 5.

In the remainder of the paper the above ideas are formalized in an extension of the λ-calculus.

2 Syntax and Semantics

This section presents the syntax and operational semantics of the trust language. Figure 1 defines the syntax of our language.

Variables, lambda abstraction and application behave as usual. Trust E is used to introduce trusted values in a program. One may view trust as a run-time tag on values that indicate the trustworthiness of the value. Symmetrically, distrust indicates untrusted values. The check construct will only reduce on trusted values, so evaluation may get stuck if an expression check(distrust E) occurs at some point during evaluation.

2.1 Reduction rules

The reduction (or evaluation) rules for the language are given in Figure 2. Stating E → E′ means that there is a derivation of that reduction in the system.

There are three kinds of values around during reduction: trusted, distrusted and untagged. Untagged lambdas are treated as trusted program constants in the (Lambda Contraction) rules, since lambdas stem from the program text which the programmer is writing himself and they may therefore be trusted.

In order to facilitate the proof of the Church-Rosser property of the system, the reduction rules form a reflexive “one step” transition relation. This is inspired by the proof of Church-Rosser for the ordinary λ-calculus by Tait and Martin-Löf in [2, pp. 59–62].

E → E  (Reflex)
\frac{E → E′}{λx.E → λx.E′ trust E → trust E′ distrust E → distrust E′ check E → check E′}  (Sub)
\frac{E → trust E′}{trust E → trust E′ distrust E → distrust E′ check E → trust E′}  (Trust Contraction)
\frac{E → distrust E′}{trust E → trust E′ distrust E → distrust E′}  (Distrust Contraction)
\frac{E → check E′}{trust E → check E′ check E → check E′}  (Check Contraction)
\frac{E → λx.E′}{trust E → λx.E′ check E → λx.E′}  (Lambda Contraction)
\frac{E → E′ F → F′}{EF → E′F′ (λx.E)F → E′[F′/x] (distrust (λx.E))F → distrust E′[F′/x]} (Application)

Figure 2: The reduction rules.

\frac{E → const}{trust E → const check E → const}  (Constant)

T ≡ K ≡ λxy.x  (True)
F ≡ λxy.y  (False)
if E then F else G ≡ EF G  (If)

\frac{E → E′ F → F′}{if T then E else F →^{∗} E′ if F then E else F →^{∗} F′ if distrust T then E else F →^{∗} distrust E′ if distrust F then E else F →^{∗} distrust F′} (If)

Figure 3: Example rules.

The contraction rules exist to eliminate redundant uses of our new constructs in the calculus. For example, trusting an expression twice is the same as trusting it once (the first (Trust Contraction) rule) and checking the trustworthiness of an expression followed by explicitly trusting it is the same as just checking the expression. Checking an explicitly trusted expression succeeds and yields a trusted expression. Note that there is no rule contracting distrust(check E) since this would allow the removal of the check on the trustworthyness of E.

In the following we always consider equality of terms modulo α-renaming. Terms for which no further reductions are possible, i.e ¬∃F ≠ E : E → F are said to be in normal form. There are proper and improper normal forms. A normal form containing a subterm: check(distrust E′) is said to be improper. All other normal forms are proper.

As an example of how to extend the language with usual programming constructs, we show in Figure 3 how a reduction rule for program constants would look and the derived rules we get for if-then-else with the usual coding of booleans in the λ-calculus. Notice how the (Constant) rules are patterned after the (Lambda Contraction) rules. In Section 5 we also show how to encode a rec construct in the language.

2.2 Church-Rosser

The Church-Rosser (or confluence) theorem for a reduction system states that for any term, if the term can reduce to two different terms there exists a successor term such that both of the two reduced terms can further reduce to that common successor. A corollary of this is that a normal form is unique if it exists.

We write →^{∗} for the reflexive transitive closure of the reduction relation →. Theorem 1 (Church-Rosser) For expressions E, F and G. If E →^{∗} F and E →^{∗} G then there is an expression H such that F →^{∗} H and G →^{∗} H. Proof. By the Diamond lemma below (Lemma 7) and Lemma 3.2.2 of [2]. □ Lemma 2 If E → F and E has a certain structure then some conditions on the structure of F hold, as made explicit below.

• If trust E_{1} → F then F = α F_{1} where α ∈ {check, trust, λx.}.

• If check E_{1} → F then F = α F_{1} where α ∈ {check, trust, λx.}.

• If distrust E_{1} → F then F is of the form distrust F_{1}.

• If λx.E_{1} → F then F is of the form λx.F_{1}. Proof. In each case by inspection of the reduction rules. □ Lemma 3 (Trust/Check Identity) Let α ∈ {trust, check, λx.}. If E → α E_{1} then check E → α E_{1} and trust E → α E_{1} Proof. By inspection of the reduction rules, especially the contraction rules. □ Lemma 4 (Symmetry) Let α, β ∈ {trust, distrust}. If α E → α E′ then β E → β E′ Proof. By induction on the structure of the derivation of α E → α E′, verifying that in each case there is also a corresponding rule for the opposite combination.

□

Lemma 5 (Pre-Substitution) If E → F then G[E/x] → G[F/x]. Proof. By induction on the structure of G. This is essentially a consequence of the (Sub) rules and the first (Application) rule. □ Lemma 6 (Substitution) If E → F and G → H then E[G/x] → F [H/x]. Proof. By induction on the structure of the derivation of E → F. If F = E by the (Reflex) axiom, we must show that E[G/x] → E[H/x] given that G → H. This is the Pre-Substitution lemma (5).

For all the rules except the (Application) case: Suppose that α, β, and γ are in the set {check, trust, distrust, λx.} as appropriate, and β and γ may be empty as well. Assume the rule

\frac{E_{1} → β F_{1}}{E = α E_{1} → γ F_{1} = F}

is the last rule in the derivation of E → F. By the induction hypothesis we get

E_{1}[G/x] → (β F_{1})[H/x] = β(F_{1}[H/x]).

Now E[G/x] = α E_{1}[G/x] and F [H/x] = γ F_{1}[H/x], and we may now deduce

\frac{E_{1}[G/x] → β F_{1}[H/x]}{α E_{1}[G/x] → γ F_{1}[H/x]}

as required. Of course, in the case of a lambda, if the bound variable is the one substituted for, nothing happens during substitution, i.e.

E[G/x] = E → F = F [H/x]

as the only rule applicable to the case of α = λx. is the (Sub) rule.

The (Application) cases: If E = E_{1}E_{2} → F_{1}F_{2} = F, where E_{1} → F_{1} and E_{2} → F_{2} then the result follows directly from the induction hypothesis. Suppose the last rule in the derivation of E → F was (x ≠ y):

\frac{E_{1} → F_{1} E_{2} → F_{2}}{E = (λy.E_{1})E_{2} → F_{1}[F_{2}/y] = F}

By the induction hypothesis E_{1}[G/x] → F_{1}[H/x] and similarly for E_{2}. Also E[G/x] = (λy.E_{1}[G/x])(E_{2}[G/x]) and

F [H/x] = (F_{1}[F_{2}/y])[H/x] = (F_{1}[H/x])[F_{2}[H/x]/y]

where the last equality depends on y not being free in H. This can be assured by α-renaming H. We may now deduce:

\frac{E_{1}[G/x] → F_{1}[H/x] E_{2}[G/x] → F_{2}[H/x]}{(λy.E_{1}[G/x])(E_{2}[G/x]) → (F_{1}[H/x])[F_{2}[H/x]/y]}

Suppose the last rule in the derivation of E → F was:

\frac{E_{1} → F_{1} E_{2} → F_{2}}{E = (λx.E_{1})E_{2} → F_{1}[F_{2}/x] = F}

By the induction hypothesis, E_{2}[G/x] → F_{2}[H/x]. Also E[G/x] = (λx.E_{1})(E_{2}[G/x]) and

F [H/x] = (F_{1}[F_{2}/x])[H/x] = F_{1}[F_{2}[H/x]/x].

Now

\frac{E_{1} → F_{1} E_{2}[G/x] → F_{2}[H/x]}{(λx.E_{1})(E_{2}[G/x]) → F_{1}[F_{2}[H/x]/x]}

as required. Two similar cases apply to the distrust λx.E case. □

Lemma 7 (Diamond) For expressions E, F and G. If E → F and E → G then there is an expression H such that F → H and G → H. Proof. By induction on the derivation of E → F and E → G and by cases on how F and G must look depending on E.

Depending on E there are a number of applicable rules. In all cases (Reflex) and (Sub) are applicable.

1. E = λx.E_{1}: none other.

2. E = trust E_{1}:

(a) E → trust E′_{1} since E_{1} → trust E′_{1}. (Trust Contraction)

(b) E → λx.E′_{1} since E_{1} → λx.E′_{1}. (Lambda Contraction)

(c) E → check E′_{1} since E_{1} → check E′_{1}. (Check Contraction)

(d) E → trust E′_{1} since E_{1} → distrust E′_{1}. (Distrust Contraction)

3. E = distrust E_{1}:

(a) E → distrust E′_{1} since E_{1} → trust E′_{1}. (Trust Contraction)

(b) E → distrust E′_{1} since E_{1} → distrust E′_{1}. (Distrust Contraction)

4. E = check E_{1}:

(a) E → trust E′_{1} since E_{1} → trust E′_{1}. (Trust Contraction)

(b) E → check E′_{1} since E_{1} → check E′_{1}. (Check Contraction)

(c) E → λx.E′_{1} since E_{1} → λx.E′_{1}. (Lambda Contraction)

5. E = (λx.E_{1})E_{2}: E → E′_{1}[E′_{2}/x] since E_{1} → E′_{1} and E_{2} → E′_{2}.

6. E = (distrust λx.E_{1})E_{2}: E → distrust E′_{1}[E′_{2}/x] since E_{1} → E′_{1} and E_{2} → E′_{2}. If E → F or E → G by (Reflex) then there is no problem, one may just use the

rule applied in the other branch to get to the common successor. Case 1 is easy as well: there is only one applicable rule except (Reflex) namely (Sub).

The tables below map pairs of “outgoing” reductions to proofs of the corresponding case.

Case 2 2a 2b 2c 2d (Sub)
2a  B B C  A
2b  B C  A
2c  C  A
2d  D

Case 3 3a 3b (Sub)
3a G F
3b  E
Case 4 4a 4b 4c (Sub)
4a  B B  A
4b  B  A
4c  A

For case 6 the argument is as follows: Here the last rules in the derivation of E → F and E → G were:

\frac{E_{1} → F_{1} E_{2} → F_{2}}{E = (distrust λx.E_{1})E_{2} → distrust F_{1}[F_{2}/x] = F} (Application)

and

\frac{E_{1} → G_{1} E_{2} → G_{2}}{E = (distrust λx.E_{1})E_{2} → (distrust λx.G_{1})G_{2} = G} (Sub)

respectively. By the induction hypothesis there are H_{1} and H_{2} such that F_{1} → H_{1}, G_{1} → H_{1} and F_{2} → H_{2}, G_{2} → H_{2}. So by the Substitution lemma (Lemma 6) (and (Sub)):

F = distrust F_{1}[F_{2}/x] → distrust H_{1}[H_{2}/x] = H

and by (Application)

G = (distrust λx.G_{1})G_{2} → distrust H_{1}[H_{2}/x] = H.

Case 5 without distrust is similar.

In each of the cases below, the quest is to find an appropriate common successor H to F and G.

Case A. Let α ∈ {trust, check} and β ∈ {trust, check, λx.}. The last rules of the derivation of E → F and E → G were

\frac{E_{1} → β F_{1}}{E = α E_{1} → β F_{1} = F} (β Contraction)

\frac{E_{1} → G_{1}}{E = α E_{1} → α G_{1} = G} (Sub)

By the induction hypothesis there is an H_{1} such that G_{1} → H_{1} and β F_{1} → H_{1} By Lemma 2 and the restriction on β; H_{1} = γ H_{2} where γ ∈ {trust, check, λx.}. By the Trust/Check Identity lemma (Lemma 3), G_{1} → γ H_{2} implies that α G_{1} → γ H_{2} = H_{1}. So we can use H = H_{1}.

Case B. Let α, β, γ ∈ {trust, check, λx} as appropriate. The last rules used in the derivation of E → F and E → G are:

\frac{E_{1} → β F_{1}}{E = α E_{1} → β F_{1} = F} (β Contraction)

\frac{E_{1} → γ G_{1}}{E = α E_{1} → γ G_{1} = G} (γ Contraction)

By the induction hypothesis there is an H_{1} such that β F_{1} → H_{1} and γ G_{1} → H_{1}. We may now use H_{1} as H.

Case C. Let α ∈ {trust, check, λx.}. The two last rules used in the derivation of E → F and E → G are:

\frac{E_{1} → α F_{1}}{E = trust E_{1} → α F_{1} = F} (α Contraction)

\frac{E_{1} → distrust G_{1}}{E = trust E_{1} → trust G_{1} = G} (Distrust Contraction)

By the induction hypothesis we know there exists H_{1} such that α F_{1} → H_{1}. Here Lemma 2 says that H_{1} = β H_{2} where β ∈ {check, trust, λx.}. Also by the induction hypothesis we have distrust G_{1} → H_{1}. And here Lemma 2 says that H_{1} = distrust H_{2}! This is a contradiction so it cannot be the case that both E_{1} → α F_{1} and E_{1} → distrust G_{1}.

Case D. The two last rules used in the derivation of E → F and E → G are:

\frac{E_{1} → distrust F_{1}}{E = trust E_{1} → trust F_{1} = F} (Distrust Contraction)

\frac{E_{1} → G_{1}}{E = trust E_{1} → trust G_{1} = G} (Sub)

By the induction hypothesis there is an H_{1} such that distrust F_{1} → H_{1} and G_{1} → H_{1}. By Lemma 2 H_{1} = distrust H_{2} so

\frac{G_{1} → distrust H_{2}}{trust G_{1} → trust H_{2}} (Distrust Contraction)

By Symmetry (Lemma 4) distrust F_{1} → distrust H_{2} implies trust F_{1} → trust H_{2}. So we can use trust H_{2} as H.

Case E. The two last rules used in the derivation of E → F and E → G are:

\frac{E_{1} → distrust F_{1}}{E = distrust E_{1} → distrust F_{1} = F} (Distrust Contraction)

\frac{E_{1} → G_{1}}{E = distrust E_{1} → distrust G_{1} = G} (Sub)

By the induction hypothesis there is an H_{1} such that distrust F_{1} → H_{1} and G_{1} → H_{1}. By Lemma 2 H_{1} = distrust H_{2}. By (Distrust Contraction) G_{1} → distrust H_{2} implies distrust G_{1} → distrust H_{2} = H_{1}. So we use H = H_{1} in this case.

Case F. The two last rules used in the derivation of E → F and E → G are:

\frac{E_{1} → trust F_{1}}{E = distrust F_{1} → distrust F_{1} = F} (Trust Contraction)

\frac{E_{1} → G_{1}}{E = distrust E_{1} → distrust G_{1} = G} (Sub)

By the induction hypothesis there is an H_{1} such that trust F_{1} → H_{1} and G_{1} → H_{1}. By Lemma 2 H_{1} = α H_{2} where α ∈ {trust, check, λx.}.

If α = trust then we have G_{1} → trust H_{2} and trust F_{1} → trust H_{2} and by Symmetry distrust F_{1} → distrust H_{2}. By (Trust Contraction) we also get distrust G_{1} → distrust H_{2}, so here we may use H = distrust H_{2}.

If α = check or α = λx. then by (Sub) we get distrust G_{1} → distrust (α H_{2}). Since trust F_{1} → α H_{2} one sees by inspection of the rules that for each α there is just one possible last rule for this reduction so we must have F_{1} → α H_{2}. Now by (Sub) we get distrust F_{1} → distrust (α H_{2}). So here we may use H = distrust (α H_{2}).

Case G. The two last rules used in the derivation of E → F and E → G are:

\frac{E_{1} → distrust F_{1}}{E = distrust E_{1} → distrust F_{1} = F} (Distrust Contraction)

\frac{E_{1} → trust G_{1}}{E = distrust E_{1} → distrust G_{1} = G} (Trust Contraction)

By the induction hypothesis there is an H_{1} such that distrust F_{1} → H_{1} and trust G_{1} → H_{1}, but by Lemma 2 this is a contradiction so this case cannot arise.

This concludes the proof of the Diamond lemma. □

\begin{aligned}u, v, w & ::= & ⊤ | ⊥ \\ s, t & ::= & base | s ⟶^{u v} t \end{aligned}

Figure 4: Syntax of trust-types

3 The Type System

Our decorated type system is based on Currys simple monomorphic type system for the λ-calculus, also known as simply typed λ-calculus. Figure 4 shows the syntax of the trust-types. Recall from Section 1.1 that ⊥ means that the value is trusted and ⊤ means that it is untrusted.

Trust-types are subject to a partial ordering ≤, defined on trusts as: ⊥ ≤ ⊤ and extended to types such that two base types are ordered only if they are identical, and for arrow types:

s ⟶^{u v} t ≤ s′ ⟶^{u′ v′} t′ if and only if s′ ≤ s, u′ ≤ u, v ≤ v′ and t ≤ t′

so argument types are ordered contravariantly. This is inspired by the work on structural subtyping by Mitchell [12] and others.

We denote by ⊔ the least upper bound operation on the trust lattice. In Section 5 we discuss several extensions of the type system to cope with recursion, polymorphism and more general lattices.

3.1 Rules

A type assumption A is a partial function which takes a program identifier to a pair of its type and trust. Figure 5 shows the inference rules for the type system. A type judgment A ⊢ E : t # u means that from the assumptions A we can deduce that the expression E has type t and is as trustworthy as u.

The rule for variables and the subtyping rule should give no surprises. A lambda expression occurring in the program is always known to have a function type thus we can mark all lambdas in the program as trusted. This means that we trust that a lambda will evaluate to a function, but it says nothing about the arguments and results of the function. That information is kept in the arrow type.

In the application rule, the trust of the actual argument is required to match the argument trust coded in the arrow type of the function. The trust of the result of the application is the least upper bound of the result-trust from the arrow type and the trust of the function itself. The intuition is that if we cannot trust the function, we cannot trust the result of applying it.

The three rules for trust, distrust and check show that they behave as the identity on the type. Trust makes any value trusted and distrust makes any value untrusted. Check E has a type only if E is trusted. This means that we cannot type improper

A ⊢ x : t # u if x ∈ dom(A) and A(x) = ⟨t, u⟩ (Var)
\frac{A ⊢ E : t # u t ≤ t′ u ≤ u′}{A ⊢ E : t′ # u′}  (Sub)
\frac{A[x ↦ ⟨t, u⟩] ⊢ E_{1} : s # v}{A ⊢ λx.E_{1} : t ⟶^{u v} s # ⊥}  (Lambda)
\frac{A ⊢ E_{1} : s ⟶^{u v} t # w A ⊢ E_{2} : s # u}{A ⊢ E_{1}E_{2} : t # v ⊔ w}  (App)
\frac{A ⊢ E_{1} : t # u}{A ⊢ trust E_{1} : t # ⊥}  (Trust)
\frac{A ⊢ E_{1} : t # u}{A ⊢ distrust E_{1} : t # ⊤}  (Distrust)
\frac{A ⊢ E_{1} : t # ⊥}{A ⊢ check E_{1} : t # ⊥}  (Check)

Figure 5: The type system.

[figure: distrust ∘ check : t ⟶^{⊥ ⊤} t; trust: t ⟶^{⊤ ⊥} t; check: t ⟶^{⊥ ⊥} t; distrust: t ⟶^{⊤ ⊤} t]

Figure 6: The relationship between arrow types

normal forms and together with Subject Reduction (Theorem 9) this ensures the soundness of the type system.

Figure 6 shows the ordering of arrow types and how the constructs trust, distrust and check would fit into it.

3.2 Subject Reduction

The main result of this section is the Subject Reduction theorem. The theorem states that types are invariant under reduction.

Lemma 8 (Substitution) If A[x ↦ ⟨s, u⟩] ⊢ E : t # v and A ⊢ F : s # u then A ⊢ E[F/x] : t # v.

Proof. By induction on the derivation of A[x ↦ ⟨s, u⟩] ⊢ E : t # v. □

Theorem 9 (Subject Reduction) If A ⊢ E : t # u and E → F then A ⊢ F : t # u.

Proof. By induction on the structure of the derivation of E → F and by cases on the structure of E. The (Reflex) case is trivial. In the (Sub) cases the result follows directly from the induction hypothesis. The type rule (Sub) is applicable in all cases, so when reasoning “backwards” (as in “when α E has type t then E must have type t′”) we must take care to handle the case where the (Sub) type rule was used in between.

For the contraction rules we show just two illustrative cases, the remaining cases are extremely similar. Suppose the last rule used in the derivation of E → F was

\frac{E_{1} → trust F_{1}}{E = trust E_{1} → trust F_{1} = F} (Trust Contraction)

By assumption we have A ⊢ trust E_{1} : t # u so by the rules we must have A ⊢ E_{1} : t′ # u′ where t′ ≤ t. By the induction hypothesis we now get A ⊢ trust F_{1} : t′ # u′ and again we must have A ⊢ F_{1} : t′′ # u′′ where t′′ ≤ t′. Now by the (Trust) rule of the type system we get A ⊢ trust F_{1} : t′′ # ⊥ and finally by (Sub) we get A ⊢ trust F_{1} : t # u as required.

Another case: Suppose the last rule used in the derivation of E → F was

\frac{E_{1} → distrust F_{1}}{E = distrust E_{1} → distrust F_{1} = F} (Distrust Contraction)

By assumption we know A ⊢ distrust E_{1} : t # u and therefore u = ⊤, so by the rules we must have A ⊢ E_{1} : t′ # u′ where t′ ≤ t. From the induction hypothesis we get A ⊢ distrust F_{1} : t′ # u′. By the (Distrust) rule we must have A ⊢ F_{1} : t′′ # u′′ where t′′ ≤ t′ and u′ = ⊤. By the (Distrust) rule we now get A ⊢ distrust F_{1} : t′′ # ⊤ which via (Sub) yields the required result.

Regarding application: If E = E_{1}E_{2} → F_{1}F_{2} = F then the result follows by two applications of the induction hypothesis.

If the last rule used in the derivation of E → F was

\frac{E_{1} → F_{1} E_{2} → F_{2}}{E = (distrust(λx.E_{1}))E_{2} → distrust F_{1}[F_{2}/x] = F} (Application)

then by assumption A ⊢ (distrust(λx.E_{1}))E_{2} : t # u. By definition of the type rules this must mean that A ⊢ distrust(λx.E_{1}) : s_{1} ⟶^{v_{1} v_{2}} t_{1} # w_{1} and A ⊢ E_{2} : s_{1} # v_{1} where

t_{1} ≤ t and v_{2} ⊔ w_{1} ≤ u. Again, we must also have A ⊢ λx.E_{1} : s′_{1} ⟶^{v′_{1} v′_{2}} t′_{1} # w′_{1} and it

must be case that w_{1} = ⊤ and thus u = ⊤. Also t′_{1} ≤ t_{1}, v′_{2} ≤ v_{2}, v_{1} ≤ v′_{1} and s_{1} ≤ s′_{1}. Once again by the type rules we must have A[x ↦ ⟨s′′_{1}, v′′_{1}⟩] ⊢ E_{1} : t′′_{1} # v′′_{2} where s′_{1} ≤ s′′_{1}, v′_{1} ≤ v′′_{1}, t′′_{1} ≤ t′_{1} and v′′_{2} ≤ v′_{2}. By the (Sub) rule we get A ⊢ E_{2} : s′′_{1} # v′′_{1}.

We can now apply the induction hypothesis to get A[x ↦ ⟨s′′_{1}, v′′_{1}⟩] ⊢ F_{1} : t′′_{1} # v′′_{2} and A ⊢ F_{2} : s′′_{1} # v′′_{1}. By the Substitution lemma (Lemma 8) we now get A ⊢ F_{1}[F_{2}/x] : t′′_{1} # v′′_{2}. By the (Distrust) rule we get A ⊢ distrust F_{1}[F_{2}/x] : t′′_{1} # ⊤ and by (Sub) we get the desired result as t′′_{1} ≤ t′_{1} ≤ t_{1} ≤ t.

The case without distrust is similar. □

3.3 Comparison with the Curry System

Our type system may be viewed as a restriction of the classic Curry type system for λ-calculus. This notion is formalized in the following. Define the erasure | · | of a term as:

|x|  = x  |λx.E|  = λx.|E|
|E_{1}E_{2}|  = |E_{1}||E_{2}|  |trust E| = |E|
|distrust E| = |E|  |check E| = |E|

and likewise the erasure of a trust-type as:

|base| = base  |s ⟶^{u v} t| = |s| ⟶ |t|.

The notion of erasure is extended pointwise to environments: |A|(x) = |t| if and only if A(x) = ⟨t, u⟩.

The Curry type rules for erased expressions are defined in Figure 7. Here type assumptions A map program identifiers to Curry types.

A ⊢_{C} x : t if x ∈ dom(A) and A(x) = t

\frac{A[x ↦ s] ⊢_{C} E_{1} : t}{A ⊢_{C} λx.E_{1} : s ⟶ t}  \frac{A ⊢_{C} E_{1} : s ⟶ t A ⊢_{C} E_{2} : s}{A ⊢_{C} E_{1}E_{2} : t}

Figure 7: The Curry type system.

Lemma 10 (Erasure) If s and t are trust types and s ≤ t then |s| = |t|.

Proof. For base-types s ≤ t implies s = t. For arrow types note that by definition of ≤, s and t must have the same arrow structure. So the result follows by an induction on the common structure of s and t. □

Theorem 11 If A ⊢ E : t # u then |A| ⊢_{C} |E| : |t|.

Proof. By induction on the derivation of A ⊢ E : t # u.

E = x: By assumption we have x ∈ dom(A) and ⟨t, u⟩ = A(x). Thus x ∈ dom(|A|) and |A|(x) = |t|.

E = α E_{1}: Here α ∈ {trust, distrust, check}. By the definition of erasure, |E| = |E_{1}| and the result follows by induction.

E = λx.E_{1}: By assumption we must have A[x ↦ ⟨s_{1}, v_{1}⟩] ⊢ E_{1} : t_{1} # u_{1} where s_{1} ⟶^{v_{1} u_{1}} t_{1} ≤ t. By the induction hypothesis |A|[x ↦ |s_{1}|] ⊢_{C} |E_{1}| : |t_{1}|. By the lambda rule in the Curry system we get |A| ⊢_{C} λx.|E_{1}| : |s_{1}| ⟶ |t_{1}|. By definition of erasure and the Erasure lemma we get the desired result.

E = E_{1}E_{2}: By assumption we must have A ⊢ E_{1} : s_{1} ⟶^{v_{1} u_{1}} t_{1} # w_{1} and A ⊢ E_{2} : s_{1} # v_{1} where t_{1} ≤ t and u_{1} ⊔ w_{1} ≤ u. From the induction hypothesis we get |A| ⊢_{C} |E_{1}| : |s_{1}| ⟶ |t_{1}| and |A| ⊢_{C} E_{2} : |s_{1}|. By the application rule in the Curry system we get |A| ⊢_{C} |E_{1}E_{2}| : |t_{1}|. Finally by the Erasure lemma we get the desired result.

□

If there are no subterms of the form check E in a program and the erasure of the program is Curry typable then the program is trust-typable and all the trusts may be chosen as ⊤. This idea is formalized below. Define the decoration of a Curry type as

Δ(base)  = base
Δ(s ⟶ t) = Δs ⟶^{⊤ ⊤} Δt

Extend decorations to Curry type assumptions: (ΔA)(x) = ⟨Δt, ⊤⟩ whenever A(x) = t. Clearly |Δ t| = t.

E → E (Reflex) \frac{E → E′}{λx.E → λx.E′} (Sub)

\frac{E → E′  F → F′}{\begin{aligned}EF & → & E′F′ \\ (λx.E)F & → & E′[F′/x] \end{aligned}} (Application)

Figure 8: Reductions in the ordinary λ-calculus.

Theorem 12 If A ⊢_{C} |E| : t and E contains no subterm of the form check E′ then ΔA ⊢ E : Δt # ⊤.

Proof. By induction on the structure of E.

E = x: By assumption we have x ∈ dom(A) and A(x) = t, so x ∈ dom(ΔA) and (ΔA)(x) = ⟨Δt, ⊤⟩. By the (Var) rule we get ΔA ⊢ x : Δt # ⊤.

E = λx.E_{1}: By the assumptions and the Curry rules we must have A[x ↦ s_{1}] ⊢_{C} |E_{1}| : t_{1} where s_{1} ⟶ t_{1} = t. By induction Δ(A[x ↦ s_{1}]) ⊢ E_{1} : Δt_{1} # ⊤. By the (Lambda) and (Sub) rules of the trust

system, we get ΔA ⊢ λx.E_{1} : Δs_{1} ⟶^{⊤ ⊤} Δt_{1} # ⊤ as required.

E = E_{1}E_{2}: By the assumptions and the Curry rules we must have A ⊢_{C} |E_{1}| : s ⟶ t and A ⊢_{C} |E_{2}| : s. By the induction hypothesis we get ΔA ⊢ E_{1} : Δ(s ⟶ t) # ⊤ and ΔA ⊢ E_{2} : Δs # ⊤. By the (App) rule we then

get ΔA ⊢ E_{1}E_{2} : Δt # ⊤ as required.

E = trust E_{1}: Since |trust E_{1}| = |E_{1}| and A ⊢_{C} |E_{1}| : t by the induction hypothesis one gets ΔA ⊢ E_{1} : Δt # ⊤. Now we may apply the (Trust) and (Sub) rules to get ΔA ⊢ trust E_{1} : Δt # ⊤ as wanted. The case for distrust is similar.

This exhausts the possible cases since E was assumed check-free. □

3.4 Simulation

The aim of this section is to show that for well-typed terms one may erase all the trust, distrust and check constructs and reduce expressions according to the ordinary λ-calculus as displayed in Figure 8 (this is taken from Definition 3.2.3 in [2].) We use the same symbol for this reduction relation as for our own and it will be clear from the context which reduction relation is meant. Note that the relation defined in Figure 8 is a subrelation of the reduction relation defined in Figure 2.

More formally the two following simulation theorems show that for well-typed terms, reduction and erasure commute: | · |∘ →^{∗} = →^{∗} ∘| · |.

In terms of implementation this means that after typechecking an interpreter may erase all trust tags and run the program without tags, thus no run-time performance penalty is paid.

Lemma 13 (Step) If E →^{∗} α F (α may be empty) and there is a reduction rule

\frac{E_{1} → α F_{1}}{β E_{1} → γ F_{1}}

then β E →^{∗} γ F.

Proof. By induction on the length of the sequence E →^{∗} α F. If E = α F then by (Reflex) we have E → α F and we may apply the rule to get β E → γ F and since →⊆→^{∗} this is the required result.

Otherwise the last step in the reduction sequence E →^{∗} α F must look like E′ → α F, where E →^{∗} E′ and E′ ≠ α F. Now we apply the rule mentioned in the statement of the lemma:

\frac{E′ → α F}{β E′ → γ F}

By the induction hypothesis one gets (via the (Sub) rule and using β for γ): E →^{∗} E′ implies β E →^{∗} β E′. By appending the two reductions we get β E →^{∗} γ F as we wanted. In effect we get this derived rule:

\frac{E_{1} →^{∗} α F_{1}}{β E_{1} →^{∗} γ F_{1}}

Similarly, from

\frac{E → G F → H}{EF → GH}  we get  \frac{E →^{∗} G F →^{∗} H}{EF →^{∗} GH}
□

Some notation: We write E_{0} = CTD^{∗}F to mean that E_{0} is produced by the following grammar, where F is an ordinary term.

E_{0} ::= check E_{0} | trust E_{0} | distrust E_{0} | F

We also write distrust^{?} E to mean either E or distrust E.

Lemma 14 (CTD) If E = CTD^{∗}(λx.E_{1}), A ⊢ E : t # u and E_{1} →^{∗} F_{1} then E →^{∗} distrust^{?} (λx.F_{1}).

Proof. By induction on the length of the CTD sequence. Suppose that

CTD^{∗}λx.E_{1} = (α (β … (λx.E_{1}) …)).

In the base case (the empty sequence) E_{1} →^{∗} F_{1} implies (via Sub and Step) that λx.E_{1} →^{∗} λx.F_{1}.

Otherwise, there are two cases depending on whether (β …) reduces to a lambda or a distrusted lambda.

Suppose that (β …) →^{∗} λx.F_{1} by the induction hypothesis then via the Step lemma and (Lambda Contraction):

α = trust: (trust (β …)) →^{∗} λx.F_{1}.

α = distrust: (distrust (β …)) →^{∗} distrust λx.F_{1}.

α = check: (check (β …)) →^{∗} λx.F_{1}.

Finally, suppose that (β …) →^{∗} distrust λx.F_{1} by the induction hypothesis then via the Step lemma and (Distrust Contraction):

α = trust: (trust (β …)) →^{∗} trust λx.F_{1} and via a (Lambda Contraction) step: trust λx.F_{1} → λx.F_{1}.

α = distrust: (distrust (β …)) →^{∗} distrust λx.F_{1}.

α = check: As E is well-typed this case cannot occur since check(distrust E_{1}) is untypable.

□

Theorem 15 (Simulation 1) If A ⊢ E : t # u and |E| → F then there is a term G such that E →^{∗} G and |G| = F.

Proof. By structural induction on E.

E = x: Here |E| = E and the only applicable rule is (Reflex), thus we get E = F = G.

E = α E_{1}, where α ∈ {trust, distrust, check}. Here we have |E| = |E_{1}|, A ⊢ E_{1} : t_{1} # u_{1} and |E| = |E_{1}| → F. So by the induction hypothesis there is a G_{1} such that E_{1} →^{∗} G_{1} and |G_{1}| = F. By the Step lemma we can deduce:

\frac{E_{1} →^{∗} G_{1}}{E = α E_{1} →^{∗} α G_{1} = G} (Sub)

and the erasure of G is F as required.

E = λx.E_{1}: By the assumptions we must have A[x ↦ ⟨t_{1}, u_{1}⟩] ⊢ E_{1} : t_{2} # u_{2}. Also, |E| = λx.|E_{1}| and F = λx.F_{1}. By the nature of the reduction rules, we must have |E_{1}| → F_{1}. By the induction hypothesis we know there is a G_{1} such that E_{1} →^{∗} G_{1} and |G_{1}| = F_{1}. By the (Sub) rule and the Step lemma we get

\frac{E_{1} →^{∗} G_{1}}{E = λx.E_{1} →^{∗} λx.G_{1} = G} (Sub)

and |G| = λx.|G_{1}| = λx.F_{1} = F as required.

E = E_{1}E_{2}: By the assumptions E is well-typed thus E_{1} and E_{2} are well-typed. By definition of the reduction rules we must have |E_{1}| → F_{1} and |E_{2}| → F_{2}. By the induction hypothesis we get G_{1} and G_{2} such that E_{1} →^{∗} G_{1}, E_{2} →^{∗} G_{2}, |G_{1}| = F_{1} and |G_{2}| = F_{2}.

There are two cases depending on the form of |E|:

|E| = not a β-redex: Here F = F_{1}F_{2} where |E_{1}| → F_{1} and |E_{2}| → F_{2} so by the reasoning above |G_{1}G_{2}| = F and we are done.

|E| = (λx.H_{1})H_{2}: If F = (λx.F′_{1})F_{2} where H_{1} → F′_{1} and H_{2} → F_{2} then also |E_{1}| = λx.H_{1} → λx.F′_{1} = F_{1} by (Sub). By the above statements and the Step lemma we get E →^{∗} G_{1}G_{2} and |G_{1}G_{2}| = F. Otherwise a β-reduction happens. Here H_{1} → F′_{1}, H_{2} → F_{2} and F = F′_{1}[F_{2}/x]. Clearly, E_{1} must have form CTD^{∗}(λx.Q_{1}) where |Q_{1}| = H_{1}. By the induction hypothesis there is a Q′_{1} such that Q_{1} →^{∗} Q′_{1} and |Q′_{1}| = F′_{1}. By the CTD lemma E_{1} →^{∗} distrust^{?} (λx.Q′_{1}) and by the Subject Reduction theorem (Theorem 9) we get that distrust^{?} (λx.Q′_{1}) is well-typed. We may now reason as follows:

\frac{E_{1} →^{∗} distrust^{?} (λx.Q′_{1}) E_{2} →^{∗} G_{2}}{E_{1}E_{2} →^{∗} (distrust^{?} (λx.Q′_{1}))G_{2}} (Sub + Step)

and

\frac{Q′_{1} → Q′_{1} G_{2} → G_{2}}{(distrust^{?} (λx.Q′_{1}))G_{2} → distrust^{?} Q′_{1}[G_{2}/x]} (Application)

since |Q′_{1}| = F′_{1} and |G_{2}| = F_{2}:

|distrust^{?} Q′_{1}[G_{2}/x]| = |Q′_{1}[G_{2}/x]| = F′_{1}[F_{2}/x] = F

as required.

This concludes the proof of the Simulation theorem. □

Theorem 16 (Simulation 2) If E → F then |E| → |F |.

Proof. By induction on the derivation of E → F.

• If E → F by (Reflex) then |E| = |F | and the result holds trivially.

• If E → F by the (Sub) rule. The subterm(s) E_{i} of E then must reduce E_{i} → F_{i} and by the induction hypothesis |E_{i}| → |F_{i}|. We may now apply the (Sub) rule to these erased terms and get |E| → |F |.

• Let α, β, γ ∈ {trust, distrust, check}. If the last rule in the derivation of E → F was

\frac{E_{1} → α F_{1}}{E = β E_{1} → γ F_{1} = F} (α-Contraction)

then |E| = |E_{1}| and |F | = |F_{1}|. By the induction hypothesis we know |E_{1}| → |F_{1}| which is the desired result.

• If the last rule used in the derivation of E → F was

\frac{E_{1} → λx.F_{1}}{E = α E_{1} → λx.F_{1} = F} (Lambda Contraction)

where α ∈ {trust, check} then by the induction hypothesis we get |E_{1}| → λx.|F_{1}| and since |E| = |E_{1}| and |F | = λx.|F_{1}| this is the desired result.

• If the last rule used in the derivation of E → F was

\frac{E_{1} → F_{1} E_{2} → F_{2}}{E = (distrust λx.E_{1})E_{2} → distrust F_{1}[F_{2}/x] = F} (Application)

We have |E| = (λx.|E_{1}|)|E_{2}| and |F | = |F_{1}|[|F_{2}|/x]. By the induction hypothesis |E_{1}| → |F_{1}| and |E_{2}| → |F_{2}|. We may now apply the (Application) rule to get the desired result. The case for the trusted lambda is similar.

□

3.5 Strong Normalization

In Curry typed λ-calculus all typable terms are strongly normalizing, i.e. they reduce to a normal form. This result carries over to our language, essentially since our type system admits fewer terms than the Curry system. On the other hand we have terms not occurring in the standard λ-calculus and a lot more reduction rules so this requires a proof.

Theorem 17 (Strong Normalization) If A ⊢ E : t # u then there is a normal form G′ such that E → G′.

Proof. By Theorem 11, A ⊢ E : t # u implies |A| ⊢_{C} |E| : |t|. By the Strong Normalization theorem for Curry typed λ-calculus [7] there is a Curry normal form F such that |E| →^{∗} F. We can now apply the first Simulation theorem (Theorem 15) to obtain a term G such that E →^{∗} G and |G| = F.

As |G| = F is a normal form it has no β-redexes, but in G some other reductions may be applicable. Because of the Church-Rosser theorem, only using contraction and Sub rules will not block any possible other reduction that might be applicable, so let G →^{∗} G′ be such a reduction sequence. In all the contraction rules the number of {check, trust, distrust} constructs decrease with one. Writing →^{!} for the irreflexive part of the → relation we have that in the sequence G →^{!} G_{1} →^{!} ⋯ →^{!} G′ there are a finite number of steps (less than the size of G). Thus we may take G′ such that in G′ no more of these non-β reductions are applicable.

After reaching G′ can it be the case that the contractions revealed a β-redex in G′? Suppose for a contradiction that this is the case. This means that G′ has a subterm of the form (distrust^{?} λx.G_{1})G_{2}. So we have G′ → G′′ by reducing this redex. By Theorem 16 this means that F = |G′| →^{!} |G′′| and clearly |G′′| ≠ F. But this contradicts the fact the F could be reduced no further! So it cannot be the case that the final contractions reveal a β-redex, and thus G′ is a normal form. □

4 Type Inference

The type inference problem is:

Given an untyped program E, is E typable? If so, annotate it.

From Theorem 11 we have that trust typing implies Curry typing. Our type inference algorithm works by first checking if the program has a Curry type and then checking a condition that only involves trust values.

4.1 Constraints

The type inference problem can be rephrased in terms of solving a system of constraints.

Definition 18 Given two disjoint denumerable sets of variables V_{y} and V_{r}, a Tsystem is a pair (C, D) where:

• C is a finite set of inequalities X ≤ X′ between constraint expressions, where X and X′ are of the forms V or V ⟶^{W W′} V′, and where V, V′ ∈ V_{y} and W, W′ ∈ V_{r}.

• D is a finite set of constraint of the forms W ≤ W′, W = ⊥, or W = ⊤, where W, W′ ∈ V_{r}.

A solution for a T-system is a pair of maps (δ, φ), where δ maps variables in V_{y} to types, and where φ maps variables in V_{r} to trusts, such that all constraints are satisfied.

If φ satisfies all constraints in D, we say that D has solution φ. □

Given a λ-term E, assume that E has been α-converted so that all bound variables are distinct. Let V_{y} be the set consisting of:

• A variable [[F]]_{y} for each occurrence of a subterm F of E; and

• A variable x_{y} for each λ-variable x occurring in E.

(The notation [[F]]_{y} is ambiguous because there may be more than one occurrence of F in E. However, it will always be clear from context which occurrence is meant.) Intuitively, [[F]]_{y} denotes the type of F after the use of subsumption. Moreover, x_{y} denotes the type assigned to the bound variable x.

Let V_{r} be the set consisting of:

• A variable [[F]]_{r} for each occurrence of a subterm F of E; and

• A variable x_{r} for each λ-variable x occurring in E.

• A variable ⟨GH⟩_{r} for each occurrence of an application GH in E.

(As before, the notation [[F]]_{r} is ambiguous.) Intuitively, [[F]]_{r} denotes the trust value of F after the use of subsumption. Moreover, x_{r} denotes the trust value assigned to the bound variable x. Finally, ⟨GH⟩_{r} denotes the trust value of GH before the use of subsumption.

From the λ-term E, we generate the T-system (C, D) where:

For each

occurrence in E We have in C

We have in D

x  x_{y} ≤ [[x]]_{y}  x_{r} ≤ [[x]]_{r}
λx.F  x_{y} ⟶^{x_{r} [[F]]_{r}} [[F]]_{y} ≤ [[λx.F]]_{y}
GH  [[G]]_{y} ≤ [[H]]_{y} ⟶^{[[H]]_{r} ⟨GH⟩_{r}} [[GH]]_{y} \begin{aligned}[[G]]_{r} & ≤ & [[GH]]_{r} \\ ⟨GH⟩_{r} & ≤ & [[GH]]_{r} \end{aligned}
trust F  [[F]]_{y} ≤ [[trust F]]_{y}
distrust F  [[F]]_{y} ≤ [[distrust F]]_{y}  [[distrust F]]_{r} = ⊤
check F  [[F]]_{y} ≤ [[check F]]_{y}  [[F]]_{r} = ⊥

Denote by T (E) the T-system of constraints generated from E in this fashion. The solutions of T (E) correspond to the possible type annotations of E in a sense made precise by Theorem 21.

Let A be a trust-type environment. If δ is a function assigning types to variables in V_{y} and φ a function assigning trusts to variables in V_{r}, we say that (δ, φ) extend A if for every x in the domain of A, we have A(x) = ⟨δ(x_{y}), φ(x_{r})⟩.

As a shorthand in the following, we write (δ, φ) ⊧ (C, D) to mean that (δ, φ) is a solution to the constraints (C, D). Define also, for two functions δ and δ′ agreeing on dom(δ) ∩ dom(δ′), δ + δ′ as the unique function on dom(δ) ∪ dom(δ′) that agree with the two functions on their respective domains.

Lemma 19 (Soundness) If (δ, φ) ⊧ T (E), and δ, φ extend A then A ⊢ E : δ([[E]]_{y}) # φ([[E]]_{r}).

Proof. By induction on the structure of E. □

Lemma 20 (Completeness) If A ⊢ E : t # u then there is a solution (δ, φ) ⊧ T (E) with δ and φ extending A, and δ([[E]]_{y}) = t and φ([[E]]_{r}) = u.

Proof. By induction on the derivation of A ⊢ E : t # u.

E = x: As A ⊢ x : t # u we must have x ∈ dom(A), A(x) = ⟨t′, u′⟩ and t′ ≤ t, u′ ≤ u. In this case T (E) = {x_{y} ≤ [[x]]_{y}, x_{r} ≤ [[x]]_{r}}. Put δ(x_{y}) = t′ and φ(x_{r}) = u′ so that (δ, φ) extends A. Finally assign δ([[x]]_{y}) = t and φ([[x]]_{r}) = u to satisfy the constraints.

E = λx.F: By the type rules we must have A[x ↦ ⟨s, v⟩] ⊢ F : s′ # u′ where s ⟶^{v u′} s′ ≤ t. By the induction hypothesis we get (δ, φ) ⊧ T (F), δ([[F]]_{y}) = s′, φ([[F]]_{r}) = u′, and (δ, φ) extends A[x ↦ ⟨s, v⟩]. Now assign δ′ = δ[[[λx.F]] ↦ t] and φ′ = φ[[[λx.F]] ↦ u]. Now check that s ⟶^{v u′} s′ ≤ t implies

δ′(x_{y}) ⟶^{φ′(x_{r}) φ′([[F]]_{r})} δ′([[F]]_{y}) ≤ δ′([[λx.F]]_{y})

as required. So we get (δ′, φ′) ⊧ T (E).

E = GH: By the type rules we must have A ⊢ G : s′ ⟶^{u′ v′} t′ # w′, A ⊢ H : s′ # u′ where t′ ≤ t and v′ ⊔ w′ ≤ u. By the induction hypothesis we get (δ, φ) ⊧ T (G) and (δ′, φ′) ⊧ T (H) and both solutions extending A which means that they agree on their common domain (the x_{y}’s and the x_{r}’s in dom(A)). The definition of T (E) says

\begin{matrix}T (E) = T (G) ∪ T (H) ∪ ( & \{[[G]]_{y} ≤ [[H]]_{y} ⟶^{[[H]]_{r} ⟨GH⟩_{r}} [[GH]]_{y}\}, \\ \{[[G]]_{r} ≤ [[GH]]_{r}, ⟨GH⟩_{r} ≤ [[GH]]_{r}\}) . \end{matrix}

Define δ′′ = δ + δ′[[[GH]]_{y} ↦ t] and φ′′ = φ + φ′[[[GH]]_{r} ↦ u, ⟨GH⟩_{r} ↦ v′]. Now, (δ′′, φ′′) ⊧ T (E) because

δ([[G]]_{y}) = s′ ⟶^{u′ v′} t′ ≤ s′ ⟶^{u′ v′} t = δ′([[H]]_{y}) ⟶^{φ′([[H]]_{r}) φ′′(⟨GH⟩_{r})} δ′′([[GH]]_{y})

φ([[G]]_{r}) = w′ ≤ u = φ′′([[GH]]_{r})
φ′′(⟨GH⟩_{r}) = v′ ≤ u = φ′′([[GH]]_{r}) .

and clearly (δ′′, φ′′) extend A.

E = check F: From the type rules we must have A ⊢ F : t′ # ⊥ where t′ ≤ t. By the induction hypothesis we get (δ, φ) ⊧ T (F), δ([[F]]_{y}) = t′, and φ([[F]]_{r}) = ⊥. Now, T (E) = T (F) ∪ {[[F]]_{y} ≤ [[check F]]_{y}, [[F]] = ⊥}. Put δ′ = δ[[[check F]]_{y} ↦ t] and φ′ = φ[[[check F]]_{y} ↦ u].

Clearly, δ′, φ′ extend A, δ′([[F]]_{y}) ≤ δ′([[check F]]_{y}), and φ′([[F]]_{r}) = ⊥ as required. The cases for trust and distrust are very similar.

□

Theorem 21 The judgement A ⊢ E : t # u is derivable if and only if there exists a solution (δ, φ) of T (E) with (δ, φ) extending A such that δ([[E]]_{y}) = t and φ([[E]]_{r}) = u. In particular, if E is closed, then E is typable with type t and trust u if and only if there exists a solution (δ, φ) of T (E) such that δ([[E]]_{y}) = t and φ([[E]]_{r}) = u.

Proof. Combine Lemma 19 and 20. □

4.2 Algorithm

Definition 22 Given a T-system (C, D), define the deductive closure (C̄, D̄) to be the smallest T-system such that:

• C ⊆ C̄.

• D ⊆ D̄.

• If V_{1} ⟶^{W_{1} W_{2}} V_{2} ≤ V′_{1} ⟶^{W′_{1} W′_{2}} V′_{2} is in C̄, then V′_{1} ≤ V_{1} and V_{2} ≤ V′_{2} are in C̄, and

W′_{1} ≤ W_{1} and W_{2} ≤ W′_{2} are in D̄.

• If X_{1} ≤ X_{2} and X_{2} ≤ X_{3} are in C̄, then X_{1} ≤ X_{3} is in C̄.

□

Lemma 23 (C, D) and (C̄, D̄) have the same solutions.

Proof. Since C ⊆ C̄ and D ⊆ D̄, any solution of (C̄, D̄) is also a solution of (C, D). The converse can be proved by induction on the construction of (C̄, D̄). □

If we remove all mentioning of trust and subtyping from the type rules in figure 5 and from the constraints defined earlier in this section, we obtain two equivalent formulations of Curry typability [16]. Clearly, E is Curry typable if and only if |E| is Curry typable. The constraint system (written out below) that expresses Curry typability will be denoted Curry(E).

For each

occurrence in E

We have in Curry(E)

x  x_{y} = [[x]]_{y}
λx.F  [[λx.F]]_{y} = x_{y} → [[F]]_{y}
GH  [[G]]_{y} = [[H]]_{y} → [[GH]]_{y}
trust F  [[trust F]]_{y} = [[F]]_{y}
distrust F  [[distrust F]]_{y} = [[F]]_{y}
check F  [[check F]]_{y} = [[F]]_{y}

If s, t are trust types such that |s| = |t|, then define the operators ⊔^{|s|} and ⊓^{|t|} as follows.

s ⊔^{|s|} t = \{ \begin{matrix}base & if s = t = base \\ (s_{1} ⊓^{|s_{1}|} t_{1}) ⟶^{u_{1}⊓v_{1} u_{2}⊔v_{2}} (s_{2} ⊔^{|s_{2}|} t_{2}) & if s = s_{1} ⟶^{u_{1} u_{2}} s_{2} \\ & and t = t_{1} ⟶^{v_{1} v_{2}} t_{2} \end{matrix}

s ⊓^{|s|} t = \{ \begin{matrix}base & if s = t = base \\ (s_{1} ⊔^{|s_{1}|} t_{1}) ⟶^{u_{1}⊔v_{1} u_{2}⊓v_{2}} (s_{2} ⊓^{|s_{2}|} t_{2}) & if s = s_{1} ⟶^{u_{1} u_{2}} s_{2} \\ & and t = t_{1} ⟶^{v_{1} v_{2}} t_{2} . \end{matrix}

If t_{1}, …, t_{n} are trust types, and s is a Curry type such that |t_{i}| = s for all i ∈ 1..n, then define ⨆_{i}^{s} t_{i} = t_{1} ⊔^{s} … ⊔^{s} t_{n}. If t is a Curry type, define

small(base) = base  big(base) = base
small(s → t) = big(s) ⟶^{⊤ ⊥} small(t)  big(s → t) = small(s) ⟶^{⊥ ⊤} big(t)

If s is a trust type and t is a Curry type such that |s| = t, then s ⊔^{t} small(t) = s and s ⊓^{t} big(t) = s. In other words, small(t) is the least trust type with erasure t.

For each a constraint expression X define

L(C, X) = {V_{1} ⟶^{W_{1} W′_{1}} V′_{1} | V_{1} ⟶^{W_{1} W′_{1}} V′_{1} ≤ X is in C̄} .

Intuitively, L(C, X) is the set of syntactic lower bounds for X.

We also define the erasure of a constraint expression used in C, mapping trusttype constraint expressions to Curry constraint expressions:

|V | = V
|V ⟶^{W W′} V′| = |V | → |V′|

where V, V′ ∈ V_{y} and W, W′ ∈ V_{r}.

Lemma 24 If T (E) = (C, D), and ψ is a solution to Curry(E), and X_{1} ≤ X_{2} is a constraint in C̄, then ψ(|X_{1}|) = ψ(|X_{2}|).

Proof. By induction on the construction of C̄. □

Theorem 25 Suppose T (E) = (C, D). Then T (E) is solvable if and only if E is Curry typable and D̄ is solvable.

Proof. Suppose first that T (E) is solvable. By Theorem 21, E is trust typable. It follows from Theorem 11 and the remark above that E is Curry typable, and from Lemma 23 that D̄ is solvable.

For the reverse implication, suppose that Curry(E) has solution ψ and that D̄ has solution φ. We define δ inductively in the Curry types of the constraint variables.

δ(V) = if ψ(|V |) = base then base

else let {V_{i} ⟶^{W_{i} W′_{i}} V′_{i}} = L(C, V) ∪ {small(ψ(|V |))}

in ⨆_{i}^{ψ(|V |)}(δ(V_{i}) ⟶^{φ(W_{i}) φ(W′_{i})} δ(V′_{i}))

To see that δ is well-defined, we need that the Curry types of the variables V_{i} and V′_{i} are of strictly less size than the Curry type of V. For (V_{i} ⟶^{W_{i} W′_{i}} V′_{i}) ∈ L(C, V),

we get by Lemma 24 that ψ(|V_{i} ⟶^{W_{i} W′_{i}} V′_{i}|) = ψ(|V |) = s → t for some s, t. This means that ψ(|V_{i}|) = s and ψ(|V′_{i}|) = t which are both of smaller size than s → t, so δ is well-defined.

To see that (δ, φ) is a solution of T (E), consider an inequality X_{1} ≤ X_{2} in C. If ψ(|X_{1}|) = base, then by Lemma 24, ψ(|X_{2}|) = base, δ(X_{1}) = δ(X_{2}) = base, thus δ(X_{1}) ≤ δ(X_{2}) as required.

In case ψ(|X_{1}|) = s → t, we have by Lemma 24 that ψ(|X_{2}|) = s → t and since C̄ is transitively closed we get L(C, X_{1}) ⊆ L(C, X_{2}) so δ(X_{1}) ≤ δ(X_{2}) as required.

□

Using the characterization of Theorem 25, we get a type inference algorithm:

Input: A λ-term E of size n.
1: Construct T (E) = (C, D) (in log space).
2: Close (C, D), yielding (C̄, D̄) (in O(n^{3}) time, see for example [15]).
3: Check if E is Curry typable (in O(n) time).
4: Check if D̄ is solvable (in O(n^{2}) time).
5: If E is Curry typable and D̄ is solvable,

then output “typable” else output “not typable”.

The entire algorithm requires O(n^{3}) time. To construct an annotation of a typable program, we can use the construction of the second half of the proof of Theorem 25.

5 Extensions and Related Work

In this section we discuss several extensions of the type system and related work.

Recursion. The type system can be extended to handle recursion by adding a rec rule. In the (untyped) reduction system, the rec combinator can be coded with the classical Y combinator: rec x.E ≡ Y(λx.E). The following reduction rule is a derived rule in the λ-calculus and in our system, and correspondingly we would have a rec rule in the type system:

\frac{E →^{∗} F}{YE →^{∗} F (YE)}  \frac{A[x ↦ ⟨t, u⟩] ⊢ E_{1} : t # u}{A ⊢ rec x.E_{1} : t # u}

Subject Reduction still holds, but Strong Normalization of course fails in this case. The type inference algorithm can also be extended in a straightforward way to deal with the rec construct.

Polymorphism. ML style let polymorphism can be achieved in the usual way by replacing let bound variables with their definition. This is of course inefficient as each definition might then be type-checked many times. The type system can be extended along the same ideas that extend Curry types to Hindley-Milner types. An extension of our type inference algorithm remains to be found.

Other Lattices. The values of trust-tags may be extended from the two point lattice used in this paper to any finite lattice. Extending the lattice to a longer linear lattice accommodates multiple levels of trust. Extensions to non-linear orderings may allow different properties of values.

Related Work. The original notion of trust analysis was presented in [14] where an abstract interpretation [4] analysis and a constraint based analysis for a simple imperative, first order, language were given. This work extends trust analysis to the higher order functional case and formalizes it in terms of a decorated type system.

Security flow analysis [5, 13, 1] aims at restricting the flow of confidential information out of a trusted computer system, dually to our analysis that aims at preventing untrustworthy information from entering into a secure facility. Also, the above analyses all deal with procedural, imperative languages without higher-order functions.

In [12] Mitchell developed the structural subtyping idea and our type system borrows some of these ideas to handle automatic coercion from trusted data to untrusted data.

Our type system extends the basic Curry types with annotations in the same spirit as Talpin and Jouvelot’s effect systems [17], Wright’s annotated types [18] and others.

The idea of accepting fewer programs than a well-known type system is in the spirit of the refinement types of [6].

Other Analyses. Without support for trust in the type system one might approximate the same effect by coding the relevant types as sums with a trusted and a distrusted variant. This has two drawbacks: the values have to be explicitly packed and unpacked each time they are used and the tags will be present at run-time which means that hackers might be able to fiddle with these tags and thereby circumvent the security measures.

As mentioned in Section 1 many other program analyses approximate information inherent in the values that exists at run-time. Strictness analysis [3, 11] aims to find out whether functions in a higher order lazy language are strict or not. This may not be a decidable property but it is nevertheless a property of a value (function). In binding time analysis [8] one aims to approximate whether a value can be computed at compile-time or not. At compile-time this is a property of the values. Also, this is something that does not change from one compilation of the same program to the next.

Another kind of analysis that looks related to trust analysis is dynamic typing or boxing/unboxing analysis [9, 10] which aims to remove type tags as much as possible in a dynamically typed language. One might be tempted to view, say, distrust as a boxing operation and trust as the corresponding unboxing operation. However, this does not explain how check should be interpreted and it doesn’t match with our application type rule, in that applying a boxed function to an argument does not necessarily result in a boxed result.

6 Conclusion

We have argued for the usefulness of so-called trust analysis to help programmers produce safer and more trustworthy software. We have presented an extension of the λ-calculus together with a reduction semantics. The reduction relation is proved Church-Rosser. Then we gave a type system that enables the static inference of the trustworthiness of values and the type system was proved to have the Subject Reduction property with respect to the semantics of our language.

Last a constraint based type inference algorithm was presented and proved correct with respect to the type system.

References

[1] Jean-Pierre Banâtre, Ciarán Bryce, and Daniel Le Metayer. Compile-time detection of information flow in sequential programs. In Dieter Gollmann, editor, Computer Security – ESORICS 94, 3rd European Symp. on Research in Comp. Security, pages 55–73. Springer-Verlag (LNCS 875), 1994.

[2] Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, 1981.

[3] Geoffrey L. Burn, Chris Hankin, and Samson Abramsky. Strictness analysis for higher-order functions. Science of Computer Programming, 7:249–278, 1986.

[4] Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Fourth ACM Symposium on Principles of Programming Languages, pages 238–252, 1977.

[5] Dorothy E. Denning and Peter J. Denning. Certifications of programs for secure information flow. Communications of the ACM, 20(7):504–512, July 1977.

[6] Tim Freeman and Frank Pfenning. Refinement types for ML. In Proc. ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation, 1991.

[7] Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and Types. Number 7 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[8] Carsten K. Gomard and Neil D. Jones. A partial evaluator for the untyped lambda-calculus. Journal of Functional Programming, 1(1):21–69, 1991.

[9] Fritz Henglein. Dynamic typing. In Proc. ESOP’92, European Symposium on Programming, pages 233–253. Springer-Verlag (LNCS 582), 1992.

[10] Fritz Henglein and Jesper Jørgensen. Formally optimal boxing. In Proc. POPL’94, 21st Annual Symposium on Principles of Programming Languages, pages 213–226, 1994.

[11] Tsung-Min Kuo and Prateek Mishra. Strictness analysis: A new perspective based on type inference. In Proc. Conference on Functional Programming Languages and Computer Architecture, pages 260–272, 1989.

[12] John Mitchell. Coercion and type inference. In Eleventh Symposium on Principles of Programming Languages, pages 175–185, 1984.

[13] Masaaki Mizuno and David Schmidt. A security flow control algorithm and its denotational semantics correctness proof. Technical Report TR-CS-90-21, Kansas State University, 1990.

[14] Peter Ørbæk. Can you trust your data? In P. D. Mosses, editor, Proc. TAPSOFT’95, Theory and Practice of Software Development, pages 575–590. Springer-Verlag (LNCS 915), 1995.

[15] Jens Palsberg. Efficient inference of object types. Information and Computation. To appear. Also in Proc. LICS’94, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 186–195, Paris, France, July 1994.

[16] Jens Palsberg and Michael I. Schwartzbach. Safety analysis versus type inference. Information and Computation, 118(1):128–141, 1995.

[17] Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245–271, 1992.

[18] David A. Wright. A new technique for strictness analysis. In Proc. TAP-SOFT’91, pages 235–258. Springer-Verlag (LNCS 494), 1991.

Recent Publications in the BRICS Report Series

RS-95-31 Jens Palsberg and Peter �rb�k. Trust in the λ-calculus. June 1995. 32 pp. To appear in Static Analysis: 2nd International Symposium, SAS ’95 Proceedings, 1995.

RS-95-30 Franck van Breugel. From Branching to Linear Metric Domains (and back). June 1995. 30 pp. Abstract appeared in Engberg, Larsen, and Mosses, editors, 6th Nordic Workshop on Programming Theory, NWPT ’6 Proceedings, 1994, pages 444-447.

RS-95-29 Nils Klarlund. An n log n Algorithm for Online BDD Re�nement. May 1995. 20 pp.

RS-95-28 Luca Aceto and Jan Friso Groote. A Complete Equational Axiomatization for MPA with String Iteration. May 1995. 39 pp.

RS-95-27 David Janin and Igor Walukiewicz. Automata for the μcalculus and Related Results. May 1995. 11 pp. To appear in Mathematical Foundations of Computer Science: 20th Int. Symposium, MFCS ’95 Proceedings, LNCS, 1995.

RS-95-26 Faith Fich and Peter Bro Miltersen. Tables should be sorted (on random access machines). May 1995. 11 pp. To appear in Algorithms and Data Structures: 4th Workshop, WADS ’95 Proceedings, LNCS, 1995.

RS-95-25 S�ren B. Lassen. Basic Action Theory. May 1995. 47 pp.

RS-95-24 Peter �rb�k. Can you Trust your Data? April 1995. 15 pp. Appears in Mosses, Nielsen, and Schwartzbach, editors, Theory and Practice of Software Development. 6th International Joint Conference CAAP/FASE, TAPSOFT ’95 Proceedings, LNCS 915, 1995, pages 575�590.

RS-95-23 Allan Cheng and Mogens Nielsen. Open Maps (at) Work. April 1995. 33 pp.

RS-95-22 Anna Ing� olfsd� ottir. A Semantic Theory for Value�Passing Processes, Late Approach, Part II: A Behavioural Semantics and Full Abstractness. April 1995. 33 pp.