authority question

[Jonathan Aldrich]

I have a question for this group (and perhaps especially Mark Miller, whose thesis and other work is closely related).  We are trying to define authority formally in a paper we're writing (I'm cc'ing my coauthors).  Our starting point comes from Mark's thesis, where he says "Authority is the ability to cause effects."  We are formalizing this quite directly as our language includes an effect system that overapproximates what actions of interest a function can perform.  We have found an interesting corner case that I wanted to ask the group for your opinion on.

Imagine you have an object constructed by the following pseudocode expression:

let o = new object {

    def invoke(callback) {

        callback(file)

    }

}

In the pseudocode above, "file" is a resource in the file system; I am assuming that reading or writing to that file is an effect we are interested in.  Now the question: does the object o above have authority to the file?

On the one hand, you might say the answer is "no" because the object o does not  (and cannot, given the way it is written) ever directly read or write from the file.  Reading and writing might happen, but if it does it would be a result of what the callback does, not the object o.

But our current thought is that the answer should be "yes" because if an appropriate callback is passed in, object o can cause a read or write to happen on the file based on that callback.  In fact, the callback may in fact only have access to that file because o passed it to the callback.  So it seems most appropriate to conclude that o has authority to the file, and o delegates that authority to the callback when invoke() is called.

An interesting twist is that because we have a static effect checking system, we can actually verify that the callback passed in does not have a file read or write effect on the file when it is invoked.  Does this change the conclusion above?  I would argue not--because one of the things the callback can do is store the file for use later.  If this happens, then once again the logical conclusion is that o had the authority to read and write the file, it delegated this authority to the callback, and the callback further passed on the authority to some third party which at some later point actually has a read/write effect on the file.

What do you think?  Does the above analysis make sense to you?

Thanks,

Jonathan

[Raoul Duke]

i know it was only pseudocode, but where did "file" even come from? 

as a joe programmer on the street i expect the root of all this to be the type on "callback" in terms of where the authority lies to operate on "file" - then "invoke" must say what kinds of callbacks are allowed, it must specify the signature of allowed callbacks. 

[Jonathan Aldrich]

Thanks for your question!

On Wed, Jun 23, 2021 at 12:31 PM Raoul Duke <rao...@gmail.com> wrote:

i know it was only pseudocode, but where did "file" even come from? 

Good question--I am assuming that a capability to the file is given to the object when it is created.  In a language with constructors, it would be passed to the constructor.  The question I am considering is whether the object has authority to the file after construction.

 

as a joe programmer on the street i expect the root of all this to be the type on "callback" in terms of where the authority lies to operate on "file" - then "invoke" must say what kinds of callbacks are allowed, it must specify the signature of allowed callbacks. 

The signature for callback we're assuming is:

callback: File -> {} unit

In other words, callback is a function that accepts a file and returns nothing (type "unit" in type theory--the equivalent of void in C or Java).  The {} express the effect of the function when it is invoked; in this case we're saying it has no effect (that we are tracking).  As I mentioned at the end of my email, this means the callback can't actually do a "file.write()" operation, because that would have an effect.  But the callback *can* pass a capability to the final on to any other object, which means that "file.write()" could be called at some later time.

This means that the type of invoke is something like:

invoke: ( File -> {} unit ) -> {} unit

Best,

Jonathan

 

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAJ7XQb4Yn72w%2B-5f1zZku%3DJXn3vvTxkA2Dhv3HcLwQY7k1Y5bA%40mail.gmail.com.

[Mike Stay]

I would say that it's a wrong question. You can ask what authority an
object reference conveys; the holder of a reference may use that
authority or may not.

> --
> You received this message because you are subscribed to the Google Groups "cap-talk" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANwk4UYOhG1X4PNMt7JOoYZzva1%2BB4c-z90oygWCZY22uX2Lng%40mail.gmail.com.



--
Mike Stay - meta...@gmail.com
http://math.ucr.edu/~mike
https://reperiendi.wordpress.com

[Kevin Reid]

On Wed, Jun 23, 2021 at 8:43 AM Jonathan Aldrich <jonathan...@cs.cmu.edu> wrote:

I have a question for this group (and perhaps especially Mark Miller, whose thesis and other work is closely related).  We are trying to define authority formally in a paper we're writing (I'm cc'ing my coauthors).  Our starting point comes from Mark's thesis, where he says "Authority is the ability to cause effects."  We are formalizing this quite directly as our language includes an effect system that overapproximates what actions of interest a function can perform.  We have found an interesting corner case that I wanted to ask the group for your opinion on.

Imagine you have an object constructed by the following pseudocode expression:

let o = new object {

    def invoke(callback) {

        callback(file)

    }

}

In the pseudocode above, "file" is a resource in the file system; I am assuming that reading or writing to that file is an effect we are interested in.  Now the question: does the object o above have authority to the file?

On the one hand, you might say the answer is "no" because the object o does not  (and cannot, given the way it is written) ever directly read or write from the file.  Reading and writing might happen, but if it does it would be a result of what the callback does, not the object o.

Any useful definition of "authority" should have the transitive property: the fact that "o" is using a supplied arbitrary function rather than making calls itself should not reduce the authority it is understood to have. (If the function is not otherwise restricted; see below.)

 

