Short cut into the lambda calculus and Security

This note attempts a crude introduction to my favorite ideas in Rees’ paper. The key concepts are very familiar to the Scheme or the Smalltalk programmer. They will be familiar to some users of languages where procedures are first class values, such as PL/I, Algol68, gcc. My examples will be in Scheme for my knowledge of Smalltalk is entirely theoretical.

Imagine a computer with several terminals, each consisting of a mouse, keyboard and screen. Each terminal is controlled by one user. The several users trust each other, but only to a degree. The machine runs a Scheme space and provides a distinct TLE (top level environment, defined here) and REPL (read-eval-print loop) for each terminal. Even if the Scheme values rooted in the several TLEs inhabit the same virtual address space, they do not link to each other for mutable values accessible from the initial TLEs are disjoint and no action can break this isolation. (set! car '()) executed in one REPL damages only programs spawned from that terminal. Other terminals continue to use the value bound to 'car in their own TLE. Except for competing for space and time, they are worlds apart.

Now suppose that we modify the system to provide controlled communications between the TLEs. The system assigns a symbol to each terminal, and binds certain procedures to 'send and 'receive in each TLE. If user Sue performs (send 'Jim "plan" plan) and then Jim performs (receive 'Sue "plan"), Jim’s expression will yield the value bound to 'plan in Sue’s TLE. Simpler primitives to connect the worlds are possible but this one is convenient and fairly simple.

Now a number of novel security problems admit to solutions — problems that are difficult or impossible on Unix or other classic systems when none of the users is trusted by the others to be root.

The lunch voting code is a non trivial application solving a trivial social problem. Suppose that Tom is trusted and appointed to provide the voting mechanism. He defines the following values in his TLE: 

(define (mocntr) (let ((x 0)) (cons (lambda () (let ((yet #t))
     (lambda () (if yet (begin (set! yet #f) (set! x (+ 1 x)) x)))))
  (lambda () x))))
(define restaurants (list "Mandarin" "Casa Lupe" "Coffee Shop"))
(define (noontime) (let ((bb
       (map (lambda(r) (cons r (mocntr))) restaurants)))
    (for-each (lambda (e) ((cdr e) (cons "Lunchtime!" (map
      (lambda(r)(cons (car r) ((cadr r)))) bb)))) lunchAgents)
    (lambda ()(map (lambda(x) (cons (car x) ((cddr x)))) bb))))
(define lunchcrowd (list 'Jim 'Sue 'Tom 'Jennifer))

(define lunchAgents (map (lambda (eater) (let ((cell
    (cons eater (lambda (ballot) '()))))
  ('send eater "LunchAgentAppointer"
  (lambda (agent) (set-cdr! cell agent))) cell)) lunchcrowd))
Tom has sent messages to each participant. Each message includes a procedure with which the participant can appoint, and reappoint, an agent to vote each day. Sue might subscribe as follows:
(define AgentSetter (receive 'Tom "LunchAgentAppointer"))
(AgentSetter (lambda (ballot) ((cdr (assoc "Mandarin" (cdr ballot))))))
Until Sue invokes AgentSetter again she is always voting Mandarin!

But Tom does:

((receive 'Tom "LunchAgentAppointer") (lambda (bal)
(for-each (lambda (x) (if (not (string=? "Mandarin" (car x))) ((cdr x)))) (cdr bal))))
just countering Sue’s agent. At least Tom didn’t abuse his authority.

What are the security properties implicit in this code? Each eater can vote for each restaurant just once each day. He can vote for more than one. Different eaters cannot affect the vote otherwise. Eaters can provide nonterminating agents which stop the whole system, not just the voting application; they can likewise exhaust storage. This is a limitation of Scheme that would be addressed for a real system. None of the participants know the behavior of the agents of others. Tom is in a position to know how each voted. The above code will not report that to Tom, however.