[cap-talk] Security by safe language processing

[David-Sarah Hopwood]

Jed Donnelley wrote:
> At 05:43 PM 9/3/2009, Bill Frantz wrote:
>> The idea of depending on the compiler or byte code verifier in a "language
>> based system" (LBS) is quite attractive since it might result in a higher
>> performance system.
> 
> Higher performance in that it can avoid hardware context switches that
> are typically rather expensive?  I'm sure we all know of many ways that this
> issue has been addressed (with whatever success or not).

Despite such attempts, there is still a very significant gap between the
performance of IPC involving context switches, and the performance of an
method call between objects. This makes it possible in a language-based
system to consider designs involving security boundaries between extremely
fine-grained objects, that would be totally impractical in a system based
on hardware memory protection.

>> The only compiler that needs
>> verification is the one used to compile the system, and it only needs to be
>> verified for the features used by the source code of the system. Since only
>> a limited amount of programming needs to be verified, auditing the output
>> of the compiler is a feasible, if tedious, possibility.
>>
>> In contrast, LBS system compilers and/or byte code verifiers must be
>> verified against all possible inputs, which seems to me to be a harder
>> problem.
> 
> Not only that, but the LBS system compilers and/or byte code verifiers
> must be valid against all possible inputs over a long range of time -
> perhaps all time.

That is not necessarily the case. A system could be designed so that the
input to any code generation step is always kept, and the output is only
treated as a cache. Then, whenever the code generator is upgraded, the
cached output is invalidated and will be automatically regenerated as
needed. There have been language-based systems (for example Self) that
were able to do dependency checking and automatic recompilation at least
as complicated as this, although with different motivations.

> I know of very few systems that depend on language processing for
> security.  One example that I'm aware of was the Burrough B* systems
> (B5500, B5700, B6500, B6700).  These systems depended on their
> compliers for security.

Note that those were high-level language compilers. Relying on such
compilers is not the approach that I or most advocates of language-
based security would suggest; we would argue for having only a trusted
compiler for some much simpler kernel language, and then to use
"untrusted" compilers for several higher-level languages to the kernel
language. (These are still relied on, but only for correctness of the
programs they compile, not for system security.)

> One problem with this approach is that if
> there is a bug in a complier that generates unsafe code at any
> time and one can save that code, then it is unsafe for as long as
> it can be saved.

Yes; the design I outlined above solves this problem because the saved
code would be invalidated when the compiler changed. Since you say
that the compiler was only "briefly" bad, the window of vulnerability
would also have been brief. It would actually be quite easy to implement
this in a capability system -- the output of the code generator would be
an object that refuses to run until it has checked that the compiler that
produced it has not recently changed. (For persistent systems that use
an event-loop model, each vat can be stopped, recompiled, and restarted
at a turn boundary.)

Note that in current operating systems, essentially the same kind of
vulnerability can occur with compiler-induced bugs in user-mode
applications and libraries, even though it does not *directly* allow
attacking the kernel. To fix all of the potential security vulnerabilities
due to a compiler bug, after the compiler itself has been fixed, it is
in principle necessary to recompile almost everything on the system.
This is rarely done in practice. The above design solves the problem
at this level as well.

-- 
David-Sarah Hopwood  ⚥  http://davidsarah.livejournal.com