On Sat, Jul 5, 2014 at 12:13 AM, Jonathan S. Shapiro <[email protected]> wrote: > On Fri, Jul 4, 2014 at 8:52 PM, Matt Oliveri <[email protected]> wrote: >> Now that I'm using your definition of "permission", I can't even tell >> what we were arguing about here.
To be sure we haven't miscommunicated, I only meant to take back what I said about "primitive permissions", which now seems nonsensical. I still think you're thinking about Java casts the wrong way, and that they aren't security-related operations, and that in itself, this is not a design flaw. > A word though about "primitive" operations. Any operation implemented by a > program is necessarily constructed from the primitive operations of the > runtime. One of the design axioms in KeyKOS, EROS, and Coyotos is that there > is only one "rights amplifying" operation (the identifyEntry operation[s]), > and we're damned queasy about that one. It actually turns out that you could > do that operation without rights amplification, but you'd need to maintain a > pretty monstrous capability set to do that. You might want to take a look at the trick to do checked downcasts in OCaml. It might be similar. http://caml.inria.fr/pub/docs/manual-ocaml-4.00/manual005.html#toc29 Search for "idiom". > The reason we feel so strongly about this: > > If the primitive operations do not provide any means for rights > amplification, then it follows that there is no way for a program to somehow > escape or exceed the authority bounds presented by it's capability [set]... > > But conversely, if the primitive operations do offer some means of rights > amplification, you're screwed from the get-go. I'm not convinced. Rights amplification is not as bad as undeniable authority as far as I can see. It makes figuring out authority harder, but it's still very systematic, and the answer isn't necessarily bad news. In logic, theories can often be specified by a finite set of axioms, but the full theory is all theorems entailed by the rules of deduction starting from those axioms. I'm going to try an analogy. The rules of deduction are like the rules about how capabilities can be obtained. The initial capabilities are the axioms. The authority is the full theory: the closure under deduction, starting from the axioms. In general, unioning some axiom sets, then closing to get the theory, is not the same as closing each axiom set, then taking the union of the theories. The former is a superset, and it's often a strict superset. This is essentially rights amplification. Combinations of axioms do more than just get you independent sets of conclusions to combine. So in logic, no one asks about the conclusions you can draw from an axiom. You only talk about the conclusions you can draw from a set of axioms. That is, you ask about the theory for a set of axioms. So in capability systems with rights amplification, it seems you should ask about the authority of a set of capabilities. The idea being that determining authority isn't reducible to determining the authority of the individual capabilities (or any strict subsets of the full set) in isolation. What's wrong with thinking about authority this way? > So following this philosophy of minimizing rights amplification, I would > argue the things I have been arguing over the past day or two: that downcast > and interface fetch should not be operations that are inherently permitted > by the primitives of the language. At the very least, there should be a > mechanism by which the programmer says "yes or no" to these operations, and > also "under what conditions". It sounds like you're still thinking of downcast as rights amplification. That's pretty frustrating. Has nothing changed, other than me learning the proper definition of "permission" and you learning that Java object casts don't affect object id? > I think we've talked this through at this point. Are you saying you don't want to discuss it anymore? I don't think we've settled much of anything. > The only reason I'm sending > this is to try to give some sense of the relationship between the capability > ideas in Coyotos and the guarded interface ideas that we have been talking > about here. There's clearly some commonality. If I understood Coyotos better, I might recognize even more commonality. Your notion of interface does seem to have a clear family resemblance to Coyotos capabilities, being distinct runtime entities from the object itself. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
