Best formal backing for ocap security?

[Christopher Lemmer Webber]

I'm aware of the existence of, but haven't read, some research talking
about ocap security in much more formal terms. Much of the basis for
talking about ocaps I've done is based on storytelling, because I'm more
of a narrative person personally in how I think than a formalist. But,
I recognize that collaborating with formal methods researchers is good.

We're going to be putting out an episode on our FOSS & Crafts podcast
about ocaps as "Hygiene for a Computing Pandemic". To better back that,
I'd ask: what are the papers you think best back these ideas? Narrative
answers can be helpful too, but more rigorous methods are extra good.

Even classic monte-carlo methods are valuable, if well backed. ;)

- Chris

[Tristan Slominski]

Checkout Assume Guarantee reasoning. Paper links in the video I think 

https://www.youtube.com/watch?v=IQd7RIQEFTQ

--
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/87v9chkahg.fsf%40dustycloud.org.

[Mark S. Miller]

http://wiki.erights.org/wiki/Documentation#Formal_Methods

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

[Christopher Lemmer Webber]

Thanks to both of you!

>> https://groups.google.com/d/msgid/cap-talk/CAOXxbHwmNNFT9sx5R5RH2kVZAHmswh96%3DcXgHasOnDovoE-cUQ%40mail.gmail.com
>> <https://groups.google.com/d/msgid/cap-talk/CAOXxbHwmNNFT9sx5R5RH2kVZAHmswh96%3DcXgHasOnDovoE-cUQ%40mail.gmail.com?utm_medium=email&utm_source=footer>
>> .
>>

[Jonathan Aldrich]

A couple of years ago, some colleagues and I studied a link between capabilities and formal reasoning in the form of effect systems:

Capabilities: Effects for Free. Aaron Craig, Alex Potanin, Lindsay Groves, and Jonathan Aldrich. Proc. International Conference on Formal Engineering Methods (ICFEM), 2018.  http://www.cs.cmu.edu/~aldrich/papers/effects-icfem2018.pdf

The paper formalizes the very basic idea that you can only have an effect if you have the capability that can perform it.  Although the approach works for any application of effects, the motivating examples are security-related.

Cheers,

Jonathan

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/87o8i9k76f.fsf%40dustycloud.org.

[Mark S. Miller]

This is great work. Highly recommended!

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

--

  Cheers,
  --MarkM

[Carl Hewitt]

Thanks Jonathan!

    [Craig et. al. 2018] illustrate the power of strong types along with the Actor Laws of Locality [Hewitt and Baker 1977] with an example of a logging procedure, which uses an append-only file and a read-only socket using the following type definitions:

   Logging:[AppendOnlyFile, ReadOnlySocket ]→Logger // Logging is a procedure that takes

                                                              // an append-only file and a read-only socket returning a logger

   AppendOnlyFile  interface append[String]→Void  // AppendOnlyFile  is an interface that implements

                                                                                        // the message append[String] returning Void

   ReadOnlySocket  interface read→String     // ReadOnlySocket  is an interface that that implements

                                                                                   // the message read returning a String 

Using the Laws of Locality discussed in this article, it is easy to see that given afile:AppendOnlyFile  and aSocket:ReadOnlySocket  that Logging_.[afile, aSocket]   is thereby provided the means to only send read to aSocket and append[aString] to afile, where aString:String. According to the Laws of Locality while communicating across the Internet, a string provided by a read-only socket could perhaps provide information about the addresses of Actors on remote computers, which might in turn provide access to local Actors.

What did I miss from [Craig et. al. 2018]?

Thanks!

Carl

On Fri, Jan 1, 2021 at 8:29 PM Jonathan Aldrich <jonathan...@cs.cmu.edu> wrote:

[Jonathan Aldrich]

Dear Carl,

What you write accurately positions our example in the context of the Actor Laws of Locality.  And thank you for doing that, by the way--our paper was generally positioned with respect to more recent work on capabilities, but we missed the chance to highlight the historical connection to actors and including this would have enriched it.  We'll take care to do this in any follow-on work.

Of course, the example itself is not really the contribution of our paper--as you observe, it is an application of longstanding principles of actor and capability systems.  Rather, our contribution is showing that you can combine strong types with capability-based (or laws of locality-based) reasoning to get the formal benefits of an effect system.  We chose to investigate effect systems because they formally capture "what code can do"--which is the most basic thing you get from capabilities.  We develop a strong type system that is enhanced with effects.  We then observe that we can avoid doing effect analysis inside a module, and instead infer an upper bound that module's effect based on the capabilities it has access to (as revealed in its type).  The main proof in the paper shows that this reasoning is mathematically sound.

So what the paper does is connect the arguments made (sometimes informally) about capabilities to formal reasoning in the form of effects, and show that those arguments can be made rigorous in this setting.

We hope the paper will have two impacts.  The first impact is obviously a technical advance in effect systems: our approach can make effect systems both more powerful and more usable by allowing capabilities to reason about the effect of code that is not itself effect-annotated.  The second impact is less technical, but perhaps broader and more relevant to this audience: even if you don't use the formal effect system we developed, our paper supports confidence in the human reasoning that the capabilities community has been doing by showing that it *can* be formalized.  This may help more formalists (who sometimes have a tendency to discount anything that's not formalized) to understand why what we're doing has value.

This second piece is, of course, also supported by the other formal work mentioned in this thread.  All bricks in a wall that is hopefully growing more solid with time. :)

Cheers,

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/CA%2BymXc1_TXqTbE4YwP16KP7M0RHOT3gVAe6zy-NXqu2YZzbybg%40mail.gmail.com.

[Carl Hewitt]

Dear Jonathan,

Thanks for your insightful response!

The most fundamental task is to characterize computation up to a unique isomorphism.

Only by rigorously characterizing computation, can we know what we are doing.

Unless I missed something, it doesn't look like your axiomatization

characterizes computation up to a unique isomorphism?

I am most concerned about proving security properties of Citadels because they are 

fundamental to the future of representative government and civil liberties.  

The importance of Citadels is developed here:

          Project Liftoff: Universal Intelligent Systems (UIS) by 2030    
                 https://papers.ssrn.com/abstract=3428114

What kind of security properties can we have for Citadels?

With respect to the example:

   Logging:[AppendOnlyFile, ReadOnlySocket ]→Logging

  AppendOnlyFile  interface append[String]→Void      

   ReadOnlySocket  interface read→String 

Using the Laws of Locality, it is easy to see that 

given afile:AppendOnlyFile  and aSocket:ReadOnlySocket  that

Logging_.[afile, aSocket]   is thereby provided the means to append to afile and

to read from aSocket.

To go beyond the above, claims (like the kinds in your paper) 

can be made about what Actor addresses are held by 

the implementation of the procedure Logging 

For a device in a Citadel, what assumptions would be 

reasonable for the device to make about 

the implementation of the procedure Logging, 

which is implemented on another device in the Citadel?

Would attestation provide sufficient grounds for such assumptions?

Cheers,

Carl

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANwk4Ua2Y8%3DG3YiXgnFKCueAoRh7-F%2BsbRb9brJ-0hSqfcqZbw%40mail.gmail.com.

[Christopher Lemmer Webber]

Jonathan Aldrich writes:

> Dear Carl,
>
> What you write accurately positions our example in the context of the Actor
> Laws of Locality. And thank you for doing that, by the way--our paper was
> generally positioned with respect to more recent work on capabilities, but
> we missed the chance to highlight the historical connection to actors and
> including this would have enriched it. We'll take care to do this in any
> follow-on work.
>
> Of course, the example itself is not really the contribution of our
> paper--as you observe, it is an application of longstanding principles of
> actor and capability systems. Rather, our contribution is showing that you
> can combine strong types with capability-based (or laws of locality-based)
> reasoning to get the formal benefits of an effect system. We chose to
> investigate effect systems because they formally capture "what code can
> do"--which is the most basic thing you get from capabilities.

BTW, it strikes me there are really two versions of "what code can do"
that people mean:

- An actor's change of its own internal behavior/state (popularly,
"become")
- Effects in from or out to the outside world

I read most of your paper today (thought it seemed quite good, despite
my limitations of understanding notation); I think most of it focused on
the latter more than the former, is that right?

I suspect both would be interesting to be able to demonstrate/analyze
though. There may be value in being able to perform an invocation that
is demonstratably "read-only", including to actor state changes.

Thanks for your excellent paper btw!

>> Logging:*[**AppendOnlyFile*, *ReadOnlySocket **]*→*Logger* // Logging

>> is a procedure that takes
>>
>> // an
>> append-only file and a read-only socket returning a logger
>>

>> *AppendOnlyFile * *interface* *append*[*String**]*→*Void* // *AppendOnlyFile
>> * is an interface that implements
>>
>>
>> // the message* append*[*String**]* returning *Void*
>>
>> *ReadOnlySocket * *interface* *read*→*String* // *ReadOnlySocket * is

>> an interface that that implements
>>
>>

>> // the message* read* returning a *String*

>>
>> Using the Laws of Locality discussed in this article, it is easy to see

>> that given afile:*AppendOnlyFile * and aSocket:*ReadOnlySocket * that
>> Logging.*[*afile, aSocket*]* is thereby provided the means to only send*
>> read* to aSocket and* append*[aString*]* to afile, where aString:*String*.

>> According to the Laws of Locality while communicating across the Internet,
>> a string provided by a read-only socket could perhaps provide information
>> about the addresses of Actors on remote computers, which might in turn
>> provide access to local Actors.
>>
>>
>> What did I miss from [Craig et. al. 2018]?
>>
>>
>> Thanks!
>>
>> Carl
>>
>> On Fri, Jan 1, 2021 at 8:29 PM Jonathan Aldrich <
>> jonathan...@cs.cmu.edu> wrote:
>>
>>> A couple of years ago, some colleagues and I studied a link between
>>> capabilities and formal reasoning in the form of effect systems:
>>>
>>> Capabilities: Effects for Free

>>> <http://www.cs.cmu.edu/~aldrich/papers/effects-icfem2018.pdf>. Aaron

>>> Craig, Alex Potanin, Lindsay Groves, and Jonathan Aldrich. Proc.
>>> International Conference on Formal Engineering Methods (ICFEM), 2018.
>>> http://www.cs.cmu.edu/~aldrich/papers/effects-icfem2018.pdf
>>>
>>> The paper formalizes the very basic idea that you can only have an effect
>>> if you have the capability that can perform it. Although the approach
>>> works for any application of effects, the motivating examples are
>>> security-related.
>>>
>>> Cheers,
>>>
>>> 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/CA%2BymXc1_TXqTbE4YwP16KP7M0RHOT3gVAe6zy-NXqu2YZzbybg%40mail.gmail.com