But our current thought is that the answer should be "yes" because if an appropriate callback is passed in, object o can cause a read or write to happen on the file based on that callback.  In fact, the callback may in fact only have access to that file because o passed it to the callback.  So it seems most appropriate to conclude that o has authority to the file, and o delegates that authority to the callback when invoke() is called.

An interesting twist is that because we have a static effect checking system, we can actually verify that the callback passed in does not have a file read or write effect on the file when it is invoked.  Does this change the conclusion above?  I would argue not--because one of the things the callback can do is store the file for use later.  If this happens, then once again the logical conclusion is that o had the authority to read and write the file, it delegated this authority to the callback, and the callback further passed on the authority to some third party which at some later point actually has a read/write effect on the file.

If “writes to storage that outlasts the function call” is an effect, or (as a more precise analysis) if storage locations are statically tagged with the effects that all of their readers may have, then you can track effects and correctly conclude that the callback with no effects cannot have effects upon "file" and thus does not contribute to "o"'s authority.

(This is a useful property similar to the guarantees you can get via parametric polymorphism as seen in e.g. Haskell, like "I can sort this list of objects and know the sorting algorithm will not invoke them except via the comparison function, because it is generic over the type of objects and has only been given the list and the type-specific comparison function.")

If your system can support either of these analyses, then you can conclude that "o" has no authority to "file" (except whatever is not counted as an effect — such as the ability to prevent it from being garbage collected). If it cannot, then you must conclude that "o" has full authority to "file".

[Jonathan Aldrich]

On Wed, Jun 23, 2021 at 1:59 PM Mike Stay <meta...@gmail.com> wrote:

I would say that it's a wrong question. You can ask what authority an
object reference conveys; the holder of a reference may use that
authority or may not.

Does it help if I rephrase the question as follows: "Does a reference to object o convey the authority to read and write to the file?"

Again, we currently think the answer should be yes, based on the reasoning below.  But we'd like to check our intuition with this group and mkae sure we're on the right track.

Thanks,

Jonathan

 

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAKQgqTa3XH%2BYaWVtoBAgUXHvmKFD%3DuQX-UzPXA3XiVU-2MbErA%40mail.gmail.com.

[Matt Rice]

On Wed, Jun 23, 2021 at 6:03 PM Kevin Reid <kpr...@switchb.org> wrote:

On Wed, Jun 23, 2021 at 8:43 AM Jonathan Aldrich <jonathan...@cs.cmu.edu> wrote:

I have a question for this group (and perhaps especially Mark Miller, whose thesis and other work is closely related).  We are trying to define authority formally in a paper we're writing (I'm cc'ing my coauthors).  Our starting point comes from Mark's thesis, where he says "Authority is the ability to cause effects."  We are formalizing this quite directly as our language includes an effect system that overapproximates what actions of interest a function can perform.  We have found an interesting corner case that I wanted to ask the group for your opinion on.

Imagine you have an object constructed by the following pseudocode expression:

let o = new object {

    def invoke(callback) {

        callback(file)

    }

}

In the pseudocode above, "file" is a resource in the file system; I am assuming that reading or writing to that file is an effect we are interested in.  Now the question: does the object o above have authority to the file?

On the one hand, you might say the answer is "no" because the object o does not  (and cannot, given the way it is written) ever directly read or write from the file.  Reading and writing might happen, but if it does it would be a result of what the callback does, not the object o.

Any useful definition of "authority" should have the transitive property: the fact that "o" is using a supplied arbitrary function rather than making calls itself should not reduce the authority it is understood to have. (If the function is not otherwise restricted; see below.)

 

But our current thought is that the answer should be "yes" because if an appropriate callback is passed in, object o can cause a read or write to happen on the file based on that callback.  In fact, the callback may in fact only have access to that file because o passed it to the callback.  So it seems most appropriate to conclude that o has authority to the file, and o delegates that authority to the callback when invoke() is called.

An interesting twist is that because we have a static effect checking system, we can actually verify that the callback passed in does not have a file read or write effect on the file when it is invoked.  Does this change the conclusion above?  I would argue not--because one of the things the callback can do is store the file for use later.  If this happens, then once again the logical conclusion is that o had the authority to read and write the file, it delegated this authority to the callback, and the callback further passed on the authority to some third party which at some later point actually has a read/write effect on the file.

If “writes to storage that outlasts the function call” is an effect, or (as a more precise analysis) if storage locations are statically tagged with the effects that all of their readers may have, then you can track effects and correctly conclude that the callback with no effects cannot have effects upon "file" and thus does not contribute to "o"'s authority.

Not much to add to Kevin's email, just wanted to point out an example from Koka lang, fib3 uses a stateful algorithm/heap effect, but the effect derived for the functions signature is total,

which exactly coincides with the "writes to storage that does not outlast the function call".

https://koka-lang.github.io/koka/doc/book.html#sec-runst

 

(This is a useful property similar to the guarantees you can get via parametric polymorphism as seen in e.g. Haskell, like "I can sort this list of objects and know the sorting algorithm will not invoke them except via the comparison function, because it is generic over the type of objects and has only been given the list and the type-specific comparison function.")

If your system can support either of these analyses, then you can conclude that "o" has no authority to "file" (except whatever is not counted as an effect — such as the ability to prevent it from being garbage collected). If it cannot, then you must conclude that "o" has full authority to "file".

