ContractModel: Detect Double Satisfaction Problems

[MaximilianAlgehed]

This PR introduces a new property to check for double satisfaction vulnerabilities in any contract with a ContractModel. This property is not complete, but as far as we know it is sound. See the checkDoubleSatisfaction property in Plutus.Contract.Test.ContractModel.

Pre-submit checklist:

• Branch
  • Tests are provided (if possible)
  • Commit sequence broadly makes sense
  • Key commits have useful messages
  • Formatting, PNG optimization, etc. are updated
• PR
  • Self-reviewed the diff
  • Useful pull request description
  • Reviewer requested

[MaximilianAlgehed]

@sjoerdvisscher we didn't touch this code, is something broken on main?

[locallycompact]

What is a double satisfaction problem?

[ThomasArts]

What is a double satisfaction problem?

https://plutus.readthedocs.io/en/latest/reference/common-weaknesses/double-satisfaction.html?highlight=double%20satisfication

[sjoerdvisscher]

@MaximilianAlgehed Hmm, it looks like a legitimate failure, and I don't see it on other branches. Did you try to run cabal test plutus-pab-test-full-long-running locally?

[MaximilianAlgehed]

... It's a cached failure?!

[sjoerdvisscher]

As far as I can tell it is cached from a previous build of this PR.

[MaximilianAlgehed]

This indeed fails locally but I'm absolutely stumped as to why - we haven't touched anything related to the PAB?

[MaximilianAlgehed]

@sjoerdvisscher there is a change to Ledger.Index here! But that's because the semantics of the old code are, as far as I can tell, wrong! The semantics of the old code is that you always pay the collateral, when the semantics should be that you only pay if phase 2 validation fails, no?

[sjoerdvisscher]

the semantics should be that you only pay if phase 2 validation fails, no?

Yes, that's definitely how it's supposed to work.

[MaximilianAlgehed]

So then the old version was buggy (because of how do and infix notation interact). Best regards *Maximilian Algehed*

…

On Thu, 9 Jun 2022 at 18:38, Sjoerd Visscher ***@***.***> wrote: the semantics should be that you only pay if phase 2 validation fails, no? Yes, that's definitely how it's supposed to work. — Reply to this email directly, view it on GitHub <#501 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACBPPQOPKUIVBHCR7ZZKL3LVOIMZXANCNFSM5YCYN2KQ> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[MaximilianAlgehed]

Then the fact that this test is broken tells us something. Is something broken in the PAB or is something broken elsewhere?

[MaximilianAlgehed]

@sjoerdvisscher I'll make a separate PR with that fix and hopefully that means we can dig into the issue in the PAB separately.

[MaximilianAlgehed]

Also, @sjoerdvisscher it would be good if you or someone could just have a look over this to make sure there is nothing absolutely insane going on :)

[sjoerdvisscher]

So then the old version was buggy (because of how do and infix notation interact).

😱

it would be good if you or someone could just have a look over this to make sure there is nothing absolutely insane going on :)

As a comment in the code says -- Double satisfaction magic, and as with any magic it is hard to tell if something insane is going on or not! To be honest this is true for most of the ContractModel code. In can review it for code quality (and this is already quite a task since most PRs are quite big) but I can't review the logic.

Don't forget to rebase on main to get the fix for the OOM CI issue.

[UlfNorell]

@sjoerdvisscher: 43b73ac changed runValidation to no longer compute an updated UtxoIndex. What's the best way to compute that now? We need to keep an up-to-date UtxoIndex when traversing an emulator trace looking for double satisfaction vulnerabilities.

[sjoerdvisscher]

Ah sorry, I keep forgetting that we're not the only ones using these functions. You need something like this:

        idx' = case e of
            Just (Index.Phase1, _) -> idx
            Just (Index.Phase2, _) -> Index.insertCollateral txn idx
            Nothing                -> Index.insert txn idx

[UlfNorell]

Does that mean we should to switch to using CardanoTxs instead of the emulator Tx? Currently we're expecting to find an emulator Tx in TxnValidate events, but that will now be a CardanoTx?

[sjoerdvisscher]

That's right.