search

rchain-community / behavr

Toward Behavioral Type checking for Rholang
Apache License 2.0
6 stars 1 forks source link

Use case: ERTP / Chainmail #13

Open dckc opened 4 years ago

dckc commented 4 years ago

Holistic Specifications for Robust Programs Sophia Drossopoulou Feb 2020 - how much overlap with behavioral types?

https://github.com/Agoric/agoric-sdk/blob/master/packages/ERTP/src/types.js

https://github.com/rchain-community/js2rho/issues/4

dckc commented 3 years ago

Here's hoping to discuss how this Feb presentation by Sophia Drossopoulou relates to behaivoral types, @leithaus @steverosstalbot

Holistic_Specs_IC_Feb_2021.pdf

dckc commented 3 years ago

TIL: @JulianMackay is the main contributor on https://github.com/sophiaIC/HolisticSpecifications thesed days.

currently: https://github.com/sophiaIC/HolisticSpecifications/commit/dbdf4921b01e93504a59b5850288b8a6e0ce5bfd

dckc commented 3 years ago

I spent some time studying Iris Project over the weekend, prompted by coming across another paper that uses it. I'm starting to get my head around separation logic... at least the separating conjunction part. (I don't grok the magic wand operator fully yet).

It has modalities but not reflection, as far as I can see.

Capability-based systems support the enforcement of security properties in the presence of arbitrary untrusted code in the system through what are typically called object capability patterns, like the membrane or caretaker patterns [31]. It is only relatively recently that sufficiently powerful formal reasoning approaches have been developed that can prove such properties. Devriese et al. [7] proposed a reasoning approach based on logical relations, (what we now call) universal contracts and the concept of effect parametricity. Swasey et al. [8] developed the first program logic, OCPL, that can compositionally specify and verify the properties enforced by object capability patterns. Building on these ideas, program logics have been developed to reason about software in low-level capability-based instruction set architectures [10], [11]. These logics, as ours, are built in Iris [18], a separation logic framework for building program logics. Iris integrates, unifies, and simplifies a wide variety of mechanisms for reasoning about programs that can be higher order, concurrent, or use mutable state

cc @jake-gillberg

dckc commented 2 years ago

Where is that stuff on open-world reasoning and barbs and such? [1102.5584] A Spatial-Epistemic Logic for Reasoning about Security Protocols talks about the general technique of putting things in parallel, but i don't see barbs:

4.1 Modeling Attackers To analyze a security protocol one usually needs to consider how it behaves in any possible environment. While our logic focuses on the analysis of closed systems, it is possible to verify properties of a system in an arbitrary environment, by internalizing an arbitrary attacker in the system. The general idea is that, for any process P, we may determine a process Q (making essential use of the attacker prefix construct) such that P|Q reaches some state whenever P reaches an equivalent state when placed in an arbitrary environment. While the explicit specification of an attacker for a given protocol may not be easy, our approach to represent the attacking environment is quite different and general, and may indeed be used to find attacks (see example in Section 4.2).

The next bit looks like something I should look into:

We can generically model a Dolev-Yao [12] attacker in our framework by considering the number of message exchanges and the communication channels used in a protocol

dckc commented 2 years ago

Ah yes... spi calculus and the new operator

SPi Calculus Calculus: Outline The Spi Calculus

4.2 Testing Equivalence In order to de ne equivalence, we rst de ne a predicate that describes the channels on which a process can communicate. We let a barb, , be an input or output channel, that is, either a name m (representing input) or a co-name m (representing output). For a closed process P , we de ne the predicate P exhibits barb , written P # -- A Calculus for Cryptographic Protocols: The Spi Calculus Martn Abadi Digital Equipment Corporation Systems Research Center Andrew D. Gordon University of Cambridge Computer Laboratory 1999

[1208.2749] Hide and New in the Pi-Calculus

On Bisimulations for the Spi Calculus Johannes Borgstr¨om and Uwe Nestmann

dckc commented 1 year ago

Formalize Zoe Offer Safety? in TLA+? Coq? Idris? Behavioral types?

Recently some of us asked MarkM what's the motivation for E(brand).isMyIssuer(i).

Zoe does not “trust” the issuers presented by Zoe’s customers. More precisely, Zoe must

  • maintain its own integrity even when the Issuers misbehave
  • provide each customer the usual offer-safety guarantees, etc, if the issuers presented by THAT customer behave correctly.

Note that Zoe is not assumed in general to ever know whether an issuer is correct or not. The second guarantees are conditional, but Zoe itself doesn’t know whether the condition “if the issuers presented by THAT customer behave correctly” holds in any one case.

Given correct IssuerA, IssuerA.getBrand() will (by definition of Issuer correctness) produce a correct BrandA that is unique to IssuerA.