--

You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANkSj9XbKhx2VCC%2BPz%2B6KKWdJuaMFhWUkyDqVc0BPsHZE-3HdA%40mail.gmail.com.

[Carl Hewitt Twitter: ProfCarlHewitt]

Hopefully, the axioms that define Actors up to a unique isomorphism

enable all possible effects to be inferred including using strings to

pass addresses between machines.

See the following:

• https://papers.ssrn.com/abstract=3418003
• https://papers.ssrn.com/abstract=3459566

Regards,

Carl

https://professorhewitt.blogspot.com/

On Wed, Jun 23, 2021 at 8:43 AM Jonathan Aldrich <jonathan...@cs.cmu.edu> wrote:

--

You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANwk4UYOhG1X4PNMt7JOoYZzva1%2BB4c-z90oygWCZY22uX2Lng%40mail.gmail.com.

[Scott Moore]

Hi Jonathan,

Apologies if you get this response twice... it wasn't clear if my first message went through.

We encountered similar conceptual questions and examples when trying to create a formal model of a capability system for a paper investigating further controls on authority in a capability system a few years ago: http://www.thinkmoore.net/papers/2014-CSF-capability-control.pdf. In that paper, we ended up formalizing a notion of capability system using a syntactic system of ownership annotations that are tracked in the semantics, similar to formalisms of software contracts.

I think in that model we ended up considering an example like yours as not granting o authority of over the capability to the file, but granting authority over the "callback" capability (akin to one of the other responses to your message) which can indirectly influence it, a separate concept we captured in the style of information-flow theory.

Definitely interested to hear further conversation here and happy to dig into more details.

Best,

Scott

[Scott Moore]

Hi Jonathan,

This is an interesting question that came up in paper I worked on with Christos Dimoulas, Aslan Askarov, and Stephen Chong a few years back: http://www.thinkmoore.net/papers/2014-CSF-capability-control.pdf. In it, we attempted to formalize a notion of capability safety using a syntactic system of ownership annotations similar to those used to reason about software contracts. I'd need to think about it more carefully, but I think in our system we would say that the object does not have authority over the file, but does have influence, which is more closely related to information flow properties.

I'd be very interested to hear what others on the list think!

Best,

Scott

[Mike Stay]

On Wed, Jun 23, 2021 at 12:04 PM Jonathan Aldrich
<jonathan...@cs.cmu.edu> wrote:
>
> On Wed, Jun 23, 2021 at 1:59 PM Mike Stay <meta...@gmail.com> wrote:
>>
>> I would say that it's a wrong question. You can ask what authority an
>> object reference conveys; the holder of a reference may use that
>> authority or may not.
>
>
> Does it help if I rephrase the question as follows: "Does a reference to object o convey the authority to read and write to the file?"

Assuming that you could do so given `file` itself, then yes, since
invoke passes `file` to `callback`.

[Carl Hewitt Twitter: ProfCarlHewitt]

The term "influence" is improved terminology :-)

In terms of Actor Theory, an event e1 could have influenced an event e2

if e1 "precedes" e1 in the partial order of events of a computation.

Regards,

Carl

https://professorhewitt.blogspot.com/

PS. There are only a few tickets left for sale at the "Theory and Practice of Actors" at StrangeLoop 2021.

https://thestrangeloop.com/2021/theory-and-practice-of-actors.html

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/ef17ccdb-c8fe-4f21-9cee-024ab14f81a1n%40googlegroups.com.

[Alan Karp]

I understand authority to come from a combination of permission and behavior.  For example, I do not have permission to read the file containing your home page, but your web server does.  When I do a GET on that page, your web server has a behavior that uses its permission to show me the home page.  The result is that I have the authority to read your home page.  

In your example, file represents a permission to read the file.  As I understand it, object o allows the callback to act on the file without further intervention of o.  Hence, I would say that o has permission to read the file and grants that permission to the callback.  In my view, a permission is an authority, just a direct one that isn't mediated by someone else.  In that sense, o has the authority.  If you have a strict definition of authority that requires mediation, then I would say o has permission but not authority.

--------------
Alan Karp

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANwk4UZKygkARQUxvMTOFFC08O_Z9iBqZdU275TJV9FsSAoyiA%40mail.gmail.com.

[Raoul Duke]

er, do we know what "file" really is here? i would not assume from the pseudocode or any prose so far that it confers (only/exactly) read access, one could imagine a case where instead it would be write-only? and there can be different kinds of read access eg metadata stat vs. bytes contents? the original prose left it open to interpretation/ was not sufficiently  nuanced when i read it. i guess if anything it sounded like read+write together. 

[Carl Hewitt Twitter: ProfCarlHewitt]

It seems to me that 'authority' and 'permission' are systematically ambiguous.

We need much more nuanced terminology used in theory of computation defined up to a unique isomorphism.

Otherwise, discussion degenerates into conflicting jargon and dogma.

Regards,

Carl

https://professorhewitt.blogspot.com/

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANpA1Z0pEK6Z34GwbxCpiw4hOUEpX5mpi3cgez8nLYKGN7B68A%40mail.gmail.com.

[Mark S. Miller]

Wow, great thread that I cannot yet spend much time on. But you should be aware of another formalization at

