I’ve been thinking.
Let me preface this by suggesting: if there were a globally trusted capability-secure computing fabric, we would have no need of (some kinds of) crypto.
Why? What do we do with crypto? We sign things, and we encrypt things. How do we do this with our GTCSCF? Easy. To sign something, I hand that something to the relying party. He then exercises his capability to me that checks authenticity of somethings, and I respond that it is authentic.
Encryption is even easier – I just send the something down a capability leading to the intended recipient.
So, I claim, there is effectively a mapping between crypto (at least for signing and encrypting) and a great capability machine in the sky (i.e. the GTCSCF).
Considering this idea further, it seems to me that this is essentially the core idea behind Universal Composability. If I can show that my crypto system does indeed map to a GTCSCF, then I have a crypto system that can clearly be composed with other crypto systems, and only have the consequences we would expect from a capability-secure system that implemented the same functionality.
What would it mean to make such a proof? My, perhaps amateur, understanding is that you would have to show that the corresponding capabilities have the properties we expect of them: that they are opaque, unforgeable, and only obtainable by being handed them in some way.
This sounds doable to me, modulo assumptions about the hardness of the discrete log problem, and the like.