>> <https://groups.google.com/d/msgid/cap-talk/CA%2BymXc1_TXqTbE4YwP16KP7M0RHOT3gVAe6zy-NXqu2YZzbybg%40mail.gmail.com?utm_medium=email&utm_source=footer>
>> .
>>

[Carl Hewitt]

Thanks Chris!

As as you pointed out, the following kinds of kinds of "effects" have been discussed:

1. Changes that have occurred because
   an Actor made changes in its own internal state
2. Changes that have occurred because 
   Actors have been sent messages causing
   some of them to change their own respective local state.

It can be difficult to show that no changes have 

occurred as a result of sending a message to 

an Actor on another device in a Citadel because 

logging, caching, etc. may have taken place.

Cheers,

Carl

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/87turx3mhp.fsf%40dustycloud.org.

[Alan Karp]

Carl Hewitt <carl.e...@gmail.com> wrote:

 

It can be difficult to show that no changes have 

occurred as a result of sending a message to 

an Actor on another device in a Citadel because 

logging, caching, etc. may have taken place.

You might find it easier to understand what's going on if you separate changes to application state from those orthogonal to it, such as logging, caching, etc.

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

[Christopher Lemmer Webber]

"Yes, and..." as the improv people say.

I'm not sure if I'll have read your use of the term "citadel" correctly
(how far does it encompass "externalized device access"?), but maybe
there's some degree of "when do messages cause changes to something
*outside* of the citadel"...

Assuming some sort of well-controlled, well-understood fortress, what
about those who watch for or listen to noises from outside the gates?
What about those who shout at or wave flags to outsiders?

Interestingly, I think in general most people concerned with effects
tend to be worried about changes that affect things "outside of the
process"... "if it doesn't perform external effects, that must mean it's
safe, because the program can't do much damage". However, there's also
value in realizing that even internal object behavior/state changes
(inside the ~citadel?) are also important.

Interestingly, I think all of these kinds of "effects" can be
encapsulated between two scopes:

1) Actor "become" or behavior/state change, within an observed process
(or process set, or actor collection).

2) Changes *outside* of that observed set of actors, either to:

2a) boundary-external distributed objects/actors

2b) "devices" that might be local-ish, eg some kind of local-ish IO
(these can be conceptually actor'ified but aren't always, and I
feel like this is what most people tend to worry about)

Interestingly fewer people seem too worried about the "become" stuff in
terms of safety (clearly Carl is, and I am, and most people here are); I
suspect a lot of that has to do with traditional concepts of process
boundaries. And you can get a lot with mostly focusing on (2);
Sandstorm is a nice example of that I think, and is clearly valuable.
But in my game world stuff I worry about changes to local-only objects
(eg I don't want you to graffiti all over my walls). Interestingly,
Carl's two points clearly show by contrast a lot of interest in terms of
(1) very directly. (2) is probably also fully encompassed, clearly
actors are set up for it... though the term "citadel" is interesting;
how far do the castle walls go? The ability to cooperate with parties
*not* in your ~citadel is valuable even when full observation is not
possible. Cooperating cities with some level of safety and not needing
to resort to imperialistic takeover seems like a lot of the promise of
actors. (Okay, that got a bit rambly.)

Carl Hewitt writes:

> Thanks Chris!
>
> As as you pointed out, the following kinds of kinds of "effects" have been
> discussed:
>

> 1. Changes that have occurred because

> an Actor made changes in its own internal state

> 2. Changes that have occurred because

[Carl Hewitt]

Thanks Alan!

Taking the difference into account is a fundamentally good idea :-)

However, for many Intelligent Applications, it is going to be very difficult to 

separate application information from other ontological information.

Regards,

Carl

--

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/CANpA1Z2Mfn8xJwHTqEWN1%2BfAiHGOw%2BhM8P59jy-DhLn0AGLcBA%40mail.gmail.com.

[Carl Hewitt]

Thanks Chris!

With respect your writing:

"I'm not sure if I'll have read your use of the term "citadel" correctly

(how far does it encompass "externalized device access"?)

A home citadel should ideally encompass 
all the devices of a home including router, car, big screen, smart phones, etc.
Military citadels are similarly local.

Cheers,
Carl

[Alan Karp]

Carl Hewitt <carl.e...@gmail.com> wrote:

However, for many Intelligent Applications, it is going to be very difficult to 

separate application information from other ontological information.

True, but it might be a good architectural principle to keep them separate to the greatest extent possible.  

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

[Carl Hewitt]

An Intelligent Systems application needs to ontologically integrate its own information together with system information as well as information from other applications.

--

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/CANpA1Z0HTt1Mi6nOEigAc%3Dowf0GcNDSgh6wg9PjLoyLDgTejog%40mail.gmail.com.

[Carl Hewitt]

PS. Unless I am missing something, your programming language seems incapable of concurrency :-(

How would your results change if concurrency is included?

[Jonathan Aldrich]

On Sun, Jan 3, 2021 at 1:33 PM Christopher Lemmer Webber <cwe...@dustycloud.org> wrote:

BTW, it strikes me there are really two versions of "what code can do"
that people mean:

 - An actor's change of its own internal behavior/state (popularly,
   "become")
 - Effects in from or out to the outside world

I read most of your paper today (thought it seemed quite good, despite
my limitations of understanding notation); I think most of it focused on
the latter more than the former, is that right?

That's right, effects out to the outside world is the focus of our "Capabilities: Effects for Free" paper.

 

I suspect both would be interesting to be able to demonstrate/analyze
though.  There may be value in being able to perform an invocation that
is demonstratably "read-only", including to actor state changes.

Definitely a lot of value there!

In my group, we've done a little bit of work on using lightweight types for this, and while it's not explicitly positioned with respect to capabilities or actors, there may be some relevance.  For example, our work on Plural, a typestate-checking system for Java, provides static reasoning about state changes within the object (abstracted as a finite set of high-level states).  Plural also included static permissions that restrict what you can do with an object; one of these is a "pure" permission that prohibits state change in invocations.  An overview paper is:

1. Modular Typestate Checking of Aliased Objects. Kevin Bierhoff and Jonathan Aldrich. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '07), October 2007.  http://www.cs.cmu.edu/~kbierhof/papers/typestate-verification.pdf

We did a fair bit of follow-on work including empirical evaluation in various Java codebases, extension to a concurrent setting, and exploration of this in a setting with a primitive "become" for typestates.  I can point you to more if interested, or just see the papers on my web page.  It would be interesting to explore this explicitly in the world of actors and/or look at the interactions with capability-based reasoning.

Thanks for your excellent paper btw!

Thanks for the kind words and interesting questions!

Cheers,

Jonathan 

[Jonathan Aldrich]

Hi Carl,

Thanks for your questions!

No, we haven't characterized computation up to a unique isomorphism in this particular system--our focus is on what you can learn from lightweight types, and a syntactic formalism (small-step operational semantics plus typing rules) is sufficient for that.  Certainly more powerful mathematical techniques would permit stronger reasoning--lots of work to do in this area more generally!

You're right that our paper on capabilities and effects was formalized without concurrency.  We aren't reasoning about effects that are specific to concurrency, and the capability-based reasoning we are formalising appears to be independent of concurrency, so I expect (but don't know for sure, of course, without doing the work) that our results would extend to that setting under reasonable assumptions (e.g. that race conditions can't break capability safety / memory safety).

I need to spend a bit of time absorbing your paper on Citadels before responding to your other questions, so I'll have to get back to you on that.

Thanks,

Jonathan

[Christopher Lemmer Webber]

Here's a suspicion I have:

- You probably are able to add this with concurrency... within the same
"runtime" or at least with the right "trusted overseer".

- Once you try to do something like CapTP's assumption of cooperation
across a *mutually suspicious* network where many participants are
*remotely opaque*, I think you're going to lose access to this. (The
point where this might be false is if the "remote vat/machine" is
actually something like a blockchain... but that throws away the
"remotely opaque" part of it.)

To some degree, I think this is because traditional type checkers
structurally tend to resemble central planners...? (That may make it
sound like I'm diminishing this; I'm not. It's clear that the
Effects-for-Free paper is an enormous contribution for local
effect-causing-capabilities analysis. I think the "central planner"
phrasing just makes it clear why they don't seem to work across mutually
suspicious boundaries.) The blockchain example is a good example of how
to subvert this, but then again blockchains are decentralized
centralization. Happy to be demonstrated wrong here.