Permission and Authority Revisited: towards a formalization

https://research.google/pubs/pub45570/

with Sophia, James, and Toby, cc'ed

Also, Darya (cc'ed) had a hilarious slide about the dozen or so meanings she found for "permission" vs "authority" in the ocaps literature.

--

  Cheers,
  --MarkM

[Ben Laurie]

On Wed, 23 Jun 2021 at 19:04, Jonathan Aldrich <jonathan...@cs.cmu.edu> wrote:

On Wed, Jun 23, 2021 at 1:59 PM Mike Stay <meta...@gmail.com> wrote:

I would say that it's a wrong question. You can ask what authority an
object reference conveys; the holder of a reference may use that
authority or may not.

Does it help if I rephrase the question as follows: "Does a reference to object o convey the authority to read and write to the file?"

That's not even a question in capability-speak. If you have the thing you can do the thing. That's the definition of a capability.

Again, we currently think the answer should be yes, based on the reasoning below.  But we'd like to check our intuition with this group and mkae sure we're on the right track.

I think your track is weird, at least so far. What capability is "file"? Whatever it can do, "callback" can do. Having "o" is the same as having "file", AFAICS. How could it be otherwise?

 

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANwk4UZKygkARQUxvMTOFFC08O_Z9iBqZdU275TJV9FsSAoyiA%40mail.gmail.com.

[Carl Hewitt Twitter: ProfCarlHewitt]

Thanks for the link!

However, computation is better formalized using events rather states because states have problems with concurrency.

Also, computation should be formalized in a way that is programming language independent.

Regards,

Carl

https://professorhewitt.blogspot.com/

--

You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK5yZYjeXawZJ6soVuv%2BO7yomwbmA2ooDdCokASXGQNNpKPZYw%40mail.gmail.com.

[Mark S. Miller]

On Wed, Jun 23, 2021 at 1:13 PM Carl Hewitt Twitter: ProfCarlHewitt <carl.e...@gmail.com> wrote:

It seems to me that 'authority' and 'permission' are systematically ambiguous.

Carl, have you put in any effort at all to understand what the ocap community means by "permission" vs "authority"? If so, let's do a bit of active listening. Please summarize in your own words an explanation that you believe accurately represents the position of those in the ocap community who use these terms to make a useful distinction. What is that distinction?

If you don't know what distinction we are trying to make, then...

 

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CA%2BymXc1Q8aa3uEMSYDY76cZgvYBQWb5usRdusMfeRSoXYvHLQA%40mail.gmail.com.

[Carl Hewitt Twitter: ProfCarlHewitt]

Yes, I have spent hours at FriAM listening and debating these points.

The result is that I have become increasingly dissatisfied with the "permission" and "authority" jargon.

Regards,

Carl

https://professorhewitt.blogspot.com/

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK-_AD7sVocQm8sL3Y1%2BCDps5OFe21ST%3D6ADCHM4EH6xpXL9Zw%40mail.gmail.com.

[Matt Rice]

On Wed, Jun 23, 2021 at 8:41 PM 'Ben Laurie' via cap-talk <cap-...@googlegroups.com> wrote:

On Wed, 23 Jun 2021 at 19:04, Jonathan Aldrich <jonathan...@cs.cmu.edu> wrote:

On Wed, Jun 23, 2021 at 1:59 PM Mike Stay <meta...@gmail.com> wrote:

I would say that it's a wrong question. You can ask what authority an
object reference conveys; the holder of a reference may use that
authority or may not.

Does it help if I rephrase the question as follows: "Does a reference to object o convey the authority to read and write to the file?"

That's not even a question in capability-speak. If you have the thing you can do the thing. That's the definition of a capability.

I would just like to counter this with: there exist objects which are useful precisely because they do not wield the authority which they are given, even when that authority is conveyed by the objects which they return.

I'm probably shifting the perspective from the object o, to the constructor of o however.  It is somewhat the nature of the keykos factory, that you put capabilities in, it doesn't wield them, and prevents their escape.

The confined domain (o itself) still conveys authority, Anyhow that is the framing where the particular nuances Jonathan describes makes sense to me in that it allows some static checking of what exists in the keykos factory merely as a trust relationship.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CABrd9SQdpNbW0KH2538Ztdjsbbacz_Lqp5nDrwf0G_L5QsjE5w%40mail.gmail.com.

[Carl Hewitt Twitter: ProfCarlHewitt]

PS. Maybe we should have a discussion at FriAM sometime ;-)

[Mike Stay]

On Wed, Jun 23, 2021 at 3:18 PM Carl Hewitt Twitter: ProfCarlHewitt
<carl.e...@gmail.com> wrote:
>
> PS. Maybe we should have a discussion at FriAM sometime ;-)

Only if you "summarize in your own words an explanation that you

believe accurately represents the position of those in the ocap
community who use these terms to make a useful distinction. What is

that distinction?" Otherwise we'd just be talking past each other.

[Carl Hewitt Twitter: ProfCarlHewitt]

Seems only fair for it to be symmetric.

Mark could summarize in his own words an explanation that he

believes accurately represents Actor Theory position on "Actor address",

"event", "communication", "event induction", "region of mutual exclusion",

and "precedes partial ordering".

See the following:

