Use case: ERTP / Chainmail

[dckc]

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

rchain-community/js2rho#4

[dckc]

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]

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

currently: sophiaIC/HolisticSpecifications@dbdf492

[dckc]

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

• Proving Full-System Security Properties under Multiple Attacker Models on Capability Machines.
  T. Van Strydonck, A.L. Georges, A. Gueneau, A. Trieu, A. Timany, F. Piessens, L. Birkedal, and D. Devriese.
  In CSF 2022: Computer Security Foundations

cc @Jake-Gillberg

[dckc]

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]

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 Mart��n 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]

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]

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:

• Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov, Dominique Devriese, Verified Symbolic Execution with Kripke Specification Monads (and No Meta-Programming), Proceedings of the ACM on Programming Languages, volume 6, issue ICFP, pages 194-224, Association for Computing Machinery (ACM), August 31, 2022 download0 3799487bibtex 3799487lirias 3799487doi
• Thomas Van Strydonck, Aïna Linn Georges, Armaël Gueneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese, Proving full-system security properties under multiple attacker models on capability machines, IEEE Computer Security Foundations Symposium (CSF), 2022 IEEE 35th Computer Security Foundations Symposium (CSF), pages 80-95, Haifa, Israel, August 7-10, 2022 download0 3945169bibtex 3945169lirias 3945169doi

Oh... and this one too...

• Stylianos Tsampas, Christian Williams, Andreas Nuyts, Dominique Devriese, Frank Piessens, Abstract Congruence Criteria for Weak Bisimilarity, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), volume abs/2010.07899, pages 88:1-88:23, Talinn, Estonia, August 23-27, 2021 download0 3284490bibtex 3284490lirias 3284490doi

Yikes... a little over my head.

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

• RCast 102 - A Logical View on Geometry - Sept 2 2020 - RChain Blog
• RCAST 102 - A Logical View on Geometry - SEPT 2 2020 - YouTube

[dckc]

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]

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 ⁶

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.

---