Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap
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 ___ bitcoin-dev mailing list bitcoin-dev@lists.linuxfoundation.org https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap
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 wrote: > В Thu, 14 May 2020 07:31:13 +0200 > Ruben Somsen 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 spend will have 'Bob unilateral > override' case) > ___ bitcoin-dev mailing list bitcoin-dev@lists.linuxfoundation.org https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap
В Thu, 14 May 2020 07:31:13 +0200 Ruben Somsen 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 spend will have 'Bob unilateral override' case) ___ bitcoin-dev mailing list bitcoin-dev@lists.linuxfoundation.org https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap
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 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 wrote:
> В Wed, 13 May 2020 21:03:17 +0200
> Ruben Somsen 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 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 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.
>
___
bitcoin-dev mailing list
bitcoin-dev@lists.linuxfoundation.org
https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap
В Wed, 13 May 2020 21:03:17 +0200
Ruben Somsen 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 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 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.
___
bitcoin-dev mailing list
bitcoin-dev@lists.linuxfoundation.org
https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
Re: [bitcoin-dev] TLA+ specification for Succint Atomic Swap
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 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 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] > >
[bitcoin-dev] TLA+ specification for Succint Atomic Swap
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 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
