[bitcoin-dev] TLA+ specification for Succint Atomic Swap

[bitcoin-dev] TLA+ specification for Succint Atomic Swap

[Dmitry Petukhov]

The Succint Atomic Swap contract presented by Ruben Somsen recently has
drawn much interest.

I personally am interested in the smart contracts realizeable in the
UTXO model, and also interested in applying formal methods to the
design and implementation of such contracts.

I think that having formal specifications for the contracts and to be
able to machine-check the properties of these specifications is very
valuable, as it can uncover the corner cases that might be difficult to
uncover otherwise.

The SAS contract is complex enough that it may benefit from formal
specification and machine checking.

I created a specification in TLA+ [1] specification language based on
the explanation and the diagram given by Ruben.

The checking of the model encoded in the specification can successfully
detect the violation of 'no mutual secret knowledge' invariant when one
of the participant can bypass mempool and give the transaction directly
to the miner (this problem was pointed out by ZmnSCPxj in the original
SAS thread [2])

There's one transition that was unclear how to model, though: I did not
understand what the destination of Alice&Bob cooperative spend of
refund_tx#1 will be, so this transition is not modelled.

I believe there can be more invariants and temporal properties of the
model that can be checked. At the moment the temporal properties
checking does not work, as I didn't master TLA+ enough yet. The safety
invariants checking should work fine, though, but more work needed to
devise and add the invariants.

In the future, it would be great to have an established framework for
modelling of the behavior in Bitcoin-like blockchain networks.
In particular, having a model of mempool-related behavior would help to
reason about difficult RBF/CPFP issues. The specification I present
models the mempool, but in a simple way, without regards to the fees.

The specification can be found in this github repository:
https://github.com/dgpv/SASwap_TLAplus_spec

There could be mistakes or omissions in the specified model, I hope
that public review can help find these.

It would be great to receive comments, suggestions and corrections,
especially from people experienced in formal methods and TLA+, as this
is only my second finished TLA+ spec and only my third project using
formal methods (I created bitcoin transaction deserialization code in
Ada/SPARK before that [3]). Please use the github issues or off-list
mail to discuss if the matter is not interesting to the general
bitcoin-dev list audience.

[1] https://lamport.azurewebsites.net/tla/tla.html

[2]
https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2020-May/017846.html

[3] https://github.com/dgpv/spark-bitcoin-transaction-example

Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap

[Ruben Somsen]