Here's where I think Typed Racket does something interesting by having
centrally statically-type-checked systems that are opaque possibly to
all but the runtime environment with connections to
dynamically-type-checked modules... they can speak to each other, but do
contract checks across the boundaries (recent work has made these
contract checks much faster, using two different techniques... "Shallow
Typed Racket" is the new one I think not yet discussed on this list).
I've previously thought this was the answer for "how do we allow for
local static type checking but also survive something like a captp
machine boundary?" but interestingly it seems to *not* help with the
"external effects" side of things... probably because you're already
external! The best you could do is have a trusted "remote" overseer,
and see whether you believe them or not.

Just thinking about this out loud. I'm still not fully sure of the
words I'm typing. What do you think Jonathan? Does this align with
your thinking?

>> *Unless I missed something, it doesn't look like your axiomatization*
>> *characterizes computation up to a unique isomorphism?*
>>
>> *I am most concerned about proving security properties of Citadels because
>> they are *
>>
>> *fundamental to the future of representative government and civil
>> liberties. *

>>
>> The importance of Citadels is developed here:
>> Project Liftoff: Universal Intelligent Systems (UIS) by 2030
>> https://papers.ssrn.com/abstract=3428114
>>

>> *What kind of security properties can we have for Citadels?*

>>
>> With respect to the example:
>>

>> Logging:*[**AppendOnlyFile*, *ReadOnlySocket **]*→*Logging*
>>
>> * AppendOnlyFile * *interface* *append*[*String]*→*Void*

>>
>> *ReadOnlySocket * *interface* *read*→*String*
>>
>>

>> Using the Laws of Locality, it is easy to see that
>>

>> given afile:*AppendOnlyFile * and aSocket:*ReadOnlySocket * that
>>

>> Logging.*[*afile, aSocket*]* is thereby provided the means to append to

>> afile and
>>
>> to read from aSocket.
>>
>>
>> To go beyond the above, claims (like the kinds in your paper)
>>
>> can be made about what Actor addresses are held by
>>
>> the implementation of the procedure Logging
>> For a device in a Citadel, what assumptions would be
>> reasonable for the device to make about
>> the implementation of the procedure Logging,
>> which is implemented on another device in the Citadel?
>>

>> *Would attestation provide sufficient grounds for such assumptions?*

>>>> Logging:*[**AppendOnlyFile*, *ReadOnlySocket **]*→*Logger* // Logging

>>>> is a procedure that takes
>>>>
>>>> // an
>>>> append-only file and a read-only socket returning a logger
>>>>

>>>> *AppendOnlyFile * *interface* *append*[*String**]*→*Void* // *AppendOnlyFile

>>>> * is an interface that implements

>>>>
>>>>
>>>> // the message* append*[*String**]* returning
>>>> *Void*
>>>>
>>>> *ReadOnlySocket * *interface* *read*→*String* // *ReadOnlySocket

>>>> * is an interface that that implements

>>>>
>>>>
>>>> // the message* read* returning a *String*
>>>>

>>>> Using the Laws of Locality discussed in this article, it is easy to see

>>>> that given afile:*AppendOnlyFile * and aSocket:*ReadOnlySocket * that

>>>> Logging.*[*afile, aSocket*]* is thereby provided the means to only

>>>> send* read* to aSocket and* append*[aString*]* to afile, where aString:

>>>> *String*. According to the Laws of Locality while communicating across

>>>> the Internet, a string provided by a read-only socket could perhaps provide
>>>> information about the addresses of Actors on remote computers, which might
>>>> in turn provide access to local Actors.
>>>>
>>>>
>>>> What did I miss from [Craig et. al. 2018]?
>>>>
>>>>
>>>> Thanks!
>>>>
>>>> Carl
>>>>
>>>> On Fri, Jan 1, 2021 at 8:29 PM Jonathan Aldrich <
>>>> jonathan...@cs.cmu.edu> wrote:
>>>>
>>>>> A couple of years ago, some colleagues and I studied a link between
>>>>> capabilities and formal reasoning in the form of effect systems:
>>>>>
>>>>> Capabilities: Effects for Free

>>>>> <http://www.cs.cmu.edu/~aldrich/papers/effects-icfem2018.pdf>. Aaron

>>>>> Craig, Alex Potanin, Lindsay Groves, and Jonathan Aldrich. Proc.
>>>>> International Conference on Formal Engineering Methods (ICFEM), 2018.
>>>>> http://www.cs.cmu.edu/~aldrich/papers/effects-icfem2018.pdf
>>>>>
>>>>> The paper formalizes the very basic idea that you can only have an
>>>>> effect if you have the capability that can perform it. Although the
>>>>> approach works for any application of effects, the motivating examples are
>>>>> security-related.
>>>>>
>>>>> Cheers,
>>>>>
>>>>> 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/CA%2BymXc1_TXqTbE4YwP16KP7M0RHOT3gVAe6zy-NXqu2YZzbybg%40mail.gmail.com

>>>> <https://groups.google.com/d/msgid/cap-talk/CA%2BymXc1_TXqTbE4YwP16KP7M0RHOT3gVAe6zy-NXqu2YZzbybg%40mail.gmail.com?utm_medium=email&utm_source=footer>
>>>> .

>>>>
>>> --
>>> 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/CANwk4Ua2Y8%3DG3YiXgnFKCueAoRh7-F%2BsbRb9brJ-0hSqfcqZbw%40mail.gmail.com
>>> <https://groups.google.com/d/msgid/cap-talk/CANwk4Ua2Y8%3DG3YiXgnFKCueAoRh7-F%2BsbRb9brJ-0hSqfcqZbw%40mail.gmail.com?utm_medium=email&utm_source=footer>
>>> .
>>>
>>

[Jonathan Aldrich]

On Mon, Jan 4, 2021 at 3:13 PM Christopher Lemmer Webber <cwe...@dustycloud.org> wrote:

Here's a suspicion I have:

 - Once you try to do something like CapTP's assumption of cooperation
   across a *mutually suspicious* network where many participants are
   *remotely opaque*, I think you're going to lose access to this.  (The
   point where this might be false is if the "remote vat/machine" is
   actually something like a blockchain... but that throws away the
   "remotely opaque" part of it.)

Yes, that's a great question.  I said that adding concurrency is probably not difficult, but of course distribution is a much different thing.  Our method assumes that all code that runs is typechecked...which is true in a trusted virtual machine but may not be true (in general) of a remote machine you don't control.

It seems like remote attestation would be one way to solve this--i.e. before interacting with a remote virtual machine, you ensure it is running a VM that (for example) will not run code that does not typecheck.  But I guess this also gives up some amount of remote opaqueness.  To be more precise, the properties of the VM that is running cannot be opaque, but it's still OK for what actually runs on that VM to be opaque.  So the "central planning" (in your terms) has limited scope.  Not sure whether that falls within the realm of CapTP specifically?

Cheers,

Jonathan

[Mark S. Miller]

It does not. We assume a network of mutually suspicious nodes, including mutually suspicious blockchains. By having the infrastructure not make any implicit decisions to "trust"---be vulnerable to---the behavior of other nodes, the programs that run on the nodes can be built according to rely on other nodes to the degree locally considered appropriate.

Blockchains are already vastly more trustworthy than remote attestation because their mechanisms are open to inspection. Being run on a blockchain, or under attestation, or by an individual that you happen to consider honest, are all forms of evidence that can be used in making decisions to be vulnerable. But those decisions must be diverse and subjective.

Agoric applies this even to the transparency of blockchains. When running contracts under an instance of Zoe, you can ask that Zoe instance for the text and instantiation parameters ("terms") of that contract. A well behaved Zoe will provide that honestly. A Zoe run on a proper blockchain will do so honestly, and run the contact only according to the semantics of the code. But the Zoe instance itself reifies into a namable object, these decisions about which blockchains (or attenstations or whatever) to trust to be honestly transparent in this manner.

That's also why implicit linear types, though tremendously useful(!!), cannot be used to provide direct linguistic support for exclusive rights transfer. Any solution that can enforce decentralized exclusive rights transfer can solve the double spending problem. But the only known good solution to double spending is to build a blockchain to provide a highly credible virtual machine. But different blockchains will be differently credible to different parties. We need to reify those differences into distinct objects (issuers and Zoe instances) that we can treat differently.

[Bill Frantz]

On 1/4/21 at 6:02 PM, jonathan...@cs.cmu.edu (Jonathan Aldrich) wrote:

> It seems like remote attestation would be one way to solve this--i.e.
> before interacting with a remote virtual machine, you ensure it is running
> a VM that (for example) will not run code that does not typecheck.

Yes, but how do do this in the face of a nation-state attacker.

Cheers - Bill

-----------------------------------------------------------------------
Bill Frantz | When all else fails: | Periwinkle
(408)348-7900 | Voice and CW. | 150 Rivermead Rd #235
www.pwpconsult.com | | Peterborough, NH 03458

[Mark S. Miller]

Especially one that has likely already issued a national security letter to the hardware manufacturers forcing them to install a trap door and not tell anyone.

That's why blockchains are the first solution to supply chain vulnerabilities we've ever had. And still the only solution so far.

--
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/r480Ps-10146i-5DE7323455D3416ABCC7D01FC314263F%40Williams-MacBook-Pro.local.

--

  Cheers,
  --MarkM

[Bill Frantz]

On 1/4/21 at 10:12 PM, eri...@gmail.com (Mark S. Miller) wrote:

>That's why blockchains are the first solution to supply chain
>vulnerabilities we've ever had. And still the only solution so far.

I've been thinking about mitigating supply chain vulnerabilities
by using agressive POLA and many protection domains in
software/hardware. Standard stuff, but it is incredibly hard to
do right with current OSes. Look at the Postfix email server for
a worked example and think about how much easier it is to
specify in a capability secure language like E, or
Java/Javascript with restrictions.

If things were easier to do, people might do them more often.

Cheers - Bill


----------------------------------------------------
Bill Frantz | Art is how we decorate space,
408-348-7900 | music is how we decorate time.
www.pwpconsult.com | -Jean-Michel Basquiat

[Mark S. Miller]

How does that help against trapdoors built into cpus by the manufacturer?

--
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/r480Ps-10146i-A7C1A32AB3DC45619DC03B5144D1DD6F%40Williams-MacBook-Pro.local.

--

  Cheers,
  --MarkM

[Raoul Duke]

On Mon, Jan 4, 2021 at 8:13 PM Mark S. Miller <eri...@gmail.com> wrote:

How does that help against trapdoors built into cpus by the manufacturer?

eg if plain text glyphs ever show up on some display device for humans to read then it must not be possible to really be secure?

[Mark S. Miller]

Hi Raoul, I don't understand. Does this relate to supply chain vulnerabilities?

--
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/CAJ7XQb5T37K-fwN_4KubMeGmi9przd1eKpo9%2B88x%3DrPZHAOBOA%40mail.gmail.com.

--

  Cheers,
  --MarkM

[Raoul Duke]

I may have jumped off the train tracks apologies if so.

Maybe things-that-are-over-my-head could make cloud computing "safe"... like maybe homomorphic encryption or super heterogeneous consensus voting cloud of cloud things might be able to give us more chance to prevent black hats from interfering with our computations?

but i have to inject my plaintext somehow. and i want to read my plaintext somehow. 

[mostawe...@gmail.com]

I have written on my whiteboard a reminder to explain The DRM Problem. Below that, I have a note for The Inverse DRM Problem. I don't think that they're solvable, which is why they seem relevant to formal methods, and they are applicable to the direction to which the thread has turned.

The DRM Problem is simple: It seems impossible to make DRM work. In particular, it doesn't seem workable to give an actor a cryptographic payload, a key, and some sort of non-local trusted (read: bogus) promise that the actor will only apply the key to the payload under certain conditions. More generally, in any category which understands that some computations are non-local, it doesn't seem workable to give an actor an arrow (read: a function) and an element (read: a value) and trust the actor to only compose the element with the arrow (read: apply the function to the value) only under certain conditions.

The Inverse DRM Problem is much trickier to state. Informally, we might imagine that we could publish cryptographic payloads to a hyperbolically-connected (public) network; how can we hide those payloads from network operators? Grepping my #erights logs, I see that the examples I've mentioned are:

* SGX or other secure-computing enclaves: how can a customer actually be secure in an SGX context when there are so many sensors and side-channels right next door?

* Unguessable refs at scale: how can pirates or dissidents or other rebels share refs to Bittorrent or other public content-addressed payloads without Eve finding out about the rebels and their refs? (The conversation was more mundane: how can a Monte user download a module from Bittorrent without Eve gaining a list of potentially-vulnerable modules to use as an attack surface?)

Like I said, I think that these might be fundamental obstacles. The DRM Problem seems provably problematic, and in practice, it certainly seems to frustrate game publishers regularly. I think that The Inverse DRM Problem is just as impossible to deal with, but proving it seems so much harder and I don't know if there's fundamental stegonographic techniques that we could bring to bear. It could well be that this is dependent upon which of Impagliazzo's Five Worlds we're in; maybe this is related to whether public-key cryptography is even possible! Depressing, but it would at least indicate to us what we could try to build.

