Doing Keykos Style Security in Scheme

Mark Miller has reminded me of a few properties of Scheme that seemingly interfere with solving security problems. I quote from some e-mail in response to my question “How does Scheme fail to be a object capability language?”:

Global mutable state.
Implicit access to the current environment, as in the one argument variant of "load", which is still in the Scheme standard.
Mutability of cons cells makes much of the library fail to be defensively consistent, when otherwise it would be.
call/cc likewise makes many existing libraries fail to be defensively consistent. It also makes it unreasonably hard to write new stateful code that's defensively consistent.

Note that the last two bullets above are not violations of objcap *rules*, but they make objcap programming impractical.

------end of markm note-------

The standard indeed speaks of a top level environment. The configuration I imagine however is several terminals all connected to the same Scheme interpreter and Scheme state. For each terminal there is an REPL with its own unique top level environment. I don’t see in the standard just now that there must be just one top level environment; indeed the definition of scheme-report-environment calls forth a new top level environment. Presumably each top level environment initially maps car to the same procedure, but via distinct ‘locations’. My Scheme module system puts each module in its own top level; one module cannot ruin the value of car for another module.

Scheme makes it possible to provide environments for guest code that omits or tames dangerous Scheme primitives such as call/cc, eval with one argument, load, dynamic-wind, values. There may be a few more but almost all of the standard primitives are safe. In general the access to the host system environment must be attenuated.

For any intercourse between terminals it is necessary to share some locations, at least pairwise, between the top level environments. I assume below that capitalized person names are Scheme variables bound to such locations. Such bindings are somehow included in the various top level environments.

The map I propose is that Scheme’s top level environment for a particular user corresponds to the user directory associated with a user’s command environment in Keykos. Any expression typed in at the terminal is evaluated with all of the user’s authority. If the user has some source code mal that he wants to run with less authority, he may type

(eval `(let (
   (input (quote ,my-file))
   (load (lambda (fn) (write (list "he wants to load" fn))))
  ) ,mal) (scheme-report-environment 5))

This causes the suspect program mal to run in the standard environment augmented to bind input to the value denoted in my space by my-file. If program mal should invoke load a report of the requested file will be made. Most or all of the standard IO procedures such as call-with-input-file should generally be replaced as well.

Regarding Markm’s points on the last two bullets, I would add that they make any complex collection of code, such as a library, not just “objcap programming”, unduly brittle. A similar scandal is that compiling Scheme code must be continuously on guard that the meaning of the variable ‘car’ is stable.