Clarification on "valid capabilities"

[jasonyu1996]

Chapter 2 mentions:

   If the tag is set, the capability is valid and can be dereferenced (contingent on checks such as permissions or bounds).

and

(see The address Section 2.2.6.3).
 and bounds must be representable in valid capabilities i.e. when the tag is set

So one would expect "valid capabilities = capabilities with tag set"

But in 2.2.6

A capability is malformed if its encoding does not describe a valid capability because its bounds cannot
be correctly decoded.

which suggests that a capability can be invalid because its bounds cannot be decoded, even if the tag is set.

The consequence is one doesn't know if this in 2.2.1 applies to tagged capabilities with non-decodable bounds:

All capabilities derived from invalid capabilities are
themselves invalid i.e. their tags are 0

[arichardson]

The "tag set, but bounds malformed" case should only be possible due to an error in the memory subsystem/bit flips, maybe we should more explicitly call out that these will not exist in a well-defined execution?

[jasonyu1996]

The "tag set, but bounds malformed" case should only be possible due to an error in the memory subsystem/bit flips, maybe we should more explicitly call out that these will not exist in a well-defined execution?

I think the culprit is "A capability is malformed if its encoding does not describe a valid capability because its bounds cannot be correctly decoded" in 2.2.6. The reader would expect that sentence to be a definition of "malformed capabilities", which should be something like "A capability is malformed when its bounds cannot be correctly decoded." Whether it is a valid capability is irrelevant here. Also, it's not "because its bounds cannot be correctly decoded" that a malformed capability "does not describe a valid capability". In my understanding, a malformed capability cannot be valid (i.e., tagged) only because well-formedness is always enforced, rather than by definition.

[tariqkurd-repo]

In my understanding, a malformed capability cannot be valid (i.e., tagged) only because well-formedness is always enforced, rather than by definition.

Not quite, and this is something we've been working on very recently.
If a corrupted (tagged and malformed capability) is read by the memory system it will be propagated through stores, and register moves without modification.
Any instruction which needs to decode the bounds will take action, e.g. setting the result to 0 for GCBASE.

We didn't want to clean up bad caps as LC/SC/CMV should just propagate what's there to avoid complicating the micro-architecture.

[jasonyu1996]

In my understanding, a malformed capability cannot be valid (i.e., tagged) only because well-formedness is always enforced, rather than by definition.

Not quite, and this is something we've been working on very recently. If a corrupted (tagged and malformed capability) is read by the memory system it will be propagated through stores, and register moves without modification. Any instruction which needs to decode the bounds will take action, e.g. setting the result to 0 for GCBASE.

We didn't want to clean up bad caps as LC/SC/CMV should just propagate what's there to avoid complicating the micro-architecture.

But the only source of malformed but tagged capabilities is errors in the memory subsystem or hardware bugs? The ISA level makes sure that tagged capabilities that can ever be created/derived are all well-formed right?

[arichardson]

I believe this is now fixed - please reopen it if not.