A Security Kernel Based on the Lambda-Calculus

The dissertation (MIT 1995) consisted of a 50-page main part (written last) consisting of 4 chapters, followed by 80 pages of appendices, all of which had been published previously as papers or memos:

• A. A Tractable Scheme Implementation
• B. Program Mobile Robots in Scheme
• C. Scheme 48 Module System [see the Scheme 48 manual]
• D. Macros That Work
• E. Scheme 48 User's Guide [see the Scheme 48 manual]
• F. Object-Oriented Programming in Scheme

• The MIT AI memo as a postscript file. (File hosted at MIT.)
• JRM's HTML transcription of the AI memo.
• Some of the figures from the paper. If you understand these, you probably don't need to read the paper itself.

I think I used the term "authentication" incorrectly in this paper.

What the critics say

• A good word about it from Norman Hardy.
• A rave review from Mark S. Miller.
• A kind word from Richard Uhtenwoldt.

Related sites

• Norman Hardy's site on operating system security (with references to Joule, KeyKos, etc.).
• E - a scripting language and wire protocol for distributed capabilities. Very active site and mailing list (as of early 2004) with tons of introductory material and analysis.
• Mark Miller's security taxonomy.

-- Jonathan Rees