Entry Cap is a subset of AccountCall Cap?

[Latrasis]

One of the main features we want to keep as strongly as possible is that all capabilities are "seperate" to each other. Such that having a Write Cap will not allow a procedure to do anything a Log Cap does and vice versa.

This orthogonality has exceptions in the case of:

• ProcedureCall Cap, which allows a procedure to potentially dispatch capabilities of other procedures.
• AccountCall Cap, which allows a procedure to potentially dispatch capabilities of the entry procedure in the case of re-entrancy.
• Entry Cap, which allows a procedure to assign a different procedure as an entry procedure and thus expose that procedure's capabilities for dispatch to the outside world.

By themselves they don't worry me too much, however I am worried what happens if you combine them. With the AccountCall Cap and the Entry Cap, a procedure could potentially assign any procedure as the entry procedure, then in the same execution do a re-entrancy call
to access the new entry procedure's capabilities.

It seems to me that with the introduction of the concept of an Entry Procedure itself requires additional semantics to describe the relationship it has between the ProcedureCall and AccountCall Capabilities. To a certain extent it looks like the EntryCap is a subset of both of these Capabilities, but the exact reasoning isn't very clear. Which means the definition of the "Entry Capability" isn't very fleshed out in terms of it's effects on the system.

My question is, is there a more clear way we could describe the relationship between these three capabilities? And if so, what are the invariants that describe this "seperation"?

[17451k]

To a certain extent it looks like the EntryCap is a subset of both of these Capabilities, but the exact reasoning isn't very clear.

To me it looks more like any ProcedureCall Cap is a subset of combination of Entry + AccountCall capabilities, since with this combination any procedure call can be performed.

AccountCall Cap, which allows a procedure to potentially dispatch capabilities of the entry procedure in the case of re-entrancy.

This can be described in a similar way as follows: any AccountCall Cap is a subset of the ProcedureCall Cap to call the entry procedure.

But it is not clear to us whether these exceptions (including combinations of them) should be explicitly formalised in the specification, or whether they should be mitigated in some way by changing the specification?

My question is, is there a more clear way we could describe the relationship between these three capabilities? And if so, what are the invariants that describe this "separation"?

Today we had a serious internal discussion about the possibility of describing the separation concept. For now it seems that it is possible, but the exact form is quite difficult to formulate. And it will certainly require a complete formal specification, which we do not have yet.

[JakeOShannessy]

They way I see it, the Entry capability is the risky "master" key that underpins all of these issues. Account Call and Procedure Call are quite straightforward in what they can and can't do. The only risk seems to be that someone might not fully appreciate the power of the Entry capability.

It's the Entry capability that allows you to take control of the system. The other capabilities don't interact with it in a special way, they are just the normal tools you would use once you have taken control of a system (if you were malicious or otherwise).