[Jonathan Aldrich]

I agree that remote attestation would not be trustworthy against nation-state adversaries--and perhaps others, depending on your threshold of trust and your confidence in the technical approach being used.

Even with this caveat, type-based mechanisms--such as our approach to reasoning about effects based on capabilities and types--can play a role in distributed security.  Although you don't know if the adversary is running the typechecker on his VM, you know that you are running it on yours.  So if it's a VM that you or someone you trust controls, you can use types to assess the risk of running less-trusted code on your VM.  One way of looking at our paper (and other lightweight formal work in this space) is an example of how types can give you additional useful properties beyond memory- and capability-safety.

Cheers,

Jonathan

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

[Mark S. Miller]

On Tue, Jan 5, 2021 at 9:31 AM mostawe...@gmail.com <mostawe...@gmail.com> wrote:

I have written on my whiteboard a reminder to explain The DRM Problem. Below that, I have a note for The Inverse DRM Problem. I don't think that they're solvable, which is why they seem relevant to formal methods, and they are applicable to the direction to which the thread has turned.

The DRM Problem is simple: It seems impossible to make DRM work. In particular, it doesn't seem workable to give an actor a cryptographic payload, a key, and some sort of non-local trusted (read: bogus) promise that the actor will only apply the key to the payload under certain conditions.

For bizarre enough definitions of "actor", "give", and "conditions", we can trivially do the following:

We encrypt the payload and/or key with another key, an encryption key, publish the resulting doubly encrypted thing, and set up an actor on a blockchain such that when the corresponding decryption key is given to it, or published in an expected place, this actor will decrypt the encrypted thing, revealing the original cryptographic payload and key, and apply that key to that payload, as can everyone else.

We define the "certain conditions" as the release of that decryption key, or any condition which would trigger the release of that decryption key.

I mention this not because I think it actually solves anything or is even interesting, but to ask you to clarify what you mean so that such possibilities are excluded.

 

More generally, in any category which understands that some computations are non-local, it doesn't seem workable to give an actor an arrow (read: a function) and an element (read: a value) and trust the actor to only compose the element with the arrow (read: apply the function to the value) only under certain conditions.

The Inverse DRM Problem is much trickier to state. Informally, we might imagine that we could publish cryptographic payloads to a hyperbolically-connected (public) network; how can we hide those payloads from network operators? Grepping my #erights logs, I see that the examples I've mentioned are:

* SGX or other secure-computing enclaves: how can a customer actually be secure in an SGX context when there are so many sensors and side-channels right next door?

* Unguessable refs at scale: how can pirates or dissidents or other rebels share refs to Bittorrent or other public content-addressed payloads without Eve finding out about the rebels and their refs? (The conversation was more mundane: how can a Monte user download a module from Bittorrent without Eve gaining a list of potentially-vulnerable modules to use as an attack surface?)

Like I said, I think that these might be fundamental obstacles. The DRM Problem seems provably problematic, and in practice, it certainly seems to frustrate game publishers regularly. I think that The Inverse DRM Problem is just as impossible to deal with, but proving it seems so much harder and I don't know if there's fundamental stegonographic techniques that we could bring to bear. It could well be that this is dependent upon which of Impagliazzo's Five Worlds we're in; maybe this is related to whether public-key cryptography is even possible! Depressing, but it would at least indicate to us what we could try to build.

 

On Monday, January 4, 2021 at 10:22:48 PM UTC-8 rao...@gmail.com wrote:

I may have jumped off the train tracks apologies if so.

Maybe things-that-are-over-my-head could make cloud computing "safe"... like maybe homomorphic encryption or super heterogeneous consensus voting cloud of cloud things might be able to give us more chance to prevent black hats from interfering with our computations?

but i have to inject my plaintext somehow. and i want to read my plaintext somehow. 

--
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/0cf5664a-64cc-4c96-b374-820255064403n%40googlegroups.com.

--

  Cheers,
  --MarkM

[Christopher Lemmer Webber]

You've given some interesting examples of what the "Inverse DRM Problem"
might be, but it might still be useful to have a short textual
definition, since I've never heard that phrase before. Here's an
attempt at the "DRM Problem", which might be useful for inversing:

Alice would like to share information with Bob which Bob can use and
experience *without* Bob being able to share with others. This
despite some aspect of Bob being unconfined (at minimum, Bob as a user
sitting in front of their computer.)

