[cap-talk] Capabilities and Freedom vs. Safety

[David Chizmadia (JHU)]

Jonathan S. Shapiro wrote:
> On Wed, 2007-07-25 at 08:46 -0400, David Chizmadia (JHU) wrote:
> 
>> In a pragmatic sense, your situation is akin to the case of an
>> evangelical Christian minister discussing how to live life as a
>> member of the faithful with a group of Muslim imams. There is
>> occasional agreement on extremely minor details, but fundamental
>> assumptions (doctrine) about the faith being lived are too disjoint
>> for sustainable communication to occur...
> 
> Hmm. Much as I enjoy the analogy, it is not correct.
> 
> The problem between the Imam and the Priest is that they are proceeding
> from incompatible ground axioms.

    Exactly! Based on reading through the distributed system design
posted by JAD and his posts since then (especially the ones this
morning), I've concluded that we are, in fact proceeding from
different and intrinsically incompatible axioms.

> The access control community is often lazy about math, but when pushed
> to the wall we actually *do* agree about the ground axioms.

    Based on the next para, I think you backed up further than I
did. Continuing the analogy, the "doctrines" correspond to the core
axioms in each access models that establish the objects to which ACI
is attached (I believe the formal analysis term for these axioms is
invariants, but I may be wrong) and the specifications of how access
decisions are made based on available ACI.

    Using this mental model, I would claim that if the AA and OCap
models (irrespective of whether each is consistent and complete) are
not diametrically opposed in a formal modeling sense, they are
sufficiently far apart to seem that way to the casual observer.

> Further, we
> agree about the proper mechanisms for analysis (that is: formal logic
> and formal algebras). The various designs that we construct can be
> formally expressed and subjected to verification proofs, and many
> sub-communities have done so. The differences between the
> sub-communities lies in the fact that of all the various verification
> proofs that have been offered, only the ones from the RBAC communities
> and the capability communities have (a) had a useful outcome, and (b)
> survived rigorous examination.
> 
> As you point out:
> 
>> So far, the analysis has supported the part of the hypothesis that
>> OCaps are not subject to most of the AA design flaws.
> 
> The difference between the RBAC community and the capability community
> is that the RBAC approach is exceptionally hard to maintain and
> document. Consider the continuing maintenance pains of SELinux as an
> example.
> 
> The difference between James and the community is that James doesn't
> understand the math. He therefore tries to reason about this stuff
> informally. Then he gets upset when people who *do* understand the math
> tell him that he has it wrong.

-DMC