• https://papers.ssrn.com/abstract=3418003
• https://papers.ssrn.com/abstract=3459566

Then we could attempt a mutual understanding.

Regards,

Carl

https://professorhewitt.blogspot.com/

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAKQgqTa25rYrSFGz98ko%3D16K4Rk0NuiFhUkLmAUefgHEuPXfNw%40mail.gmail.com.

[Mark S. Miller]

Although I agree that may be fair, I do not accept the challenge. It looks like we will continue talking past each other, which makes me sad. I do not understand your modern Actor Theory, but I do not pretend to. 

How would you feel about substituting Classic Actor Theory?

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CA%2BymXc3t7LPvk6X3NbBbNDm1SaDQzmnGughH7YEBuED%2Bs8%3DikQ%40mail.gmail.com.

[Carl Hewitt Twitter: ProfCarlHewitt]

Unfortunately, work from a long time ago did not define Actors up to a unique isomorphism.

Consequently, "Crock Actors" are not easily explainable :-(

However, Crock or someone else might like to try ;-)

Would expect to encounter many ambiguities and security holes :-(

Regards,

Carl

https://professorhewitt.blogspot.com/

[Jonathan Aldrich]

Thanks to Scott and Mark for the pointers to your papers!

Interestingly, the definition of authority we're thinking of differs from the one in  "Permission and Authority Revisited." Take my example, with the restriction that "callback" can have no direct or transitive effects on file, but can write to mutable state of other objects.  (That restriction is one we can check in our Wyvern language, due to our effect checking system).  "Permission and Authority Revisited" would conclude that o has no authority over file, because there is no (well-typed) sequence of calls to methods of o that result in the file object changing.  Considering Eventual, Behavioral, or Maximal authority doesn't change this.  (The result *is* different, of course, if we allow callback to have a direct or transitive effect on file).  But our intuition is that o does have authority over file, because even if none of o's methods can have an effect on file, o can exfiltrate the file to others, which can then have an effect on it; they must have gotten the authority from somewhere, so we conclude o must have had that authority.

Regarding the "Declarative Policies for Capability Control" paper, it's interesting to compare "influences" to what we're trying to define with authority.  In thinking this through, my preliminary intuition is that I want to define the authority of an object independent of its context (i.e. quantifying over all possible programs that surround it).  This basically precludes including objects from the context as different contexts will have different objects...yet an object can certainly "influence" objects in its context via information flow from method return values, etc.  But I can see how appealing to information flow is very natural and useful for a whole set of questions surrounding authority.

Thanks also to others for the discussion.  One note, I was going to reply to Ben but Matt beat me to it--the reason we are asking the question is because we want to think about objects that may have a capability to an object but are specifically constructed to use it in limited ways (they attenuate its authority)...and we also want to think about objects that don't use an object but may return it to clients that can use it (the case that "Permission and Authority Revisited" doesn't seem to capture).

Best,

Jonathan

--

You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK5yZYjeXawZJ6soVuv%2BO7yomwbmA2ooDdCokASXGQNNpKPZYw%40mail.gmail.com.

[Mark S. Miller]

Let me try out a different framing that I think may clear up a number of things. But again, I am not a formalist, so I need your feedback.

For any one authority analysis frame of reference, we must first define which code is defender vs attacker. For the defender code, we reason about specific code, to determine if it means what we think it means, even under attack from potential attackers. For attackers, we're reasoning not about specific code, but about all possible attackers that may have been admitted into that attacker role. We also define yet other code as being the platform on which the others rest, which sets the rules for interaction among them. We reason about the platform only as this set of rules. We separately reason about whether the code implementing the platform correctly enforces these rules. 

This three way split --- platform, defender, attacker --- defines one frame of reference. Alice wants to know if she is safe from Bob. Bob wants to know if he is safe from Alice. Code that Alice uses for defense Bob sees as a potential attacker, and vice versa. An overall authority analysis looks at a system from several of these frames of reference. Least authority is motivated by considering at least two frames of reference: What happens if this module I'm using does what I think it does, as part of my enforcement logic on potential attacker code? But what if I'm wrong and it has a bug? How much damage can that same module do to me? For this purpose, I'm lumping "If I'm mistaken about what this code means" with "If it were other admissible code".

When we think things through intuitively, we often do so from multiple such frames of reference at once, which we need to do!, but which makes our terminology confusing. If we consider each frame of reference separately, do our terms make more sense?

I propose that, within a single given frame of reference, defenders provide and attenuate permissions and authority, but defenders do not *have* authority. If authority is the ability to *cause* effects, then we need to reason about causality. Reasoning about causality means reasoning about counterfactuals, comparing different possible worlds. For your `o` object, we have specific code in front of us. You ask the right question about whether `o` has a certain authority: What could it have done if its code had been different. But in the frame of reference where `o` is the defender, this question makes no sense. `o` cannot be different within this question. It is the defender code we're reasoning about. If the `o` code were different, our analysis is asking a different incommensurate question.

