Re: [friam] Formal modeling of systems based on E/CapTP/(Water)Ken/Cap'n Proto ideas

On 6 July 2015 at 21:59, Mark Miller <[email protected]> wrote:
> IANAF -- I am not a formalist. But my co-authors (Sophia and James, cc'ed)
> are. Today at PLAS (Programming Languages and Security) Sophia presented
>
> Swapsies on the Internet: First Steps towards Reasoning about Risk and Trust
> in an Open World
>
> <http://research.google.com/pubs/pub43808.html>

I started reading it a while back and I have a copy somewhere with
notes on that I can't find right now. sorry.

One thing that struck me is the example doesn't seem to me to address
the problem in the best way, which kinda spoiled the fun for me.

In particular, you make new Purses from existing Purses. This (it
seems to me, though perhaps I am missing something) creates an
asymmetry that can be exploited by bad actors. If, instead, Purses
came from Mints, then the two players would be forced to agree on a
Mint which one of them would then have to subvert.

>
>
>
> Having observed and participated in many attempts to formalize aspects of
> capability reasoning, I think what Sophia and James have done here is a real
> breakthrough.
>
>
> Sophia and James,
> Every Friday morning (10-12 pacific time) we have an informal meeting of
> various ocap interested people, which we call the "friam" meetings. Several
> people attend remotely by hangout. We should pick a friam meeting for you
> both to join by hangout for us to discuss this work.
>
> Tony,
> This has nothing whatsoever to do with temporal logic. Your message just
> provoked me to announce this as a response ;)
>
> Friamers,
> I know it isn't usually done, but can I ask us all to read-or-at-least-skim
> the paper prior to that hangout? IMO, this is really important work, Enjoy!
>
>
>
>
> On Mon, Jul 6, 2015 at 8:04 PM, Tony Arcieri <[email protected]> wrote:
>>
>> One thing I've observed about distributed object capability systems is
>> that things like handling errors and ensuring messages don't get dropped is
>> generally described in terms of "guidelines". I'm thinking things like COVR
>> here.
>>
>> This gives a developer a lot of expressiveness and flexibility, but not a
>> lot of assurances that making a single misstep anywhere will break
>> everything.
>>
>> Tools like temporal logic (with mechanically checked proofs) and (formally
>> modeled) replicated state machines seem like they could help here, and
>> ensure that all potential failure modes are handled in some way (even if
>> it's surfacing an error). I'm thinking of something like TLA+ here, at least
>> to model check an approach like COVR.
>>
>> Have there been any attempts at applying temporal logic to proving the
>> correctness of object capability systems?
>>
>> --
>> Tony Arcieri
>
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "friam" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to friam+unsubscribe-/JYPxA39Uh5TLH3MbocFF+G/[email protected]
> To post to this group, send email to friam-/JYPxA39Uh5TLH3MbocFF+G/[email protected]
> Visit this group at http://groups.google.com/group/friam.
> For more options, visit https://groups.google.com/d/optout.