Maliciously constructed IssuerB.getBrand() could still return BrandA. This is incorrect behavior by IssuerB. When Zoe sees BrandA, IssuerA, and IssuerB, how does Zoe know what issuer corresponds to BrandA? If BrandA is incorrect, or if both issuers are incorrect, the answer doesn’t matter. But if BrandA is correct and one of those issuers correctly pairs with it, the other misbehaving issuer should not be able to mislead Zoe to believing that BrandA is the brand of IssuerB.

So, to provide the guarantees of the two bullets above, Zoe must check that a brand and issuer agree on each other at least once. If they are both not correct, then this agreement might be fleeting, but it doesn’t matter. If at least one is correct, then they wont agree on the other unless it is correct too. So mutual agreement observed once eliminates the possibility of only one being correct. If they are both correct, then if they ever agree on each other they always agree on each other.

The registration of an issuer/brand pair in zoe asynchronously waits until zoe sees this mutual agreement.

Then we got to talking about exactly what guarantees Zoe provides and how to formalize them, and he reminded me:

See Reasoning about Risk and Trust in an Open World for the essence of this “conditional rely” and “mutual agreement” logic. That paper came from reasoning about the offer safety of the Escrow Exchange Agent of Distributed Electronic Rights in JavaScript , which is still kinda the essence of Zoe.

Holistic specification, behavioral types

In the "...Open World" paper, section 2.3 Valid Purse: Specifying Purse starts:

Using obeys, MayAccess, and MayAffect, ...

MayAccess looks like the rholang "receives from" type and MayAffect looks like the "sends to" type.

The logic in the "..Open World" paper is more recently called Holistic Specifications. I think there's a big overlap with process calculi, esp. rholang, and I'd like to get folks working on each to tell me if they think so too.

Background: toward formal spec for Zoe Offer Safety

It's been a goal at least as far back as 2019

I think it would be fun to formally verify the offer safety property. Mark Miller and I chatted about this with Eric McCarthy, who works on the ACL2 Ethereum project. I have some history with ACL2, and in some sense the untyped style of ACL2 goes well with JavaScript, but I wonder if that's a false economy. I'm more facile with ML style propositions-as-types systems (idris, ocaml) lately. -- MadMode: Toward secure distributed computing with Agoric at SFBW '19

In Aug 2021, I learned enough TLA+ (crash course notes) to write Purse.tla. But it was only the stateless part of the story, so we switched from TLA+ to a property-testing library (fast-check). In an issue about how to defined "well behaved" issuer, we talked about promptness and "eventually" and such.

So I'm interested to try TLA+ to nail down what MarkM said about isMyIssuer.

dckc commented 1 year ago

Tom Van Cutsem presented at Agoric this week. He's in the DistriNet group.

Projects include LowCapsFormally... where do I find out more about that?! Ah... led by Dominique Devriese, whose publications include one of my favorites, Reasoning about object capabilities with logical relations and effect parametricity.

Any new stuff from him? Ah... yes... these look particularly interesting:

Oh... and this one too...

Yikes... a little over my head.

Christian Williams... sounds familiar... yes:

dckc commented 1 year ago

need to restart my machine to switch on VTx in the bios to try out JaVerT

saving a tab dump from Apr / May:

coq distributed at DuckDuckGo coq · GitHub Topics uwplse/verdi: A framework for formally verifying distributed systems implementations in Coq A model for reasoning about JavaScript promises A Study on Formal Verification for JavaScript Software JaVerT: JavaScript Verification Toolchain | the morning paper Programming and Proving with Distributed Protocols will62794/tla-web: TLA+ Web Explorer Prototype Modeling Redux with TLA+ • Hillel Wayne tlaplus/Examples: A collection of TLA+ specifications of varying complexities PlusCal Tutorial - Contents TLA+ Proof System pluscal syntax at DuckDuckGo pluscal.pdf Programming and Proving with Distributed Protocols.pdf

dckc commented 7 months ago

How to be sure powerful capabilities don't leak?

from Meredith and Radestock - 2005 - Namespace Logic A Logic for a Reflective Higher-Order Calculus

5.1 Examples

Controlling access to namespaces Suppose that $\ulcorner\phi\urcorner$ describes some namespace, i.e. some collection of names. We can insist that a process restrict its next input to names in that namespace by insisting that it witness the formula

$\langle\ulcorner\phi\urcorner ? b\rangle$ true \& $\neg\langle\ulcorner\neg \phi\urcorner ? b\rangle$ true

which simply says the the process is currently able to take input from a name in the namespace pφq and is not capable of input on any name not in that namespace. In a similar manner, we can limit a server to serving only inputs in $\ulcorner\phi\urcorner$ throughout the lifetime of its behavior 6

rec $X .\langle\ulcorner\phi\urcorner ? b\rangle X$ \& $\neg\langle\ulcorner\neg \phi\urcorner ? b\rangle$ true

This formula is reminiscent of the functionality of a firewall, except that it is a static check. A process witnessing this formula will behave as though it were behind a firewall admitting only access to the ports in $\ulcorner\phi\urcorner$ without the need for the additional overhead of the watchdog machinery.