In the frame of reference where `o` is a potential attacker, then the causation question is meaningful. What `o` can cause is the differences in the effects it can have, depending on what its admissible code actually does. This question now makes sense because we're no longer reasoning about specific `o` code, but all possible admissible `o` code. Static checks potentially make the "admissible" constraint more powerful. In some languages, if `o` must implement T, and T is parametrically typed over the opaque type File, then `o` can only pass the file around. It can give it to something else that can do things with it, but it cannot do these things itself. In this case, even though `o` has direct access to the file object, because the admission rules prevent it from doing anything directly to the file, it does not have permission to the file. However, if it may or may not hand it to something that can cause an effect on the file, then it can cause an effect on the file. It has authority to file. In this frame of reference, holding the defender code constant, including the admission rules it imposes on attackers such as `o`, the file will or will not be affected depending on what the code of `o` is.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANwk4UZcFX70XxcMa51aV-mfpLrrPyPx%2Bh6hcb%2Bgji%3DOEnp-zg%40mail.gmail.com.

[Mark S. Miller]

[+Bill Tulloh] adding Bill Tulloh to this thread. 

Bill, the multiplicity of frames of reference below fits well into our decision alignment framework. See https://groups.google.com/g/cap-talk/c/r6JVShHBh0o/m/u2kTfewQBQAJ for the full thread.

[Ben Laurie]

On Thu, 24 Jun 2021 at 02:10, Jonathan Aldrich <jonathan...@cs.cmu.edu> wrote:

Thanks to Scott and Mark for the pointers to your papers!

Interestingly, the definition of authority we're thinking of differs from the one in  "Permission and Authority Revisited." Take my example, with the restriction that "callback" can have no direct or transitive effects on file, but can write to mutable state of other objects.  (That restriction is one we can check in our Wyvern language, due to our effect checking system).  "Permission and Authority Revisited" would conclude that o has no authority over file, because there is no (well-typed) sequence of calls to methods of o that result in the file object changing.  Considering Eventual, Behavioral, or Maximal authority doesn't change this.  (The result *is* different, of course, if we allow callback to have a direct or transitive effect on file).  But our intuition is that o does have authority over file, because even if none of o's methods can have an effect on file, o can exfiltrate the file to others, which can then have an effect on it; they must have gotten the authority from somewhere, so we conclude o must have had that authority.

Regarding the "Declarative Policies for Capability Control" paper, it's interesting to compare "influences" to what we're trying to define with authority.  In thinking this through, my preliminary intuition is that I want to define the authority of an object independent of its context (i.e. quantifying over all possible programs that surround it).  This basically precludes including objects from the context as different contexts will have different objects...yet an object can certainly "influence" objects in its context via information flow from method return values, etc.  But I can see how appealing to information flow is very natural and useful for a whole set of questions surrounding authority.

Thanks also to others for the discussion.  One note, I was going to reply to Ben but Matt beat me to it--the reason we are asking the question is because we want to think about objects that may have a capability to an object but are specifically constructed to use it in limited ways (they attenuate its authority)...and we also want to think about objects that don't use an object but may return it to clients that can use it (the case that "Permission and Authority Revisited" doesn't seem to capture).

I've thought about it a bit more and I realise my response was not particularly useful. :-)

It is, of course, entirely possible to wrap a capability in code that reduces its authority (in effect) and it sounds like your system could perhaps do that - if the callback is constrained to, say, only read and to not have static storage. In general, the ability to reason about code from untrusted parties is a very useful thing to combine with capabilities, IMO.

Is "no static storage" also enforceable in Wyvern?

 

Best,

Jonathan

On Wed, Jun 23, 2021 at 4:24 PM Mark S. Miller <eri...@gmail.com> wrote:

Wow, great thread that I cannot yet spend much time on. But you should be aware of another formalization at

Permission and Authority Revisited: towards a formalization

https://research.google/pubs/pub45570/

with Sophia, James, and Toby, cc'ed

