Thoughts on rights bits in caps, badges or databytes

seL4 seems to have both rights bits in caps and badges. That seems like overkill to me. Each cap has 3 rights bits, Read, Write & Grant. I don’t know whether lack of the Grant bit on cap X keeps you from sending X, or from sending caps via X. I think neither is necessary. It might possibly be an efficiency thing. We found no benefit in having a kernel function that copied and degraded keys. In each case it sufficed to call the designated object and ask for a weaker key. The object could always choose badge values to accomplish these distinctions.

The kernel, being responsible for the semantics of page keys and segmode keys, chose to use one fixed bit in the badge to indicate RO. I never examined the code to see if this made the kernel code any shorter. It made the manual slightly shorter,