[-- Attachment #1: Type: text/plain, Size: 5306 bytes --]

Hi Dmitry,

Thanks for creating a specification for testing, I appreciate the interest!

>The checking of the model encoded in the specification can successfully
detect the violation of 'no mutual secret knowledge' invariant when one of
the participant can bypass mempool and give the transaction directly to the
miner (this problem was pointed out by ZmnSCPxj in the original SAS thread
[2])

I'm not sure if I follow. The issue ZmnSCPxj described about bypassing the
mempool was not a violation. It was merely a "nuisance" strategy that
causes Alice to have to abort in three transactions. Also note that I
subsequently pointed out in the thread that this strategy does not work,
because Alice is supposed to abort sooner than that if Bob still has not
locked up any funds.

Or perhaps you're referring to the issue ZmnSCPxj pointed out after that,
where refund transaction #1 and the success transaction could both become
valid at the same time. It would make sense for the test to pick up on
that, but I believe that is ultimately also not an issue (see my last reply
in the thread).

>I did not understand what the destination of Alice&Bob cooperative spend
of refund_tx#1 will be

This transaction can be spent by Alice & Bob right away or by Alice a day
later (in relative time, so the tx has to confirm first). The Alice & Bob
condition is there purely to ensure that Bob can spend the money before
Alice once he receives her key at the end of the protocol.

If it helps, you could model this transaction as two separate transactions
instead:
txA: 1 day absolute timelock to Alice & Bob (reveals secretAlice), which
can then be spent by
txB: +1 day relative timelock to Alice

This should be functionally equivalent. Also note that the protocol should
fully function if refund tx #1 did not exist at all. It merely serves to
save block space in certain refund scenarios.

>it would be great to have an established framework for modelling of the
behavior in Bitcoin-like blockchain networks. In particular, having a model
of mempool-related behavior would help to reason about difficult RBF/CPFP
issues

A laudable goal. Good luck with your efforts.

Cheers,
Ruben

On Wed, May 13, 2020 at 7:07 PM Dmitry Petukhov via bitcoin-dev <
bitcoin-dev@lists.linuxfoundation.org> wrote:

> The Succint Atomic Swap contract presented by Ruben Somsen recently has
> drawn much interest.
>
> I personally am interested in the smart contracts realizeable in the
> UTXO model, and also interested in applying formal methods to the
> design and implementation of such contracts.
>
> I think that having formal specifications for the contracts and to be
> able to machine-check the properties of these specifications is very
> valuable, as it can uncover the corner cases that might be difficult to
> uncover otherwise.
>
> The SAS contract is complex enough that it may benefit from formal
> specification and machine checking.
>
> I created a specification in TLA+ [1] specification language based on
> the explanation and the diagram given by Ruben.
>
> The checking of the model encoded in the specification can successfully
> detect the violation of 'no mutual secret knowledge' invariant when one
> of the participant can bypass mempool and give the transaction directly
> to the miner (this problem was pointed out by ZmnSCPxj in the original
> SAS thread [2])
>
> There's one transition that was unclear how to model, though: I did not
> understand what the destination of Alice&Bob cooperative spend of
> refund_tx#1 will be, so this transition is not modelled.
>
> I believe there can be more invariants and temporal properties of the
> model that can be checked. At the moment the temporal properties
> checking does not work, as I didn't master TLA+ enough yet. The safety
> invariants checking should work fine, though, but more work needed to
> devise and add the invariants.
>
> In the future, it would be great to have an established framework for
> modelling of the behavior in Bitcoin-like blockchain networks.
> In particular, having a model of mempool-related behavior would help to
> reason about difficult RBF/CPFP issues. The specification I present
> models the mempool, but in a simple way, without regards to the fees.
>
> The specification can be found in this github repository:
> https://github.com/dgpv/SASwap_TLAplus_spec
>
> There could be mistakes or omissions in the specified model, I hope
> that public review can help find these.
>
> It would be great to receive comments, suggestions and corrections,
> especially from people experienced in formal methods and TLA+, as this
> is only my second finished TLA+ spec and only my third project using
> formal methods (I created bitcoin transaction deserialization code in
> Ada/SPARK before that [3]). Please use the github issues or off-list
> mail to discuss if the matter is not interesting to the general
> bitcoin-dev list audience.
>
> [1] https://lamport.azurewebsites.net/tla/tla.html
>
> [2]
>
> https://lists.linuxfoundation.org/pipermail/bitcoin-dev/2020-May/017846.html
>
> [3] https://github.com/dgpv/spark-bitcoin-transaction-example
> _______________________________________________
> bitcoin-dev mailing list
> bitcoin-dev@lists.linuxfoundation.org
> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
>

[-- Attachment #2: Type: text/html, Size: 6784 bytes --]

Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap

[Dmitry Petukhov]

В Wed, 13 May 2020 21:03:17 +0200
Ruben Somsen <rsomsen@gmail.com> wrote:

> Or perhaps you're referring to the issue ZmnSCPxj pointed out after
> that, where refund transaction #1 and the success transaction could
> both become valid at the same time. It would make sense for the test
> to pick up on that, but I believe that is ultimately also not an
> issue (see my last reply in the thread).

This one.

The issue as I see it: Bob can not broadcast success_tx and wait until
Alice has broadcasted refund_tx_1. While refund_tx_1 is in the mempool,
Bob gives success_tx to the friendly miner to have a chance to
invalidate success_tx. Bob already learned secretAlice, so he grabs
his LTC back. If the Bob-friendly miner has luck, success_tx is
confirmed while refund_tx_1 is invalidated, and Bob now have both LTC
and BTC, while Alice is out of her BTC.

> >I did not understand what the destination of Alice&Bob cooperative
> >spend  
> of refund_tx#1 will be
> 
> This transaction can be spent by Alice & Bob right away or by Alice a
> day later (in relative time, so the tx has to confirm first). The
> Alice & Bob condition is there purely to ensure that Bob can spend
> the money before Alice once he receives her key at the end of the
> protocol.

Ah, so this is possible because of the step 5 in the diagram: ``Alice
gives Bob her key ("Alice")'' -- As I understand, this is a way to deny
Alice to use refund_tx_1.

Then if Alice gives her _key_ to Bob before Bob has to share secretBob
via success_tx, could Bob just spend the Alice&Bob output of the
very first, "commitment" transaction that locks BTC ? Bob will receive
BTC, and the LTC can be locked forever, but Bob doesn't care, he got
his BTC.

Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap

[Ruben Somsen]

[-- Attachment #1: Type: text/plain, Size: 3366 bytes --]

Hi Dmitry,

>While refund_tx_1 is in the mempool, Bob gives success_tx to the friendly
miner

I see, so you're talking about prior to protocol completion, right after
Alice sends Bob the success_tx. The reason this is not an issue is because
Alice and Bob both had to misbehave in order for this to happen. Bob is
misbehaving here because he should have published the success_tx before
refund_tx_1 became valid, and Alice is misbehaving here because she should
have sent the revoke_tx (which invalidates the success_tx) followed by
refund_tx_2 (revealing her secret only AFTER Bob can no longer claim the
BTC). In other words: yes, the protocol can fail if Alice and Bob together
work towards that goal. A feature, not a bug. This won't happen if either
of them doesn't want it to. I imagine this is difficult to model.

>As I understand, this is a way to deny Alice to use refund_tx_1.

That is correct, and it also denies refund_tx_2 by making the revoke_tx
directly spendable by Bob.

>could Bob just spend the Alice&Bob output of the very first, "commitment"
transaction that locks BTC

Yes, he can. This is what makes it possible to complete the protocol in
merely two transactions.

>Bob will receive BTC, and the LTC can be locked forever, but Bob doesn't
care, he got his BTC.

No, because diagram step 5 comes before step 6 -- Alice won't give her key
until she learns secretBob.

I hope this clarifies it!

Cheers,
Ruben

On Thu, May 14, 2020 at 6:49 AM Dmitry Petukhov <dp@simplexum.com> wrote:

> В Wed, 13 May 2020 21:03:17 +0200
> Ruben Somsen <rsomsen@gmail.com> wrote:
>
> > Or perhaps you're referring to the issue ZmnSCPxj pointed out after
> > that, where refund transaction #1 and the success transaction could
> > both become valid at the same time. It would make sense for the test
> > to pick up on that, but I believe that is ultimately also not an
> > issue (see my last reply in the thread).
>
> This one.
>
> The issue as I see it: Bob can not broadcast success_tx and wait until
> Alice has broadcasted refund_tx_1. While refund_tx_1 is in the mempool,
> Bob gives success_tx to the friendly miner to have a chance to
> invalidate success_tx. Bob already learned secretAlice, so he grabs
> his LTC back. If the Bob-friendly miner has luck, success_tx is
> confirmed while refund_tx_1 is invalidated, and Bob now have both LTC
> and BTC, while Alice is out of her BTC.
>
> > >I did not understand what the destination of Alice&Bob cooperative
> > >spend
> > of refund_tx#1 will be
> >
> > This transaction can be spent by Alice & Bob right away or by Alice a
> > day later (in relative time, so the tx has to confirm first). The
> > Alice & Bob condition is there purely to ensure that Bob can spend
> > the money before Alice once he receives her key at the end of the
> > protocol.
>
> Ah, so this is possible because of the step 5 in the diagram: ``Alice
> gives Bob her key ("Alice")'' -- As I understand, this is a way to deny
> Alice to use refund_tx_1.
>
> Then if Alice gives her _key_ to Bob before Bob has to share secretBob
> via success_tx, could Bob just spend the Alice&Bob output of the
> very first, "commitment" transaction that locks BTC ? Bob will receive
> BTC, and the LTC can be locked forever, but Bob doesn't care, he got
> his BTC.
>

[-- Attachment #2: Type: text/html, Size: 4146 bytes --]

Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap

[Dmitry Petukhov]

В Thu, 14 May 2020 07:31:13 +0200
Ruben Somsen <rsomsen@gmail.com> wrote:

> Hi Dmitry,
> 
> >While refund_tx_1 is in the mempool, Bob gives success_tx to the
> >friendly miner
> 
> I see, so you're talking about prior to protocol completion, right
> after Alice sends Bob the success_tx. The reason this is not an issue
> is because Alice and Bob both had to misbehave in order for this to
> happen. Bob is misbehaving here because he should have published the
> success_tx before refund_tx_1 became valid, and Alice is misbehaving
> here because she should have sent the revoke_tx (which invalidates
> the success_tx) followed by refund_tx_2 (revealing her secret only
> AFTER Bob can no longer claim the BTC). In other words: yes, the
> protocol can fail if Alice and Bob together work towards that goal. A
> feature, not a bug. This won't happen if either of them doesn't want
> it to. I imagine this is difficult to model.

Right. But it should be noted that it is not enough that Bob publishes
success_tx before refund_tx_1 became valid. The success_tx needs to be
confirmed before refund_tx_1 became valid.

Only Bob can spend success_tx so this is unlikely to be the practical
problem, unless the original fee of success_tx is too small and Bob
epically screws up CPFP-ing it.

> >Bob will receive BTC, and the LTC can be locked forever, but Bob
> >doesn't  
> care, he got his BTC.
> 
> No, because diagram step 5 comes before step 6 -- Alice won't give
> her key until she learns secretBob.

I somehow missed it, and steps 5 and 6 in the diagram was not modelled
at all (on the other hand, it made the model simpler and I had
something working relatively quick). I now made the `signers_map` into
variable that can be changed to give Bob the ability to sign for Alice.

With that change, step 6 can be modelled, but this will add a bunch of
new txs to the model (each Alice&Bob spend will have 'Bob unilateral
override' case)

Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap

[Ruben Somsen]

[-- Attachment #1: Type: text/plain, Size: 2428 bytes --]

Hi Dmitry,

>But it should be noted that it is not enough that Bob publishes success_tx
before refund_tx_1 became valid. The success_tx needs to be confirmed
before refund_tx_1 became valid.

Agreed, my write-up would benefit from pointing this out more explicitly.

Cheers,
Ruben

On Thu, May 14, 2020 at 9:05 AM Dmitry Petukhov <dp@simplexum.com> wrote:

> В Thu, 14 May 2020 07:31:13 +0200
> Ruben Somsen <rsomsen@gmail.com> wrote:
>
> > Hi Dmitry,
> >
> > >While refund_tx_1 is in the mempool, Bob gives success_tx to the
> > >friendly miner
> >
> > I see, so you're talking about prior to protocol completion, right
> > after Alice sends Bob the success_tx. The reason this is not an issue
> > is because Alice and Bob both had to misbehave in order for this to
> > happen. Bob is misbehaving here because he should have published the
> > success_tx before refund_tx_1 became valid, and Alice is misbehaving
> > here because she should have sent the revoke_tx (which invalidates
> > the success_tx) followed by refund_tx_2 (revealing her secret only
> > AFTER Bob can no longer claim the BTC). In other words: yes, the
> > protocol can fail if Alice and Bob together work towards that goal. A
> > feature, not a bug. This won't happen if either of them doesn't want
> > it to. I imagine this is difficult to model.
>
> Right. But it should be noted that it is not enough that Bob publishes
> success_tx before refund_tx_1 became valid. The success_tx needs to be
> confirmed before refund_tx_1 became valid.
>
> Only Bob can spend success_tx so this is unlikely to be the practical
> problem, unless the original fee of success_tx is too small and Bob
> epically screws up CPFP-ing it.
>
> > >Bob will receive BTC, and the LTC can be locked forever, but Bob
> > >doesn't
> > care, he got his BTC.
> >
> > No, because diagram step 5 comes before step 6 -- Alice won't give
> > her key until she learns secretBob.
>
> I somehow missed it, and steps 5 and 6 in the diagram was not modelled
> at all (on the other hand, it made the model simpler and I had
> something working relatively quick). I now made the `signers_map` into
> variable that can be changed to give Bob the ability to sign for Alice.
>
> With that change, step 6 can be modelled, but this will add a bunch of
> new txs to the model (each Alice&Bob spend will have 'Bob unilateral
> override' case)
>

[-- Attachment #2: Type: text/html, Size: 3046 bytes --]

Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap

[Dmitry Petukhov]

I've finished specifying the full Succint Atomic Swap contract in TLA+.

I believe the specification [1] now covers all relevant behaviors of
the participants. It even has an option to enable 'non-rational'
behavior, so that it can be shown that the transactions that are there
to punish bad behavior can actually be used. If you examine the spec
and find that I failed to specify some relevant behavior, please tell.

The specification can be used to exhaustively check safety properties
of the model (such as no participant can take both coins, unless in
explicitly specified circumstances), and temporal properties (such as
contract always end up in an explicitly specified 'finished' state).

The specification can also be used to *show* (but not automatically
check at the moment) the hyperproperties of the model, such as what
transactions can ever be confirmed in at least one the execution path,
max/min/avg values for various stats, etc. The information on these
hyperproperties can be printed out during model checking, and can be
examined manually or with help of additional scripts (if one willing to
write some).

The model has some limitations, like only having one miner, and not
modelling fees and mempool priorities. More than one miner needed to
introduce reorgs in the model, but I believe that reorgs are relevant
only if we cannot say that "one block in the model means 6 bitcoin
blocks" (or whatever reorg safety limit is acceptable). I also believe
that the fees and mempool priorities are a lower-level concern, because
the task to confirm the transaction in time is the same for different
stages of the contract and for different transactions, and therefore
this can be modelled separately.

The goal of creating this specification was to evaluate the suitability
of TLA+ for modelling of the smart contracts in UTXO-based
blockchain systems. I believe that the presented spec shows that it is
indeed feasible to do such modelling and TLA+ is a suitable tool for
specifying and for checking such specifications (Although having ability
to automatically check hyperproperties using TLA+ expressions would be
nice).

I hope that this spec can be used as a basis for specs for other
contracts, and that using TLA+ can make designing safe contracts for
UTXO-based systems easier. I also hope that this will help to increase
interest in using formal methods in this area.

I tried to make the parts of the spec that deal with things like mining
and mempool to not depend on the concrete contract logic, in
expectation that this logic can be reused afterwards for the specs of
other contracts. I did not make specific effort to factor out this
generic logic into separate module though, because I think that more
various contract specifications need to be designed and analyzed to
understand what is really generic and what should lay with concrete
contract logic. When more knowledge is created regarding this, there
could be a module that contract specifications can use to avoid
explicitly specifying the generic blockchain-related logic.

Thanks to Ruben Somsen for designing this contract and
providing helpful description and diagram that made it possible to
create this formal specification.

[1] https://github.com/dgpv/SASwap_TLAplus_spec