The generalization of the DRM Problem is the "Delegation Myth". Ocap
people know (?) this, that delegation cannot be *technically* prevented
for unconfined participants (the rest of the world seems in denial).
DRM tends to focus on a specific use-case, readable media (though in the
general case the issue of delegation also shows up in other authority
type issues that aren't necessarily about readable media).

Notably, DRM's "success" today comes not from technical systems, but
threat of severe punishment for exploring workarounds via draconian
"intellectual restrictions laws" (btw, I advocate saying this phrase
rather than "intellectual property laws"; it's much clearer).

Less onerous solutions can also exist without law also though; "split
contracts" can have provisions where an arbitrator can flip a switch if
delegation was discovered to have occured. I think this is a worthwhile
thing to emphasize: it gives hope for the survival of doctor-patient
confidentiality for instance.

Starting from there then, what is the "Inverse DRM Problem"? I get a
sense of what you're hinting at, but not how to state it. It seems to
have to do with something like:

- Trying to force "effect safety" on the other side of a mutually
suspicious system seems similar (maybe it's even the same)

- Something something users running encryption foo on a remote enclave;
a hopefully better job of the "cloud" upholding users' needs (?)

Why "inverse", also? Perhaps it's an inversion of my sympathy...
"inversion of the DRM perversion". Instead of desiring it for what
appears to be a user-freedom-harming reason, our *desire* for this here
seems to be about upholding the wills and intentions of users. So it
seems more "positive"... I'm at least more sympathetic. But is there
anything about the mechanism that is inverted? It seems mostly the
same. Is that your thinking?

[Mark S. Miller]

Agree completely! Each analysis exercise starts by setting up a frame of reference that divides all relevant code into: defensive code, potentially offensive code, platform code. The platform code creates the rules enforced on the defensive and offensive code. The analysis assumes these ground rules, and so implicitly assumes correct platforms, so these assumptions must be constrained to what platform code can enforce under our overall trust assumptions. For distributed systems, there are only a few major structures of distributed trust assumptions. Let's start with what I like to call "The Classic Cypherpunk Reference Scenario":

Alice trusts Alice's machine but does not trust Bob's. Alice runs her defensive code on her own platform, interacting with Bob's code running on Bob's machine. For this analysis, the trusted platform is only

   * Alice's machine and OS and language implementation on up to Alice's defensive code we'll analyze.

   * The laws of physics, constraining what Bob's machine can possibly do, given only knowledge that it is physically separate from Alice's machine.

   * The cryptographic protocols by which Alice and Bob's machine interact with each other.

Within these constraints, Bob's machine and Bob's code together form the potentially offensive "code" that we'll analyze.

Alice's defensive code is specific code. Alice analyzes this code to understand whether it means what she thinks it means.

Since Alice doesn't trust Bob's platform it doesn't matter to her what code Bob alleges to run on that platform. Alice does not reason about the internal structure of such a potentially offensive system. Rather Alice wants to ensure that the computational properties she cares about holds over all possible systems that Bob might run, constrained only by the above constraints. She can therefore reason about her own defensive code richly, using all the tools of static analysis, fancy type checking, effects systems, static verification that she wants.

If the laws of physics + the cryptographic protocol constrain Bob's system, from Alice's POV, to distributed capability rules, then Alice can assume that Bob's system can only utilize --- exercise or further pass on --- capabilities that have been given to it, i.e., that have been sent to any object which is a component of Bob's system. But Alice cannot confine Bob. She cannot know what other Bob-like agents Bob may be connected to. The only capabilities that Alice can know are denied to Bob are capabilities created on Alice's system that she has not lost control of --- that she has not shared with anything that she does not trust to deny these to Bob.

So, linguistic support for distributed security can be divided along these lines. For the defensive code side, there's no limit to the benefit we can get by more analysis of our own code. IOW, Alice is not in a position to confine Bob. Bob is an "uncontrolled subject".

For the offensive side, we must stay within the limits of physics + what the limits of what cryptographic protocols can enforce. Within those limits, we would like linguistic support for reason about whatever the constraints are that we can enforce. We know that distributed caps (ocaps-without-confinement-or-unforgeability) are within those constraints, and of course we know that we can provide natural linguistic support for reasoning within those constraints. 

But distributed caps use only very basic crypto. We now have a vast menu of fantastic cryptographic primitives, including Zero knowledge proofs and multiparty secure computation. What more can cryptographic protocols enforce that we can usefully cast in linguistic terms? I don't know the answer to that. What linguistic constraints clearly lie outside those limits? A lot. Even something as simple as linear types is outside those limits, because it is equivalent enough to the double spending problem which is also outside those limits.

The next structure of distributed trust assumptions is E-like systems, which is the Classic Cypherpunk Reference Scenario + potentially offensive mobile code that can be confined. IOW, Alice's analysis includes in the potentially offensive code category code that Bob sends to Alice, over the cryptographic protocol, that Alice then runs locally, on her platform, in a confinement box that her platform makes possible. The main difference this makes is that Alice, still treating Bob's code as a blockbox constrained only by ocap constraints, is now limited to capabilities that Alice gives to it. It no longer has prior connectivity opaque to Alice. 

Besides confinement, Alice *could* use further static analysis on this code, refusing to run any Bob code that doesn't pass some static checks. She can explain these static rules to Bob, so that Bob knows that the code he sends to Alice must satisfy these static checks in order for Alice to be willing to run it. So, static checks that enforce constraints beyond ocaps are now possible. But what are useful? This is another open question. Many of the constraints that people have thought to impose by static checks, like various information-flow constraints, I am quite skeptical of. But perhaps much useful could be done here.

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

--

  Cheers,
  --MarkM

[Bill Frantz]

On 1/4/21 at 11:12 PM, eri...@gmail.com (Mark S. Miller) wrote:

>How does that help against trapdoors built into cpus by the manufacturer?

OK. Remember mitigations, not complete security (which may be
impossible). Since I always think better with a real problem,
let me talk about the network monitoring application that took
over most of the non-classified big government and business systems.

Now it is easy to imagine breaking this application into several
pieces. We have the analysis, reporting, and communication
portions. Starting with communication:

Information gathering (via SNMP)
Network reconfiguration (via SNMP? and ?)
Archival logging
Reporting to authorized users
(Anything else?)

We isolate information gathering and network reconfiguration in
separate modules, and perhaps different computers. We provide a
very limited API to these modules such as
getLoad(networkElement), startFunction(networkElement). As
narrow as we can make it so it is not possible to send arbitrary
data from the callers. Hopefully we can keep pwned callers from
contacting the command and control centers of the attackers.

This code probably has the highest assurance requirement of the
application. We demand that it be provided in source form and
build it locally. We also demand that the build process be a
simple use of make or equivalent. We want to understand what is
going on at this level.


The analysis module(s) use the information gathering module(s)
to discover the state of the network, and process that data to
generate information about that status and recommendations for
improvement. If the analysis results in recommendations for
changes that the app is authorized to make, it sends those
recommendations to the logging modules which will log the action
and use the Network Reconfiguration module to change the network.


The logging module generates log entries and writes them through
a separate module which has append only access to the log files.
We have a high assurance requirement for the log and writelog
modules as they give us insight into what the app is doing.

etc. etc.

Note that if we use separate machines for these functions, we
can improve our protection from CPU trapdoors. If we can have
different chips in the network access machines from the machines
which use them, we might make it necessary to pwne both machines
to effect an attack.

I'm thinking of a collection of Intel/AMD/ARM chips. For the
really paranoid, chip making machinery is available on the
surplus market. Since both Mark and I know one person who has
made chips in her kitchen, making chips is well within the
budget of enterprises the size of the ones attacked recently.

Cheers - Bill

---------------------------------------------------------------------------
Bill Frantz | Re: Computer reliability, performance, and security:
408-348-7900 | The guy who *is* wearing a parachute is
*not* the
www.pwpconsult.com | first to reach the ground. - Terence Kelly

[Alex Potanin]

Hello,

When it comes to supply chain reliability we had some recent real world
discussions here
(https://www.sftichallenge.govt.nz/news/veracity-technology-mission-calling-for-expressions-of-capability/)
where it turned out to be close to impossible to convince non-software
people as to "why they should trust the software" - they seem to assume
that as a given.

So to be able to apply the techniques that Aaron (Jonathan and me) used
in the paper to real world problems - perhaps Mark can suggest how to
explain to the non-software people in a language that normal people can
relate to why it is important? Otherwise, we are talking about
mechanisms like Jonathan does below and indeed can work out all sorts of
cool designs that provide a solution, but not necessarily help with the
problem (being: supply chain reliability)?

Thanks,
Alex.

> <mailto:jonathan...@cs.cmu.edu> (Jonathan Aldrich) wrote:
>
> > It seems like remote attestation would be one way to solve
> this--i.e.
> > before interacting with a remote virtual machine, you ensure
> it is running
> > a VM that (for example) will not run code that does not
> typecheck.
>
> Yes, but how do do this in the face of a nation-state attacker.
>
> Cheers - Bill
>
> -----------------------------------------------------------------------
> Bill Frantz        | When all else fails:      | Periwinkle
> (408)348-7900      | Voice and CW.             | 150 Rivermead
> Rd #235

> www.pwpconsult.com <http://www.pwpconsult.com> |

>            | Peterborough, NH 03458
>
> --
> 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

> <mailto:cap-talk%2Bunsu...@googlegroups.com>.

> To view this discussion on the web visit
> https://groups.google.com/d/msgid/cap-talk/r480Ps-10146i-5DE7323455D3416ABCC7D01FC314263F%40Williams-MacBook-Pro.local

> <https://groups.google.com/d/msgid/cap-talk/r480Ps-10146i-5DE7323455D3416ABCC7D01FC314263F%40Williams-MacBook-Pro.local>.

>
>
>
> --
>   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

> <mailto:cap-talk+u...@googlegroups.com>.

> To view this discussion on the web visit

> https://groups.google.com/d/msgid/cap-talk/CAK5yZYjBP3zMzWxe5Qkw0hZ_M1W-cghG%3D2ZG4uqN6eUaMB2FEQ%40mail.gmail.com
> <https://groups.google.com/d/msgid/cap-talk/CAK5yZYjBP3zMzWxe5Qkw0hZ_M1W-cghG%3D2ZG4uqN6eUaMB2FEQ%40mail.gmail.com?utm_medium=email&utm_source=footer>.

>
> --
> 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

> <mailto:cap-talk+u...@googlegroups.com>.

> To view this discussion on the web visit

> https://groups.google.com/d/msgid/cap-talk/CANwk4Ub__0_Eci%3DYRcsKDhbT2YyM%3D8DDOzb-okGCA2Mk4H6B2A%40mail.gmail.com
> <https://groups.google.com/d/msgid/cap-talk/CANwk4Ub__0_Eci%3DYRcsKDhbT2YyM%3D8DDOzb-okGCA2Mk4H6B2A%40mail.gmail.com?utm_medium=email&utm_source=footer>.

[Mark S. Miller]

On Tue, Jan 5, 2021 at 11:54 AM Alex Potanin <al...@ecs.vuw.ac.nz> wrote:

Hello,

When it comes to supply chain reliability we had some recent real world
discussions here
(https://www.sftichallenge.govt.nz/news/veracity-technology-mission-calling-for-expressions-of-capability/)

What does this document mean by "capability"?

Where is this discussion?

 

where it turned out to be close to impossible to convince non-software
people as to "why they should trust the software" - they seem to assume
that as a given.

If they take as given that they should trust the software, then you should first convince them that they should not trust the software. But I do not feel oriented in your question. What are you trying to convince them to trust, and under what underlying trust assumptions? What counter-productive beliefs to they already have or leap to that you're trying to convince them out of?

 

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/4d46f3cf-f105-14b0-ec4b-28c8bc50054c%40ecs.vuw.ac.nz.

--

  Cheers,
  --MarkM

[Mark S. Miller]

To those formal methods folks who have reasoned formally about the security of programs, does this three way division itself work? The part before we get to particular distributed trust assumptions. I'm especially curious about how well it describes how you reason about the security of Wyvern programs?

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

[Carl Hewitt]

Hi Jonathan,

Just want to make it clear that I think that it is great that your group wrote the article on formal security properties.

Much more work is needed on the foundations of security!

You need to ground your work on a foundation that has characterized computation up to a unique isomorphism ;-)

Concurrency is the future of Intelligent Applications :-)

Cheers,

Carl

[Carl Hewitt]

Remote attestation of an Actor (code + addresses) is 

reasonable to pursue even in the face of attacks from nation-states because

it increases work for the attacker.

Would like to only have to trust hardware provided and then

 audit hardware providers including supply chain.

On Mon, Jan 4, 2021 at 6:00 PM Bill Frantz <fra...@pwpconsult.com> 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/r480Ps-10146i-5DE7323455D3416ABCC7D01FC314263F%40Williams-MacBook-Pro.local.

[Carl Hewitt]

Unfortunately, there are many supply chain attacks that

cannot be defeated just using blockchains :-( 

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

[Carl Hewitt]

Security is a total-stack issue from multiple hardware devices to applications across a Citadel.

Types can be very helpful, especially if the types are Actors and can make use of crypto ;-)

Cheers,

Carl

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

[Mark S. Miller]

On Tue, Jan 5, 2021 at 2:11 PM Carl Hewitt <carl.e...@gmail.com> wrote:

Unfortunately, there are many supply chain attacks that

cannot be defeated just using blockchains :-( 

Of course. But the supply chain attack that blockchains do solve is an essential one that nothing else comes close to solving. It was the most vexing because it was the only essential one that we previously had no solution for.

 

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

--

  Cheers,
  --MarkM

[Carl Hewitt]

As I understand it, crypto ledgers can play a small role in security by enabling detection of erasure of previous entries.

How do you envisage using crypto ledgers to solve a crucial supply chain security issue that cannot be better addressed in another way?

Cheers,

Carl

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

[Mike Stay]

What about obfuscated code? There's a recent paper
"Indistinguishability Obfuscation from Well-Founded Assumptions"
https://eprint.iacr.org/2020/1003
It basically says if Alice sends code to Bob, then Bob can stuff
things up completely or let it run to completion, but nothing in
between. Bob may grant Alice's code extra unexpected authority or
deny her code authority that it expects to be granted, but changing
just one bit of the output of her code is hard. Extracting keys from
her code is hard.

> --
> 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/87k0srtc17.fsf%40dustycloud.org.



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

[Mark S. Miller]

That sounds promising! By itself, Alice's hardware may still be corrupt. But run on multiple hardware with cross checking, this seems to address the same essential vulnerability with much less cross checking.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAKQgqTYzv%3D%3DwZ%2B04Q4nv5nQOHYJMR_bOhj0pnkdT_3nBifishg%40mail.gmail.com.

--

  Cheers,
  --MarkM

[Mark S. Miller]

On Tue, Jan 5, 2021 at 3:28 PM Carl Hewitt <carl.e...@gmail.com> wrote:

As I understand it, crypto ledgers can play a small role in security by enabling detection of erasure of previous entries.

How do you envisage using crypto ledgers to solve a crucial supply chain security issue that cannot be better addressed in another way?

How do you know that the hardware your program runs on actually behaves according to the stated instruction set architecture with no hidden back doors? The EVM (Ethereum Virtual Machine) is a terrible instruction set architecture. But when I run an EVM program on Ethereum, I am reasonably confident that the program outcome reported is according to the semantics of the program run on that architecture. There is no prior machine that has ever provided such credibility that it runs programs honestly.

 

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

--

  Cheers,
  --MarkM

[Mike Stay]

It also allows storing keys in contracts on chain!

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

[Carl Hewitt]

PS. For those of you not on the email list, I am giving a practice talk this Friday.

Cheers,

Carl

https://professorhewitt.blogspot.com

[Mark S. Miller]

This sounds like general purpose multi-party secure computation, which is still way far from practical. In what way does this accomplish less? Or is it similarly expensive? Or is this a breakthrough making MPC practical?

If it is affordable but weaker than MPC, still, from what you said above it sounds like a game changer. Is it?

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

[Mark S. Miller]

https://www.schneier.com/blog/archives/2020/11/indistinguishability-obfuscation.html

Hat tip Bill Tulloh, cc'ed

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK-_AD46%2BEPqot-bm4FHyw8LSa1zSdMzZTAX%2BHMYsi-OJ19CEA%40mail.gmail.com.

--

  Cheers,
  --MarkM

[Bill Frantz]

The more different ways you have of checking a program for
correctness, the more you can trust it to be correct.

One big problem is, "What is correct?" With program proving, a
technology that increases our confidence in a program, we still
need to select the right things to prove. I fear it's turtles
all the way down.

Cheers - Bill

On 1/5/21 at 1:13 PM, jonathan...@cs.cmu.edu (Jonathan

Aldrich) wrote:

>Even with this caveat, type-based mechanisms--such as our approach to
>reasoning about effects based on capabilities and types--can play a role in
>distributed security. Although you don't know if the adversary is running
>the typechecker on his VM, you know that you are running it on yours. So
>if it's a VM that you or someone you trust controls, you can use types to
>assess the risk of running less-trusted code on your VM. One way of
>looking at our paper (and other lightweight formal work in this space) is
>an example of how types can give you additional useful properties beyond
>memory- and capability-safety.

-----------------------------------------------------------------------
Bill Frantz | Privacy is dead, get over | Periwinkle
(408)348-7900 | it. | 150 Rivermead
Rd #235
www.pwpconsult.com | - Scott McNealy (1999) | Peterborough,
NH 03458

[Mike Stay]

On Tue, Jan 5, 2021 at 7:21 PM Bill Frantz <fra...@pwpconsult.com> wrote:
>
> The more different ways you have of checking a program for
> correctness, the more you can trust it to be correct.
>
> One big problem is, "What is correct?" With program proving, a
> technology that increases our confidence in a program, we still
> need to select the right things to prove. I fear it's turtles
> all the way down.

Yeah, compilers can tell you that your code doesn't match your types,
but it can't tell you which one is right. It reminds me of the
concept of a torsor in physics: you can't measure absolute position,
only difference in positions. Ditto for velocities, energies,
voltages, quantum phases, etc.

[Carl Hewitt]

Not being concurrent is a terrible performance hid for Intelligent Applications :-(

Don't see how Ethereum is superior to garden-variety remote attestation?

Also, don't see how this fundamentally advances protection against supply-chain attacks?

Regards,

Carl

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

[Raoul Duke]

also in my mind "types" are never sufficient to guarantee all properties i'd want in a system. advanced types get ever more powerful but then we are back to the "turtles all the way down" that in general from what i have seen of software engineering, we cannot "specify" our way out of even a paper bag. 

[Mark S. Miller]

Attestation by a cpu built to secretly misbehave is worse than useless.

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

[Carl Hewitt]

Auditing may be our best defense?

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK-_AD5SY%2B0%2B_KyxQe1du%2B2LG7O%2B6R131%2B%2BG53kfvioLnUpuOw%40mail.gmail.com.

[Mark S. Miller]

Who audits the auditors?

The ultimate auditing is massive redundancy + massive multiway cross checking, all of which is public, open entry, and cross jurisdictional. IOW blockchain.

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

[Carl Hewitt]

It is certainly true that strong types alone are insufficient to specify many properties of systems.

However, there is a foundation that may be adequate here:

• Information Security Requires Strongly-Typed Actors and Theories

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

• Physical Indeterminacy in Digital Computation

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

Cheers,

Carl

On Tue, Jan 5, 2021 at 8:32 PM Raoul Duke <rao...@gmail.com> wrote:

also in my mind "types" are never sufficient to guarantee all properties i'd want in a system. advanced types get ever more powerful but then we are back to the "turtles all the way down" that in general from what i have seen of software engineering, we cannot "specify" our way out of even a paper bag. 

--

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/CAJ7XQb4LPeN%3Dy-s1DNcV6V4rFYq-BHrE7xEx8gDUcyv3xiq7NA%40mail.gmail.com.

[Carl Hewitt]

Auditing auditors is a well-known issue that is also addressed in financial auditing.

Auditing provides a useful mix of public and private capabilities including recourse to the courts :-)

Don't see any realistic alternative?

Cheers,

Carl

https://professorhewitt.blogspot.com/

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK-_AD6YwpXVOE8rAtVdzCLy6__g_Zj4%2BQeK4GnTF%3DKaxzc%2B9g%40mail.gmail.com.

[Christopher Lemmer Webber]

What strikes me is that this and some of the work on homomorphic
encryption both seem to open many doors, but still don't solve "The DRM
Problem" for the traditional usecase of DRM'ed *media*. They might for
games maybe, because this involves interactive code... but not for a
non-interactive stream of media. Demonstratable in the following way:
a movie must still make it to my eyes and ears, and I can record the
streams of light and sound in-between. My brain would require
significant re-arrangement for this to not be the case. So, DRM'ed
media can still be "ripped" (perhaps it's a lossy rip).

Since the difference between "DRM" and "Inverse DRM" still seems to be
"inversion of my sympathy" (I'm still unsympathetic to DRM), I wonder if
there are similar constraints we can identify on what is and isn't
possible.

Let's put it another way: I would like a therapy program which could
provide therapy for me remotely, which I can talk to about the kinds of
emotional trauma I have experienced. Currently I must rely on a
contract, legal, or reputation based system (or all three currently in
practice, but maybe it can be reduced to two... or more accurately, it's
*potentially feasible* that there's a future where legal is
reconstructed from the other two). A question might be: could I have a
therapist where I don't have to rely on any of those three mechanisms
but the computing environment itself to provide adequate therapy to me,
despite the therapist being a remote process (human or computer)?

I don't expect an immediate answer, but it's an interesting puzzle. I
suspect that for human therapists, the answer is permanently "no". For
computer therapists, it's possible that eventually it's "maybe yes".

But maybe I'd be more of a computer than I currently am myself by that
point.

>>> https://groups.google.com/d/msgid/cap-talk/CAKQgqTZE7xfojGuBayk3N9uBeB0texS9qFjFw0cwdvuMLni%2BSA%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/CAK-_AD46%2BEPqot-bm4FHyw8LSa1zSdMzZTAX%2BHMYsi-OJ19CEA%40mail.gmail.com
>> <https://groups.google.com/d/msgid/cap-talk/CAK-_AD46%2BEPqot-bm4FHyw8LSa1zSdMzZTAX%2BHMYsi-OJ19CEA%40mail.gmail.com?utm_medium=email&utm_source=footer>
>> .
>>
>
>
> --
> Cheers,
> --MarkM

[Bill Frantz]

On 1/6/21 at 12:38 PM, carl.e...@gmail.com (Carl Hewitt) wrote:

>Auditing may be our best defense?

We have a lot of evidence that reading code isn't a good enough
way of catching bugs or trapdoors. How can we improve auditing.

Things like type checking provides automatic audits of some
parts of programs. As such the contribute to better programs.

Cheers - Bill

---------------------------------------------------------------------------
Bill Frantz | "I wish there was a knob on the TV to turn
up the
408-348-7900 | intelligence. There's a knob called
"brightness", but
www.pwpconsult.com | it doesn't work. -- Gallagher

[Carl Hewitt]

Fortunately, there is a lot more to good auditing than just reading code :-)

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/r480Ps-10146i-D3D00AF9D5C74123AEE2B551A55B25D6%40Williams-MacBook-Pro.local.

[Raoul Duke]

i am an optimist by nature (joke) and i never kneejerk rant about anything...

what exactly does auditing cover here, i wonder? there's probably more than one connotation.

e.g.

money is fungible and recoverable in some sense that my private data is not. and already the financial stuff seems to be slightly tinged with keystone cops scratching each other's backs look the other way just claim it is allright under GAAP type scandals that are only sussed out long after the fact.

similarly "i am shocked, shocked" that the entire us gov't was powned due to homogeneity and BAAD (that's my newly coined sarcastic term) security practices. maybe somebody was even officially 'auditing' those software installations?

now if it were digital automatic auditing that helped apply defense in depth spackle then that's still recursively open to sploits but maybe maybe perhaps of use but really hard to know the true roi vs. the snake oil. 

or auditing in a formal methods sense of very good software engineering rather than triplicate ISO TPS reports?

i dare say the "dismal science" moniker should be transferred in a ceremony of pomp over to computer security  :-)

[Alan Karp]

Christopher Lemmer Webber <cwe...@dustycloud.org> wrote:

a movie must still make it to my eyes and ears, and I can record the
streams of light and sound in-between.  My brain would require
significant re-arrangement for this to not be the case.  So, DRM'ed
media can still be "ripped" (perhaps it's a lossy rip).

The analog hole has always been the way around DRM.  The argument made in court is that a copy made that way is less than full fidelity, so the copyright holder's rights are preserved.

Years ago I proposed that digital music be downloaded for a specific device's modulation transfer function (MTF).  Playing that copy on a different device would result in less than full fidelity since no two physical devices have the exact same MTF.

 

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

[Raoul Duke]

> The analog hole has always been the way around DRM. The argument made in court is that a copy made that way is less than full fidelity, so the copyright holder's rights are preserved.

tell that to the AIs. :-)

https://www.youtube.com/watch?v=fo_eZuOTBNc

[Alan Karp]

Raoul Duke <rao...@gmail.com> wrote:

> The analog hole has always been the way around DRM.  The argument made in court is that a copy made that way is less than full fidelity, so the copyright holder's rights are preserved.


tell that to the AIs. :-)

I said that it was argued in court.  I did not say the argument made sense.

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

[Bill Frantz]

And I remember getting a tape recorder when I was a young teen
so I could record, off the air, the top 40. Do you really think
I cared about the quality of the recording?

Cheers - Bill

-----------------------------------------------------------------------
Bill Frantz | Concurrency is hard. 12 | Periwinkle
(408)348-7900 | out 10 programmers get it | 150 Rivermead
Rd #235
www.pwpconsult.com | wrong. - Jeff Frantz | Peterborough,
NH 03458

[Bill Frantz]

On 1/6/21 at 1:16 PM, carl.e...@gmail.com (Carl Hewitt) wrote:

> Fortunately, there is a lot more to good auditing than just reading code :-)

At least a partial list please.

Cheers - Bill

--------------------------------------------------------------
Bill Frantz | There are now so many exceptions to the
408-348-7900 | Fourth Amendment that it operates only by
www.pwpconsult.com | accident. - William Hugh Murray

[mostawe...@gmail.com]

Presumably the reference is to E-style auditors (http://www.erights.org/elang/kernel/auditors/); these give us the ability to prove arbitrary properties (yes, invoking Rice's Theorem along the way!) about objects. The object who creates the proof, the auditor, is given the target object's script (AST), consent, and binding guards, but not the actual values in the object's closure. This both allows for a modicum of isolation, and also allows for situations where an auditor's proof is cached and reused every time a maker creates an object.

For a practical example, Monte modules are audited by a well-known auditor, DeepFrozen, who proves that the modules are transitively immutable and also that the module's exported values are transitively immutable. In the above situation, this would allow Alice to load code from Bob with limited trust; Alice can be confident that merely loading and instantiating modules from Bob will not be enough for Bob to exfiltrate data from Alice, just computation.

Indeed, with Chris' explanations, Bob suffers both a DRM and Inverse DRM problem: any objects which Bob asks Alice to construct, Alice can choose to instantiate multiple times and in altered contexts, and Bob cannot trust Alice to perform any computation as-is; additionally, Alice sees the source code of every object which Bob wants to instantiate using Alice's computational context.

This is dire enough that I've considered adding a Miranda method for Monte objects so that they reveal their ASTs by default, so that we don't delude ourselves into false security and also have an easier time of code generation. Following Kerckhoff's principle, what exactly is gained by letting objects conceal how they're built? There's only three cases:

* The object is local to Alice's vat and has no Monte source code; `null` is fine

* The object is local to Bob's vat but can be reconstructed on Alice's vat; the source code is available indirectly from Bob's messages to Alice

* The object is local to Bob and Alice only gets a DRM'd projection of the object; the source code is available as soon as Bob unlocks the object so that Alice can compute with it

None of this stymies MarkM's point about e.g. Ariana Grande releasing her new single by requiring people to each pay for an individualized cryptographic lockbox, and then publishing the corresponding keys for free at a set date. This is like a virtual concert, but amortizes the cost of the bandwidth of the encrypted concert stream during the prerelease sale period. I would argue (not to put words in Chris' mouth) that this is not really DRM in the traditional sense; before the key's publication, there's *no* conditions that would allow for unlocking the content. It's akin to more classical notions of copyright; the artificial right to make copies is restricted until the sale period has lasted long enough to remunerate the artist.

[Mike Stay]

Indistinguishability obfuscation is, as you noted, still merely
possible, not efficient. In the meantime, this is a fun way to
obfuscate code:

On Tue, Jan 5, 2021 at 4:38 PM Mike Stay <meta...@gmail.com> wrote:
>
> What about obfuscated code? There's a recent paper
> "Indistinguishability Obfuscation from Well-Founded Assumptions"
> https://eprint.iacr.org/2020/1003
> It basically says if Alice sends code to Bob, then Bob can stuff
> things up completely or let it run to completion, but nothing in
> between. Bob may grant Alice's code extra unexpected authority or
> deny her code authority that it expects to be granted, but changing
> just one bit of the output of her code is hard. Extracting keys from
> her code is hard.
>

> > --
> > 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/87k0srtc17.fsf%40dustycloud.org.

[Mike Stay]

D'oh! Here's the link.
https://www.youtube.com/watch?v=HlUe0TUHOIc

[Carl Hewitt]

Dear Jonathan,

I am wondering if the "effects" in the article are Actor events?

Thanks!

Carl

https://professorhewitt.blogspot.com/

[Carl Hewitt]

Dear Jonathan,

What are "effects" in the article?

They do not seem to be semantically well defined?

Thanks!

Carl

https://professorhewitt.blogspot.com/

[Jonathan A Rees]

Carl,

https://doi.org/10.1145/73560.73564

"effects describe the side-effects that an expression may have"

There has been a lot of followon work from Lucassen and Gifford's original idea and I'm pretty sure all of it uses the word "effect" in pretty much the same way.  Basically effects are to an expression's potential side effects as types are to its potential values. Because of Lucassen and Gifford it usually has this technical meaning in the programming languages literature.

I can imagine using the word "effect" to describe actual side effects (dynamically) of a particular execution instead of potential side effects (statically) of an expression, just as "type" is sometimes used to talk about actual values in hand instead of potential values of an expression, but I don't think anyone does that.

- Different 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/CA%2BymXc1ZRigEchHpoOOkQX42BMuqF7-_fS3MGPUEjG%2BX0aX9CQ%40mail.gmail.com.

[Carl Hewitt]

Thanks Jonathan!

Is the article publicly available someplace?

Cheers,

Carl

https://professorhewitt.blogspot.com/

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/a03a07d1-0494-0cc5-1554-2a4d56efa669%40mumble.net.

[Jonathan A Rees]

Oh sorry I thought the PDF link there worked.

Got this link via google scholar:

https://dl.acm.org/doi/pdf/10.1145/73560.73564?casa_token=Wk3GbQX9_mwAAAAA:LBX0lbzTKFc-DGm2nKTQvGOjdInGBEdo5TDEmQwftSUIMAZ78wuqL2foeuXZQPtW-_aVfVyKLfw

Got this link via web search:

http://groups.csail.mit.edu/pag/OLD/parg/lucassen88effects.pdf

There are lots of similar articles which turn up pretty easily in searches. I use 'lucassen gifford effect system' or similar search terms.

Best,
Jonathan

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

[Carl Hewitt]

So an effect is a local state change in an Actor?

Not that an effect may be desired and may not be a "

Thanks!

Carl

https://professorhewitt.blogspot.com/

On Sat, Jan 9, 2021 at 6:53 AM Jonathan A Rees <j...@mumble.net> wrote:

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/a03a07d1-0494-0cc5-1554-2a4d56efa669%40mumble.net.

[Carl Hewitt]

What are additional articles on effects?

Thanks!

Carl

https://professorhewitt.blogspot.com/

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/991f2aec-6a65-3d70-737d-e6cb8ac21b8d%40mumble.net.

[Jonathan A Rees]

I doubt I have any particular inside information that would make my web research better than yours - just try the searches and see what you fancy

https://scholar.google.com/scholar?hl=en&as_sdt=0%2C22&q=lucassen+gifford+effect+system&btnG=
https://duckduckgo.com/?q=lucassen+gifford+effect+system&t=ffab&ia=web

If you're familiar with monads the papers in those searches that make the link with monads should be of interest - but I haven't read them

Jonathan

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

[Carl Hewitt]

PS.  Message truncated :-(

Should have said: Note that an effect may be desired and may not be a "side effect".

[Jonathan A Rees]

On 1/9/21 12:13 PM, Carl Hewitt wrote:

So an effect is a local state change in an Actor?

Among other things. Any non-applicative expression, i.e. any that has some important meaning other than its value as a deterministic function of its execution context, would have a nontrivial 'effect'. Nondeterministic choice would be another kind of 'effect' because amb(1,2) or whatever is not applicative. We don't usually say nondeterministic choice is a kind of side effect, so the definition I quoted is incomplete. A Lisp/Java/etc (throw ...) expression would also be said to have an effect.

An expression creating a new actor would also have an 'effect', if that actor started running at the point of creation. Since I'm not fluent in any actor language I can't say where the list ends. Just use the criterion of 'purity' or applicativity. An expression that might do something impure has an effect.

Jonathan

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

[Carl Hewitt]

Thanks for your explanation, Jonathan! 

  Actors live in a world of indeterminacy, where indeterminacy is different from nondeterminacy, such as, Nondeterministic Turing Machines.  See explanation here:

      Physical Indeterminacy in Digital Computation
                https://papers.ssrn.com/abstract=3459566  

Consequently, the following would not involve change in the behavior of an Actor:

• Creation of a new Actor
• Evaluation of (0 finishesFirst 1) which returns either 0 or 1 indeterminately depending on arbitration

Regards,

Carl

https://professorhewitt.blogspot.com/

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/75082274-9e05-6989-03b6-f9980a0c1d8a%40mumble.net.

[Carl Hewitt]

PS.  Just because an Actor is indeterminate, 

doesn't necessarily mean than the Actor has 

changed its behavior because its unchanging 

behavior may support indeterminacy.

For example there is no behavior change in Eval.[⦅0 finishesFirst 1⦆] with 

the expression ⦅0 finishesFirst 1⦆ expression even though the result is indeterminate.

[William ML Leslie]

On Sun, 10 Jan 2021 at 05:09, Jonathan A Rees <j...@mumble.net> wrote:
>
>
> On 1/9/21 12:13 PM, Carl Hewitt wrote:
> >
> > So an effect is a local state change in an Actor?
>
> Among other things. Any non-applicative expression, i.e. any that has some important meaning other than its value as a deterministic function of its execution context, would have a nontrivial 'effect'. Nondeterministic choice would be another kind of 'effect' because amb(1,2) or whatever is not applicative. We don't usually say nondeterministic choice is a kind of side effect, so the definition I quoted is incomplete. A Lisp/Java/etc (throw ...) expression would also be said to have an effect.
>
> An expression creating a new actor would also have an 'effect', if that actor started running at the point of creation. Since I'm not fluent in any actor language I can't say where the list ends. Just use the criterion of 'purity' or applicativity. An expression that might do something impure has an effect.

>

It tends to be up to the implementer of the effect system what constitutes an effect and what is not tracked.  A system of effect types /may/ track heap allocations (as in Tofte and Birkedal's "A Region Inference Algorithm" - ACM ToPLaS 1998) for example, or it may only track state or external effects.  Java is a good example because it has both checked exceptions (which are an effect) and unchecked exceptions (which are not checked by the effect typing system).

To answer Carl's question, "what is an effect", maybe you want a definition.

An effect is a type which, if the type of the expression does not contain that type, the expression cannot express the action described by the type.

For example, if the effect type of a function does not express that it can assign a value to a box of type Box(Int), then an expression `box := 7` where box has type Box(Int) inside the function will not typecheck.  Importantly, it may not be able to call a function to perform this action on its behalf, either.  In this way, an effect type system can be used to enforce supermodular properties about purity, relative purity, nonlocal exits, stack/heap size, nondeterministic choice, among many other things; but exactly what effects it is desirable to check vary according to need.

Carl: I tend to think of effects as actors; maybe like your type actors, as far as I understand type actors at this point.  In order for an actor to assign a value to a box in the example above, we need to provide it with the effect (or, type actor) required to perform the action.  The benefit of effects being part of a type system is that you cannot introduce a function into the system unless it appropriately demands the effects that it requires access to.

My favourite paper on this subject (which is what lead me into a decade-long journey into the weeds of effect types) is Talpin and Jouvelot's 1992 paper "The Type and Effect Discipline", in which they extend Hindley-Milner type inference to an imperative language by using effect types to propagate invariants about the type held within imperative boxes.  It's a really fine worked example of how to use an effect system to compute something useful.

Effect types feel very "transitive" in the sense that, usually, a function cannot call another function unless it has a superset of that function's effects; but there are usually other ways to introduce effects or to act parametrically over them (both papers I linked include examples of each).  So, for example, a Java method that does not declare a certain checked exception in its signature can still call a function that has it, but it must catch and handle the exception.  Similarly, many typed functional languages with effects, such as Idris, do not have separate `map` and `mapM` functions, but rather the caller must provide the effects that the passed function will require.

--
William Leslie

Q: What is your boss's password?
A: "Authentication", clearly

Notice:
Likely much of this email is, by the nature of copyright, covered under copyright law.  You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in.  Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement.

[William ML Leslie]

On Sun, 10 Jan 2021 at 09:00, Carl Hewitt <carl.e...@gmail.com> wrote:

• Creation of a new Actor
• Evaluation of (0 finishesFirst 1) which returns either 0 or 1 indeterminately depending on arbitration

For completeness, the reason that some systems consider these effects include:

* Creation of a new actor may need to be considered with other rules to determine if an actor possibly shares state between its clients.  For example, it may be desirable to show that the actor that maintains details about user processes does not share those details with anyone but the parent process and the `ps` program.

* heap and stack allocation invariants need to be maintained.  For example, many systems do not permit heap allocation when handling certain messages, such as unix signals.  Other systems may want to be proven to complete without triggering a page fault.

* Computations which are known to produce a deterministic value are valuable as they will behave the same way under test as they will in real use.  It is not always possible, but as far as possible, we would like our computations to be deterministic to make debugging easier.  Requiring an effect in order to express computations whose value and effect depend on scheduling decisions makes it easier to discover which code may produce variation.

[Jonathan Aldrich]

Sorry for the late reply!  Had some reviewing deadlines the last couple of days.

Yes, my work on effects uses the definition that Jonathan Rees pointed to, which was introduced in Lucassen and Gifford.

Cheers,

Jonathan

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/991f2aec-6a65-3d70-737d-e6cb8ac21b8d%40mumble.net.

[Jonathan Aldrich]

The answer may be clear from other discussions, but our article is not specific to Actors.  We assume that there is some set of effects you care about, and you define what those are.  They could in principle be Actor effects, except for the caveats about concurrency already discussed.  Then our article helps you track and reason about those effects statically through a type and effect system (like the one by Lucassen and Gifford, but with extensions for capability-based reasoning about effects in our case).

Cheers,

Jonathan

[Terry Hayes]

Carl,

Let's imagine an actor that returns the value (0 finishesFirst 1) to its "customer".  This is essentially a random choice between 0 and 1.  A recent approach to this considers this to be an "effect" because the "invocation" of the "function" does not return a constant value.  That is, repeated invocations may result in different values.  In Haskell this would have to be wrapped in an "effectful" type, like a Monad.

I disagree that there is no behavior change in this actor system.  While there may be no change in the primary actor (that provides 0 or 1), there are numerous behavioral changes involved.  There are at least 3 actors created to support the "finishesFIrst" operation.  1)  An actor to arbitrate the "first" response and send it to the "customer".  2) and 3) actors to receive the results from each sub computation and forward the result to the arbiter.  At a minimum, there is state created to remember the "customer" for this request.

