
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