I wrote:
> I'd prefer a security model based on revokable capabilities,
> enforced via proof-carrying code.

This should read:
> I'd prefer a security model based on explicitly granted capabilities,
> enforced via proof-carrying code.

Anyway, here's how this can work.

Let's suppose that usability testing reveals that there are certain kinds of privilege grants that users can easily understand -- eg, something like "The program can only read and write files in the c:\\apps\\foobar directory", or "The program can only open network sockets to the foobar.com domain", and so on. When a user installs a program they check off which privileges they want to give it and then somehow the system makes sure that the program can't use resources it's not privileged to.

So the way we can do this, is to turn each privilege into an object: eg, to open a file the program must call a method on an object that the runtime hands it. You can do a formal verification that the capability object does what it says -- the object code would come with a proof, generated by the compiler, that the loader would check. Then a type- and memory-safety proof for the program code (again, verified with a safety proof emitted as part of the compilation process) would ensure that it couldn't access any ungranted resources.

This is a much better model than unverified assemblies, because it lets you extend the set of grantable capabilities without having to add any untrusted code to the system. The only code you have to trust is the proof verifier, which is small. Even the compiler doesn't have to be trusted, because if it emits buggy or false proofs the verifier will fail to accept the object code. Even better, you get the full performance of compiled machine code, with no need for a sandbox, since the proof is checked at load time, not runtime.

Here's a general overview:

[link|http://www-106.ibm.com/developerworks/library/untrusted-code/|[link|http://www-106.ibm.com/developerworks/library/untrusted-code/|http://www-106.ibm....rusted-code/]]

And some links to research projects:

[link|http://www.cs.berkeley.edu/~necula/pcc.html|[link|http://www.cs.berkeley.edu/~necula/pcc.html|http://www.cs.berke...ula/pcc.html]]
[link|http://www-2.cs.cmu.edu/~fox/pcc.html|[link|http://www-2.cs.cmu.edu/~fox/pcc.html|http://www-2.cs.cmu.edu/~fox/pcc.html]]
[link|http://www.cs.princeton.edu/sip/projects/pcc/|[link|http://www.cs.princeton.edu/sip/projects/pcc/|http://www.cs.princ...rojects/pcc/]]