[cap-talk] Language-based safety - notes and meat)

[Lex Spoon]

Jed Donnelley <jed at nersc.gov> wrote:
> We depend on the loader rejecting any 
> >module file for which it cannot ensure that the resulting behavior will 
> >preserve safety.
> 
> Then it would seem that any such loader must either scan the "code" for 
> 'safety' prior to beginning its execution or must check it on the fly for 
> safety while interpreting it.  I'll be interested to learn more about how 
> this can be achieved.  In any case it seems that either your scanner and/or 
> your interpreter must become part of your TCB.

Yes.  Additionally, if the language semantics is good, then the scanner
can become non-existent.  E claims to have such a cap-secure semantics
and thus not require a separate scanner; Java is not cap-secure, and
there is a parallel thread talking about some of the safety-scanning
approaches that have been taken.  Even if you don't have a cap-secure
language to begin with, it is certainly worth studying how E
accomplishes what it does without a scanner necessary; quite likely,
your scanner will want to reduce the language to something E-like.

To give a taste of why E does not need a separate scanner, consider the
following example (please forgive my pseudo-E):

	def string = read_from_some_file();
	def _ = eval([], string);
	
This eval() function (not the exact one that E has, I'm sure) has two
arguments: the code to run, and a list of bindings to use for any
undeclared variables that occer in the string.  This list of bindings
can be used to hook up things like stdout.

NO HARM CAN COME from this call to eval.  There are no dangerous ambiant
authorities in a cap-secure language, and thus the only handholds the
evaluated code has are ones supplied in the initial call to eval().  In
this case, an empty list is supplied, so the program can't do anything. 
If you can forgive me for a few silly metaphors, it is like...

	- ...running a .o file in an OS's protected memory space, but providing
it with no system calls.
	
	- ...putting up a Wheel-of-Time magic shield, which is not strong, but
instead is so smooth that you can't get a hand-hold on them to tear them
open.
	
	- ...trying to lift the earth and verify Archimedes' claim....  while
standing on the earth and htus having no leverage.


And a semanticist would likely say that the eval() function, when given
an empty list to start with, preserves the invariant that there are no
references between the objects created during the eval-uation, and those
created elsewhere.


This example aside, of course a useful runtime will supply a non-empty
list.  For example:

	def string = read_from_some_file();
	def _ = eval([stdin->sometty,  stdout->sometty],  string);

In this case, now the eval-ed program can access "sometty".  But even
here, *all* the eval-ed program can access is sometty (or anything
sometty indirectly provides access to).  Thus, if you want to analyze
what effects this evaluation may have, you start at the list of things
in the first argument--essentially, the list of system calls the program
gets to use--and you go from there.


Lex