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

On Wed, Jul 8, 2015 at 4:25 PM, Ken Kahn <[email protected]> wrote:

> Interesting paper. From the introduction (e.g. " you’d probably be careful
> to take only stickers you’re definitively willing to risk losing") I
> expected that probabilities would play a role here. Why not compare the
> product of the estimated probability of untrustworthiness and the amount
> loss with the difference between the value of the good and price of the
> good? This "economic" approach would apply at all levels where trust and
> risk apply not just the top-level transactions. While it is hard to
> estimate probabilities I don't really see a good alternative. Such an
> approach probably could build upon the formalism of the paper.
>

We did discuss it, but felt we needed to get the structure of logical
implications right first. On the logical structure, there is a lot left to
do, so I doubt we would get to that anytime soon. But I encourage you or
anyone interested to explore this line of research. It seems very promising.

Regarding "it is hard to estimate probabilities", I would not even try.
Rather, I would try to modify the reasoning so that it produces probability
formulas whose inputs are variables representing the unknown probabilities
that the participants assigned to their starting trust assumptions. None of
this need involve a concrete quantity.

However, I expect this would still be hard. I hope someone tries!





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



-- 
    Cheers,
    --MarkM

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