I believe there is a strong tie between "effects" and changes of behavior of actors in the system.

You may implement the "finishesFirst" as a primitive to hide the complexity of this, but there still are underlying changes and creation of new behaviors.

Terry

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

[Jonathan A Rees]

Carl,

I was trying to diagnose the disconnect here and I think I see what happened. In the introduction to Lucassen and Gifford 1988, 'effects' are equated with 'side effects' (in the sense of state changes per usual computer-sciency usage), and early messages in this thread (including mine) reinforced that idea. But as this line of research evolved, it was seen that 'effect systems' could be applied to things other than 'side effects' - basically any kind of 'impure' operation: catch/throw, exceptions, list comprehension, *ndeterminism, backtracking etc. etc. - anything you'd want a monad for in Haskell.

Even in Lucassen and Gifford 1988 section 3, simply _reading_ state is an 'effect', contradicting the introduction.

An effect system is an analysis tool for understanding and auditing what a program does, focused on impure language features. William Leslie pointed out that the set of phenomena covered by that system depends on the system. So the question "what is an effect" is not meaningful out of context; it depends on the particular system.

(0 finishesFirst 1) is impure because it is not a mathematical function of 0 and 1; its value depends also on who won the race. If you wanted to you could create an effect system for a typed actor language that treats *ndeterminism, or an operation that causes a newly created actor to start running, or any other 'impure' operation, as an effect, but that would be a design choice.

