The “Take-Grant” Model

Some take this paper to define the “Take-Grant” model. On page 1 they describe a take operation as an event much like a computer load from memory operation wherein x has a reference to y, and y has a reference to z. The call operation described on page 2 seems to require a primitive stack. Keykos has none. Keykos provides space and time accountability.

I think that any deployed system includes security relevant user mode code. This is code that protects not because it is unable to do the wrong thing, but because it is programmed to do only the right thing.

I think that “take-grant” presumes a stack and that seL4 does not—grain of salt here. What is an ‘untyped capability’? Does every capability have such a method?

I presume that a Frame object is like a Keykos page, except perhaps optionally a some larger power of 2 in size.

How Keykos Differs

This is a matter of description style. Keykos capabilities are stored in nodes. When a domain ‘loads a cap from a node’ we say that the domain sends a message to the node with a binary number that the node decodes as an order to ‘return a cap’ and another number which says from which slot of the node. The node sends a message back to the domain with the cap from the node. ‘Storing into a node’ is similar. There is thus in Keykos nothing much like the Take primitive. This is fairly literal and we get more literal yet to ferret out any problems. The domain code to do this operation is exactly the same bits as if it were asking another user mode program in another domain for something. The domain receives the response exactly as if the reply had been from another domain. The primitive node appears almost exactly to the domain as if it were another domain. Almost; there is a gimmick to be exposed here. Keykos has another fundamental requirement: All state between atomic operations is in pages and nodes. The sending of the message to the node and reply from the node is one atomic operation. Sometimes the reply is deferred as when the node is on the disk, and then the sender of the original message is left in a state of not having sent the message. This is sensible to the holder of the node key only to the extent that he never discovers his sending domain in the waiting state. But with some probability the same might happen even if the node capability had been a start key to another domain. The important thing is that the caller need not know whether what he is calling is in the kernel. Likewise there is no grant primitive in Keykos.

There are no methods in Keykos semantics. Particular objects each have their own protocol and an informal but universal(?) convention for a register value which becomes part of the data of the message, provides an ‘order’ which is in no way different from other data bits conveyed in the message. The recipient is free to do with these bits as he sees fit; the kernel does not look at them. Conventionally they indicate what in other formalities would be called a method code. Sometimes they convey more such as the slot number as in the case above. There is thus no logic concerning methods except in code that responds for some type of object, to invocations. This is possible in part by the above elimination of take and grant which required discriminating between methods. This brings to our next simplicity.

No permission bits in a cap; but a badge (álà seL4) or data byte (álà Keykos) which is one byte of data within a capability. When a message is delivered via a capability X the badge within X, as binary data, is delivered to the recipient along with the message. The information that the permission bits of the capability in the take-grant model, is carried in the badge in seL4 and data-byte in Keykos. It is not the kernel but the message recipient that interprets the badge bits. If the recipient is code in the kernel, such as the node case, then that interpretation code is in the kernel.

seL4; Older note; “take grant” in Markm’s Thesis
A discontinuity here.

I woke this morning at 04:30 this morning and realized that there is something wrong with the take-grant idea. I may be wrong but here goes:

I am trying to understand seL4 which claims to follow the take-grant model. I think that when you want to attenuate an authority, in the form of a capability, the idea of take-grant is for the kernel (cap-master) to turn off some bit as it derives a new lesser capability to the same object. I think the take-grant model imagines a central authority that understands that bit number 9 in each cap can be turned off to prevent some class of information flow. I am speaking very roughly here, of course.

The contrasting model, which I will call the “facet model” here decentralizes the coded meanings of the badge and leaves those meanings to the individual code that defines the behavior of those objects, whether or not that code is in the kernel. The cap-master does not know about badge meanings. (“Badge” is the seL4 term for the Keykos databyte. I like their term.)

I can recall worrying when we decided that you can call a page key in Keykos. We never came to regret it. In Keykos you call a page key to get a RO key to that page. Here are the several useful methods or ‘orders’ on a page key. All kernel objects reply at least to the ‘alleged key type’ order. Of course the rogue may lie about its type.

Section 4.2.2 of the manual says:

Keykos considered a weakened start key but could find no scenario where is solved a problem. The ultimate goal is to block information flow. A miscreant blocked with a endpoint capability without ‘Grant rights’ merely copies the data instead. If you have a call capability X and want another, capabilities to which cannot be passed, you install X in a new object programmed to pass messages on to X without their caps. Perhaps take-grant aspires to some sort of confinement. I have not seen any such claim. Some would argue that Keykos strays from simplicity with is primitive sensory stuff. Sensory logic makes some factory patterns efficient and factories do achieve confinement. Sensory kernel knowledge (centralized cap-master stuff) needs to be explained or explained away.