[Haskell-cafe] OS design & FP aesthetics

[Jaap Weel]

> > Normally I've seen capabilities used so that you can't access
> > anything you can't name.  Can you elaborate a little?
>
> He's saying that the language itself prevents programs from writing
> outside their address spaces

Yep. Capabilities are usually not actually unforgeable, they are just
picked from a largish key space. You can guess at them if you want to
bother. Somewhere in the Exokernel papers, there is some discussion of
this, and reference to the fact that a 64 bit capability is at least
as secure as an 8 byte UNIX password, which I suppose is a fair
assessment of the situation. 

With language based security, you can have unforgeable capabilities,
though. An example of a system based on that idea, although expressed
in different words, is

http://mumble.net/~jar/pubs/secureos/secureos.html

An alternative approach to unforgeable capabilities is to build them
into the hardware using a tagged architecture. There is a paper by Tom
Knight (mastermind of the original Lisp Machine) and Jeremy Brown
that is relevant here, although it actually deals with the somewhat
different problem of data dissemination control (think DRM but more
for military applications and suchlike):

http://www.ai.mit.edu/projects/aries/Documents/Memos/ARIES-15.pdf

Note that earlier tagged architectures, including the Knight Machine
and the K-machine, used tags mostly to speed up Lisp and not to
enforce any sort of type discipline.

> Which is a nice theory, but is dependent on the runtime not being
> buggy (I think some problems have been demonstrated with large
> arrays in GHC...).

There are three ways to deal with this. The first is the
aforementioned tagged architecture in hardware. The second is running
everything within a virtual machine that has a tagged architecture. In
both of these cases, there would be a trusted security kernel, but
you could make it pretty damn small. Unfortunately hardware is
expensive and virtual machines are slow (although people keep claiming
that they're getting better, and FPGAs are getting faster and cheaper
all the time).

The third way is to have a compiler that compiles Haskell, or any
other typesafe language, into a typed assembly language with a
sufficiently expressive type system. You can then feed TAL-annotated
binaries to the (trusted) loader. This way, you can also support
multiple programming languages while still maintaining language based
security and a small trusted security kernel, viz. the TAL type
checker.

  /jaap