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

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>



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
>

_______________________________________________
cap-talk mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/cap-talk