Jonathan

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

[Matt Rice]

On Sun, Jan 10, 2021 at 2:38 PM Jonathan A Rees <j...@mumble.net> wrote:

Carl,

I was trying to diagnose the disconnect here and I think I see what happened. In the introduction to Lucassen and Gifford 1988, 'effects' are equated with 'side effects' (in the sense of state changes per usual computer-sciency usage), and early messages in this thread (including mine) reinforced that idea. But as this line of research evolved, it was seen that 'effect systems' could be applied to things other than 'side effects' - basically any kind of 'impure' operation: catch/throw, exceptions, list comprehension, *ndeterminism, backtracking etc. etc. - anything you'd want a monad for in Haskell.

There are also many effect systems where purity, and/or totality are considered effects, in a sense that purity, and totality both describe an aspect of function behavior.

below is a link to the total effect in a particular language koka-lang.

https://koka-lang.github.io/koka/doc/std_core_types-source.html#type_space__lt__gt_

 

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/9b70bcc8-8bc4-1ae4-d180-f20b89963286%40mumble.net.

[Carl Hewitt]

Thanks Jonathan,

Speaking of tracking and reasoning about effects, I have a challenge for you:

Track and reason about effects in the example below, which is excerpted from the following article:

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

 

A controller could have the following interface:

Controller  interface

      open→Void   // when received a message to open door, return Void after it is open

      close→Void  // when received a message to close door, return Void after it is closed

       move→Void   // when received a message to move train return Void after it is moving

      stop→Void|  // when received a message to stop train, return Void after it is stopped  

 

