Clarify interaction of levels with sealed capabilities

[arichardson]

Sealed capabilities should only have their CL changed, but not the EL permission.

See also CHERIoT-Platform/cheriot-sail#14

[LawrenceEsswood]

I agree with the CheriOT decisions here and that only level is outside of sealing, this LGTM.

[nwf]

It's worth noting that we're not completely happy with the CHERIoT solution, since it means that it's possible to strip GL(obal) off a sealed sentry and so deprive the unsealed form, and all its progeny, of GL.

In practice, this isn't a huge problem for us, because we

1. Don't have that many architecturally sealed forms
2. generally don't derive long-lived capabilities to sub-objects from data-typed sealed caps, and
3. are quite restrictive in the kinds of executable-typed sealed caps we pass around:
   • intra-compartment return sentries
   • library function entry points (forward sentries)
   • forward and reverse sentries for the switcher

Flipping bits on intra-compartment anything is just going to hurt yourself. Libraries are much like your own code, and jumping in with a non-GL sentry is just going to mean anything derived from its PCC is also non-GL, but the library is unlikely to store those beyond the stack anyway (of course, the caller might, but again: don't hurt yourself). The switcher does not derive sub-objects from PCC.

But, even though it seems to work out OK for us, it's still not ideal, but we have yet to come up with a better solution. It might be a problem for different compartmentalization models that try to use sentries more directly.

[tariqkurd-repo]

The table is very hard to read formatted like that, I've made a local modification so it looks like this:

so now I can start to unpick the differences. For example:

EL=0 CL=1 Tag=1 Sealed=Yes -> reduce CL, EL unchanged (was unmodified)
EL=0 CL=1 Tag=1 Sealed=No -> EL=0, CL unchanged (was unmodified)

but also the table isn't fully specified, for example

EL=0 CL=0 Tag=0 Sealed=X -> what happens here? It should be unmodified.

How about this instead - it's much easier to read - is it correct?

@jamie-melling
@tomaird

Modifying a sealed capability also breaks this text:

Sealed capabilities (CT ≠ 0 ) cannot be dereferenced to access memory and are immutable such that modifying any of its fields clears the tag of the output capability

[davidchisnall]

It's worth noting that we're not completely happy with the CHERIoT solution, since it means that it's possible to strip GL(obal) off a sealed sentry and so deprive the unsealed form, and all its progeny, of GL.

I think we are happy with that behaviour (we use sealing for software-defined capabilities and it is useful to be able to provide a no-capture guarantee to delegated capabilities. Software that needs to capture can explicitly check for G and error, or can embed a G capability to the object inside the outer sealed object). The thing that we're not happy about (and have an issue to track) is that we can strip G by round tripping through memory but we can't do it via candperm. We aim to fix that before 1.0.

[tariqkurd-repo]

I added the note about CL changing evenon a sealed cap