[cap-talk] A question on capabilities - charts review + comments

[David Wagner]

Thanks for all the advice and feedback on my talk, Jed.  I'll keep
this around for the next time I give this kind of presentation.  I
should also say that I didn't have time to get into everything in the
slides; what I wrote in the slides is what I hoped to be able to talk
about, but what I had time for was a subset of that.

A few small comments.

You write:
>You do get to this capability value when you reach your chart,
>"Object capabilities enable local reasoning", at least I think that's
>what you're getting at.  I admit that the logger example on that
>chart doesn't convey the value to me.  When you say, "Notice
>how easy that was?" and contrast it with a monolithic C or C++
>application where you argue you would be forced to "tediously
>inspect every line of course code in the entire application", isn't
>that essentially what you're doing with the "capability" reasoning
>about the logger - namely searching the entire source  to see what
>it does to the log file.  Perhaps I'm missing the fundamental point
>here?  I don't see how it points out the value of capabilities to
>enable local reasoning - though I do believe they do.

Nope, that's not what I was proposing for capability reasoning.
Suppose the Logger creates the log data structure itself: e.g.,
    class Logger {
        private LogEntry log[];
        Logger()  {
            log = new LogEntry[...];
        }
        ...
    }
    class LogEntry { ... }
Now it is easy to do capability reasoning -- i.e., reachability
analysis -- to identify the set of all code that might be able to
get a capability to the log entries.  If Logger ensures that "log[]"
(and all of the LogEntry references stored there) is closely held
and cannot escape, then we know that no one else will get a capability
to the log entries.  That kind of reasoning lets us convince ourself
of the correctness of the logger without looking at the entire source
of the application.  If Logger and LogEntry are implemented correctly,
we can convince ourselves that the log will be append-only just by
looking at the source of Logger and LogEntry.  That's the kind of thing
that's just not possible in a language like C or C++.

>I think I've used that term "capability discipline" in another way.
>Perhaps we can get a reading from the list members on how that
>term should be used.

I'm interested to hear how others use the term.  If I've misunderstood
the intention of others here, that would be a good thing to know.

>Regarding your chart, "Immutable objects simplify reasoning"
>and the statement that "immutable objects convey no authority."
>Perhaps I'm misunderstanding something here.  What about
>a capability to a read-only file?  I believe that's immutable but
>also conveys an authority.  Am I reading this wrong?

I suspect it all depends about what degree of approximation you are
working at.  In my experience, it is typical that the abstraction of
authority that we reason about is that we reason about ability to cause
side effects upon the outside world (through overt channels).  We usually
do not attempt to reason about knowledge of secrets.  For instance, we
usually conservatively assume that the number "3" (and all other such
integer values) are known to everyone.  That's a conservative approximation
of authority.  It in some cases may too conservative -- for instance, it
is too coarse to reason about cryptography (because it assumes all
secrets are known to everyone), and it is too coarse to reason about
covert channels (because it only reasons about overt influence over the
outside world, not covert influence).  In essence, it amounts to making
the conservative assumption that the adversary is a perfect guesser --
anything the adversary could do if it could correctly guess the content
of some secrets, we will conservatively assume that the adversary can do.
The reason for making this kind of conservative approximation, where we
only reason about ability to cause side effects but not about knowledge,
is that it is an approximation that is both feasible to reason about while
at the same time being useful.  (For instance, while it might be useful if
we could reason about secrecy, it is often not feasible to reason about
secrecy or about covert channels.)

And once you work at the level of abstraction where you are only concerned
with ability to cause side effects and not about knowledge of secrets,
then an immutable reference to the integer 42 does not convey authority.
(It would probably be a little more precise to say that, if you're
starting from the assumption that everyone knows all secrets, then
passing an immutable reference to the integer 42 to Bob doesn't give Bob
any authority he didn't already have: at worst it only conveys knowledge
of a secret, but we were assuming Bob already knew all secrets anyway.)
Similarly, a read-only reference to an immutable file does not convey
authority, either.  However, if you're talking about a read-only reference
to a mutable file, I need to think about that one a little more.  I suspect
the answer is that if the file can only contain bits (but not capability),
then even a read-only reference to a mutable file doesn't convey authority
(although it is a pretty dangerous animal from a TOCTTOU and thread-safety
point of view).  However, if a file can contain capabilities, then a
read-only reference to a mutable file does convey authority.

I learned this point of view (recognizing that when we are reasoning
about authority, we are reasoning with conservative approximations of
authority) from Mark Miller.  I hope I haven't done the idea too much
injustice.