A very simple controller manager could have the following implementation:

ControllerManager:[ ]→Interface controller → Controller,   

                                                             upgrade[ControllerManagerConstructor] → Void|

   ≡ [ ]  ↦↦   // constructor has no arguments

moving := False         // train is initially not moving

isOpen  := False|     // door is initially closed

 

   controller ↦ controller       // get controller facet of this implementation

   upgrade[aNewVersionConstructor] ↦

              Become aNewVersionConstructor.[moving is moving, isOpen is isOpen]|

                                                             // upgrade to a new version which is provided current local state 

   

    Facet controller implements Controller 

open ↦  moving cases      // Received message to open door, so

           False then isOpen := True;   // if not  moving, then set isOpen  to True and then

                               Hole door.open;  // send door an open request in  hole of the region and

                                                                               // after door reports that it is open,

                               moving cases  True then  Throw TrainMoving[] // if moving, then throw exception

 

close ↦ Hole door.close;   // Received message to close door, so send door a close request

                                                          //  in a hole of the region and after door reports that it is closed,

              isOpen := False         // set isOpen to False      

 

move ↦  isOpen cases  False then  // Received a message to move train so if door is not open, then

                                  moving := True;         // set moving to True and then

                                  Hole engine.move; // send engine a move request in a hole of the region and

                                                                                            //  after engine reports that it is moving,

                                                isOpen cases True then Throw TrainMovingWhileDoorOpen[]

                                          True then Throw DoorOpen[]     // if door is open, then throw exception

  

  stop ↦ Hole engine.stop;  // received a message to stop train, so send engine a stop request in

                                                           // a hole of the region and after engine reports that it is stopped,          

                           moving := False         // set moving to False         

Regards,

Carl

https://professorhewitt.blogspot.com/

[Carl Hewitt]

Thanks Terry for your perceptive comment!

There could be a primitive Actor called 0Or1, which when 

sent the message get indeterminately returns 0 or 1 

making use of an arbiter circuit.

See discussion here:

      Physical Indeterminacy in Digital Computation
        https://papers.ssrn.com/abstract=3459566   

Consequently, 0Or1 never changes its own indeterminate behavior

and never creates any customer Actors.

Thus there are no underlying changes in the implementation of 0Or1.

What exactly is the strong tie between "effects" and changes of behavior of Actors? 

 

Regards,

Carl

https://professorhewitt.blogspot.com/

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAGLSb_Xz%3DWvy4XJD0inCFVX-xh%2BXTJEbPs1Ydm41R4Ec13gKpQ%40mail.gmail.com.

[Carl Hewitt]

Thanks for the perceptive analysis Jonathan!

Unfortunately, "impure" could be prejudicial terminology for 

pervasive indeterminacy in the implementation of Intelligent Systems.

See the following:

          Project Liftoff: Universal Intelligent Systems (UIS) by 2030
                 https://papers.ssrn.com/abstract=3428114  

Do we want to taint such massive concurrent systems with the label "impure"?

Regards,

Carl

https://professorhewitt.blogspot.com/

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/9b70bcc8-8bc4-1ae4-d180-f20b89963286%40mumble.net.

[Jonathan A Rees]

It's not up to me, I didn't pick the word.  The literature has used the word "pure" (and its negation "impure") this way for a very long time (I found a 1973 use very easily) and it's nonprejudicial among the people who use it this way. It's a very natural concept - it explains the difference between expressions in a programming language and expressions in mathematics - and offhand I don't know of a better word for it.

The water we drink is almost always impure, but that can be a good thing, not a bad thing (try drinking distilled water sometime).

If you're talking to someone outside this community who will go batty on hearing the word, sure, pick a different word.

Different Jonathan

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

[Carl Hewitt]

Actually, mathematics has been dealing with change (with Galileo being an early proponent) for a long time with no "impurity" ;-)

More recently, The Actor model (which is all about change) has been axiomatized in mathematics up to a unique isomorphism.

The Church/Turing Model of Computation (based on the solipsistic deterministic procedure) was obsolete before it was formalized because 

there were teams of programmers (invariably all women) performing large-scale computations.

Sometimes a field acknowledges its mistakes and resolves to do better.

Now the onus is on those who perpetuate the "impurity" terminology.

In particular, there are terminology issues in communicating with 

those outside a field and educating newcomers.

Regards,

Carl

https://professorhewitt.blogspot.com/

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/8e3c5e4d-30f7-d3a5-26fd-8a5e50b0aa86%40mumble.net.

[Jonathan Aldrich]

As others have said, effects are a modeling construct, and type-and-effect systems are a way of reasoning about those models.  I would say that when an Actor changes its behavior, that's definitely within the scope of things that people model with effects.  So it would be natural to use effects for that.  But ultimately it is the effect language designer's choice whether to call it an effect or not.  Once you make that modeling decision, a type-and-effect system will help you reason consistently about the effects you did choose to model.

Best,

Jonathan

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

[Carl Hewitt]

Thanks Jonathan!

Given your points, I am wondering whether the term "effects" has lost its utility because it is ill-defined and potentially subject to whim.

Regards,

Carl

https://professorhewitt.blogspot.com/

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

[Mike Stay]

"Effect" has a perfectly good meaning: any deviation from behaving
like a function.

> To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CA%2BymXc0X%2BZ2tzxF5ze5wXQDBfFKT%3DMMyzi7-CgwOS%3DQiU%3D3FpA%40mail.gmail.com.



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