I've been lurking for this whole discussion, and would like to thank all the participants for some interesting reading.
One question I would like to ask is about the motivation for this so called "endogenous" verification, in EROS and others, and potentially future-hurd. I understand this to mean that its possible within the system to calculate (using a transitive completion of the capability relation) that something cannot reach a particular other capability. This involves categorising the capabilities into "secure" and "insecure" ones in some way, and only following the "insecure" ones. You might gather from my quotes above that I'm sceptical about this classification, and whether it brings any benefits. So my question is: how much is this used in EROS etc, how useful is it, and how reliable - does it actually prove what it purports to, or are there problems with the classification? We might think of it as akin to so called "introspection" that is possible in the run-time systems of certain languages (java), and used to support dynamic loading and configuration of system components. -- [EMAIL PROTECTED] _______________________________________________ L4-hurd mailing list [email protected] http://lists.gnu.org/mailman/listinfo/l4-hurd
