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.
--
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.
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.
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAKQgqTa3XH%2BYaWVtoBAgUXHvmKFD%3DuQX-UzPXA3XiVU-2MbErA%40mail.gmail.com.
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".
--
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.
--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/ef17ccdb-c8fe-4f21-9cee-024ab14f81a1n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANwk4UZKygkARQUxvMTOFFC08O_Z9iBqZdU275TJV9FsSAoyiA%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANpA1Z0pEK6Z34GwbxCpiw4hOUEpX5mpi3cgez8nLYKGN7B68A%40mail.gmail.com.
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANwk4UZKygkARQUxvMTOFFC08O_Z9iBqZdU275TJV9FsSAoyiA%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/CAK5yZYjeXawZJ6soVuv%2BO7yomwbmA2ooDdCokASXGQNNpKPZYw%40mail.gmail.com.
It seems to me that 'authority' and 'permission' are systematically ambiguous.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CA%2BymXc1Q8aa3uEMSYDY76cZgvYBQWb5usRdusMfeRSoXYvHLQA%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK-_AD7sVocQm8sL3Y1%2BCDps5OFe21ST%3D6ADCHM4EH6xpXL9Zw%40mail.gmail.com.
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CABrd9SQdpNbW0KH2538Ztdjsbbacz_Lqp5nDrwf0G_L5QsjE5w%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/CAKQgqTa25rYrSFGz98ko%3D16K4Rk0NuiFhUkLmAUefgHEuPXfNw%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CA%2BymXc3t7LPvk6X3NbBbNDm1SaDQzmnGughH7YEBuED%2Bs8%3DikQ%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/CAK5yZYjeXawZJ6soVuv%2BO7yomwbmA2ooDdCokASXGQNNpKPZYw%40mail.gmail.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.
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--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 atPermission and Authority Revisited: towards a formalization
with Sophia, James, and Toby, cc'edAlso, 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.
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?
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.
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?
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK-_AD7uqKf5NRy3iLcNidd_VFZ2BiXyy8UGncu-DjP9VuG3qg%40mail.gmail.com.
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.
--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANwk4UajLVUePvCJYTQWjNHMtBvW-sD3bAmzQXt-785Z9w5Ltg%40mail.gmail.com.
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.
--
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.