Also, Darya (cc'ed) had a hilarious slide about the dozen or so meanings she found for "permission" vs "authority" in the ocaps literature.

--

  Cheers,
  --MarkM

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK5yZYjeXawZJ6soVuv%2BO7yomwbmA2ooDdCokASXGQNNpKPZYw%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANwk4UZcFX70XxcMa51aV-mfpLrrPyPx%2Bh6hcb%2Bgji%3DOEnp-zg%40mail.gmail.com.

[Jonathan Aldrich]

It is, of course, entirely possible to wrap a capability in code that reduces its authority (in effect) and it sounds like your system could perhaps do that - if the callback is constrained to, say, only read and to not have static storage. In general, the ability to reason about code from untrusted parties is a very useful thing to combine with capabilities, IMO.

Is "no static storage" also enforceable in Wyvern?

Yes!  In fact, Wyvern has no static storage at all, so this is enforced for all Wyvern code.  More broadly, it's also possible to enforce "does not capture any state"; all Wyvern types that are not declared with the "resource" keyword may not capture state.

Best,

Jonathan

[Scott Moore]

I find this framing very appealing! I think there is a natural relationship to how the information-flow community thinks about principals, particularly when thinking about frames of references. For example, if component A can cause some effect by interacting with B, then clearly A and B together have the authority to cause the effect, but A alone does not—B could always prevent them. Decomposing the problem in this way has nice properties in that it can separate questions about code and behaviors from questions of trust, which you can reason about separately. An interesting example of using this decomposition to reason carefully about information flow is in this recent paper presenting an authorization logic for specifying trust relationships for information-flow: https://akhirschwebsite.files.wordpress.com/2020/10/trcameraready-1.pdf.

As an aside, a “crazy idea” I have nursed for a while is that *all* of the traditional security notions (confidentiality, integrity, availability, etc) boil down to this causal notion (which you could perhaps re-brand the phrase integrity). For example, availability is integrity of termination. But perhaps more subtly, confidentiality mostly matters because it effects the integrity of future effects: I don’t want you to know my credit card information so that you can’t interfere with my ability to spend my money, I don’t want you to know my deep secrets because you might ostracize me and prevent me from having social interactions I want, etc.

You received this message because you are subscribed to a topic in the Google Groups "cap-talk" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/cap-talk/r6JVShHBh0o/unsubscribe.
To unsubscribe from this group and all its topics, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK-_AD7uqKf5NRy3iLcNidd_VFZ2BiXyy8UGncu-DjP9VuG3qg%40mail.gmail.com.

[Chris Hibbert]

On 6/23/21 8:08 PM, 'Mark S. Miller' via cap-talk wrote:
> This three way split --- platform, defender, attacker --- defines one
> frame of reference. Alice wants to know if she is safe from Bob. Bob
> wants to know if he is safe from Alice. Code that Alice uses for defense
> Bob sees as a potential attacker, and vice versa. An overall authority
> analysis looks at a system from several of these frames of reference.
> Least authority is motivated by considering at least two frames of
> reference: What happens if this module I'm using does what I think it
> does, as part of my enforcement logic on potential attacker code? But
> what if I'm wrong and it has a bug? How much damage can that same module
> do to me? For this purpose, I'm lumping "If I'm mistaken about what this
> code means" with "If it were other admissible code".

Thanks for this description, MarkM. I found it to clarify Jonathan's
question immensely. We shouldn't be thinking about the "security" of a
small fragment of code in isolation. In order to make useful judgements,
we have to know more about context. What is it defending against, and
what does it rely on?

Chris
--
Rationality is about drawing correct inferences from limited,
confusing, contradictory, or maliciously doctored facts.
-- Scott Alexander

Chris Hibbert
hib...@mydruthers.com
Blog: http://www.pancrit.org
Twitter: C_Hibbert_reads
http://mydruthers.com

[David Nicol]

Okay, I'll bite. (I have no specific relevant credentials outside of being present on this list a long time.)

On Wed, Jun 23, 2021 at 10:43 AM Jonathan Aldrich <jonathan...@cs.cmu.edu> wrote:

Imagine you have an object constructed by the following pseudocode expression:

let o = new object {

    def invoke(callback) {

        callback(file)

    }

}

In the pseudocode above, "file" is a resource in the file system; I am assuming that reading or writing to that file is an effect we are interested in.  Now the question: does the object o above have authority to the file?

[...]

What do you think?  Does the above analysis make sense to you?

As Mr. Duke and others have pointed out, the question distills to "what authority to the file does the symbol 'file' convey here, as that is what is getting presented to the callback."

I would like to say that I see the root of the confusion here having to do with the inherent ambient authority in unix file security, and this idea that capability security can mitigate that, (which may be largely true, but not to the point of making it hard to get wrong.)

Were "file" to represent an already-opened file descriptor, rather than a text string representing a named file system object, the question would disappear -- "file" would have whatever authority got returned from open().

--

"Lay off that whiskey, and let that cocaine be!" -- Johnny Cash

[Matt Rice]

On Thu, Jun 24, 2021 at 3:08 AM 'Mark S. Miller' via cap-talk <cap-...@googlegroups.com> wrote:

Let me try out a different framing that I think may clear up a number of things. But again, I am not a formalist, so I need your feedback

Not being the person to whom you solicited such feedback, I hope I don't step on any toes by giving my feedback despite that.

 

For any one authority analysis frame of reference, we must first define which code is defender vs attacker. For the defender code, we reason about specific code, to determine if it means what we think it means, even under attack from potential attackers. For attackers, we're reasoning not about specific code, but about all possible attackers that may have been admitted into that attacker role. We also define yet other code as being the platform on which the others rest, which sets the rules for interaction among them. We reason about the platform only as this set of rules. We separately reason about whether the code implementing the platform correctly enforces these rules. 

In my experience i encountered questions similar to Jonathan's primarily in platform code, and what you say is "reasoning about whether code implementing the platform correctly enforces these rules",

once the rules are formally specified, and mechanically checked we can think of this in two ways allowing arbitrary code to be checked against the platform rules (which is perhaps cavalier), or checking the specific code for the platform as it changes, ensuring it continues to enforce the rules...

platform code is in the weird situation where alice and bob are both simultaneously attacker and defender, and a platform's primary purpose should be to maintain collaboration despite conflict.

There are multiple ways that can be taken: is it just a tool for the developer of the platform, or is it a mechanism for Alice to show Bob that a program under Alice's control is actually following the rules, and Bob trusts the rules and enforcement of them.

I don't consider these multiple cases much different from the perspective of what needs to be formalized, the first of those is IMO easier to justify.

Anyhow that is the frame of reference which I find myself interested in mostly.

 

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK-_AD7uqKf5NRy3iLcNidd_VFZ2BiXyy8UGncu-DjP9VuG3qg%40mail.gmail.com.

[Mark S. Miller]

In the context of Wyvern and the question Jonathan is asking, I believe `file` is a first class object that, under Unix, would encapsulate both a file descriptor number and the authority to use it via, say, Unix system calls. The `file` object attenuates its* Unix system call authority to provide only the authority to affect only this one file. But there are plenty(!) of Wyvern experts here that can answer definitively.

In the frame of reference where such file objects are defenders, `o` is an attacker, and `o` got admitted on condition that it passes Wyvern static checks that it does not access its `file` argument directly, but can pass it on to those that do, I'd say

The `file` object provides authority to the file.

The `o` object has direct access to the `file` object, but (because of the admission constraints) does not have permission to the `file` object.

The `o` object does have authority to the `file` object, and does have the authority that the `file` object provides to affect the file it represents.

[*] By saying simultaneously "its ... authority" and " `file` is a defender" I seem to contradict my earlier stance. However, I'd argue this is more of a symptom of how we need to fluidly shift between frames of reference to carry through an analysis. The object that the `file` object encapsulates, that enables it to make Unix system calls, enables it to do so even if its code were different, i.e., even if it were an attacker of unknown code that we're quantifying over. I chose the term "frame of reference" exactly to suggest the physics analogy that the statements true in one frame of reference have to be consistent with the statements that are true within any other frame of reference within the same system, where the algebra of "consistent with" is much of the content of the theory. For ocaps, the "consistent with" constraint between frames of references is that the authority `x` has as an attacker can be no greater than the authority that the objects it holds provide to potential attackers. And `x` considered as a defender, holding as much else constant as possible (there be dragons alert) cannot provide more authority than the authority it held as a potential attacker. When it provides less, it attenuates the authority it has been given.

OTOH, the need to make such a shift, even to analyze simple statements like this, may argue against this whole frames-of-reference framework. Or at least that it should draw coarser distinctions so we can avoid fine grain shifts during one simple argument.

--

  Cheers,
  --MarkM

[David Nicol]

On Thu, Jun 24, 2021 at 4:02 PM Mark S. Miller <eri...@gmail.com> wrote:

In the context of Wyvern and the question Jonathan is asking, I believe `file` is a first class object that, under Unix, would encapsulate both a file descriptor number and the authority to use it via, say, Unix system calls. The `file` object attenuates its* Unix system call authority to provide only the authority to affect only this one file. But there are plenty(!) of Wyvern experts here that can answer definitively.

Huh. In the context of someone who doesn't know Wyverns from Dragons, I figured "file" was a symbol with a value that would get closed over by the constructor.

 

[Jonathan Aldrich]

Thanks Mark for the framing suggestion, and others for the follow-on discussion--this has been very helpful!  In my example I want to view o as the defender, I think, and I want to ask what authority is provided by o.  And I am looking at that question in the context of a particular platform, Wyvern, that provides certain guarantees, both about capability safety and about sound static effect tracking.

To confirm and clarify, Mark is right that in my example 'file' is a first-class object---i.e. a capability---that in unix would encapsulate both a file descriptor number and the authority to use it.

Best,

Jonathan

--

You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK5yZYj4A2TJuUmGkZuKawNfiKZJ6K1%2BFztVQ-vMuG89X3qeJg%40mail.gmail.com.

[Mark S. Miller]

Splitting hairs, it is consistent with the frame of reference in which `o` is a defender to ask "What authority is provided to `o`?" but not "What authority does `o` have?". Thus, as stated, your message is consistent with this framing.

Is this helpful?

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANwk4UajLVUePvCJYTQWjNHMtBvW-sD3bAmzQXt-785Z9w5Ltg%40mail.gmail.com.

[Jonathan Aldrich]

Yes, thanks!

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK-_AD4MZsLuqNoT_CUjw8dTFPoq_J7%2BDKzrYaJwyeduv_juVg%40mail.gmail.com.

[Carl Hewitt Twitter: ProfCarlHewitt]

Thanks Chris and MarkM for enlarging the perspective!

With respect to "security" and other properties, entire digital system needs to be able to be modeled.

Is there something that the Actor Abstraction left out?

Cheers,

Carl

https://professorhewitt.blogspot.com/

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/542d67f9-9339-25db-a70a-89c55e75d928%40mydruthers.com.

[Carl Hewitt Twitter: ProfCarlHewitt]

One possible way to model what is possible is founded on the the Actor "precedes" partial order on events, which is characterized up to a unique isomorphism.

Of course, higher-level predicates for Actor Systems must be formulated for proof using Event Induction.

Regards,

Carl

https://professorhewitt.blogspot.com/

[Jonathan S. Shapiro]

With the clarification that the object holds a capability to “file” from construction, this becomes a fairly classic question in static vs dynamic authority.

Static authority is always an approximation. It provides a worst-case bound on what could happen. Usually without examining code and always without examining dynamic behavior. Often this conservative worst case statement is sufficient given the question you are ultimately trying to examine. When it isn’t, stronger methods get applied to narrow the understanding of authority, ranging from static control flow analysis, to model checking, to formal [mechanized] verification.

So to some extent, the answer to the original question depends on the level of analysis applied. I would say that if an object provably has no [transitive] reachability then it is easy to answer “no.” The moment this test can no longer be satisfied, the answer must become conservatively correct, which is to say “yes, until through some deeper analysis we prove that it does not.”

Jonathan